Derive and prove the Weil constant for the deployed SSWU variant #28

WeilBounded is the formalization's named external input: WeilBounded f C asserts ‖∑ u, ψ (f u)‖² ≤ C²·#F for every nontrivial character ψ. It is parameterized, and the two-term uniformity bounds scale with C², so consuming the arc's endpoints at the deployed sizes needs an explicit constant for the deployed mappings. No such constant appears to exist in the literature.

What the literature has: FFSTV (also Mathematics of Computation 82 (2013), 491–512), whose Theorem 6 obtains |S_f(χ)| ≤ 52·√q + 151 for a sibling encoding — simplified SWU with Z = -1 over fields of size ≡ 3 (mod 4), with the y-sign chosen by quadratic-residue status (the tweak of Fouque–Tibouchi). The proof runs the two branch coverings through their Theorem 3, computing genus 8 for each by Riemann–Hurwitz, plus a conductor term deg y = 12 that accounts for the residue-status indicator.

The deployed variant differs in all three parameters. RFC 9380's Z-search criteria exclude Z = -1, and the deployed Z = -13 is independently the first admissible candidate for each iso-curve (verified by rerunning the search criteria). The Pasta base fields have size ≡ 1 (mod 4). The sign rule is the parity-based sgn0, which is not a multiplicative character, so the indicator step of the proof does not apply as written.

The task: prove the analogue of Theorem 6 for the deployed parameters. Write down the Z = -13 branch curves (the quartic-in-u coverings with a general nonsquare Z), compute their genus by Riemann–Hurwitz — the calculation itself can be done outside Lean (for example with Sage's function-field machinery), with the proof recorded as the derivation — and assemble the character-sum bound via Theorem 3. Because CharacterSum.lean reduces WeilBounded consumption to the sign-convention-free ±-class multiplicities, the redone bound should not need a sign indicator, so the conductor term may drop and the constant may come out smaller than 52.

The resulting constant then gets recorded in Hashing/WellDistributed.lean as the value that discharges the named hypothesis. Formalizing the computation in Lean is also in scope, as is formalizing the supporting facts for the paper proof — either by turning the design doc into literate Lean, or by adding a Lean file giving the supporting facts as internal endpoints (with a CI check that the design doc refers to exactly those). Out of scope: the function-field vocabulary (genus, places, covers) that stating Weil's theorem itself would need — Weil's theorem stays a cited external input. With that boundary, this issue is closable in the short term.

Status (2026-08-19)

Everything in scope is delivered on PR #29 (weil-covers):

• The constant. The paper proof in design/weil-constant-derivation.md derives |S_f(χ)| ≤ 10·√q + 1 from genus-6 covers. Sign-freeness removes the conductor term and the per-branch double-count. The recorded constant is C = 21/2, in squared form.
• The computation, formalized. Hashing/BranchCovers.lean and Hashing/WeilInstance.lean machine-check everything between the per-cover CharSumBounded inputs (at 100·#F) and the deployed WeilBounded (zeroRepaired mapToCurve) (21/2) instances of Hashing/PastaSSWU.lean, parametrically in the per-cover constant.
• The supporting facts, formalized. Hashing/WeilSupport.lean proves the paper proof's checkable inputs: the squarefreeness lemma's certificate chain and the model degrees (§2), the Eisenstein patterns and the fibre ordinate (§3), and the monodromy square exclusions (§3). CharacterSum.lean adds the §4 realness facts. The design doc cites each proven fact at its point of use, and the weil-support-refs CI job keeps the references exact.

Downstream, the zcash/ironwood#199 arc consumes the instances at concrete advantage q/2^120.

This issue closes when PR #29 merges. The function-field vocabulary stays out of scope, tracked at #30.

🤖 Claude Fable 5