Derive and prove the Weil constant for the deployed SSWU variant

[daira]

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

[daira]

Status: the derivation and proof are done and the constant is recorded; the Lean formalization remains.

Done

• Calculated (Add weilbound.sage: Weil character-sum constant for the deployed SSWU mappings zcash/pasta#7, weilbound.sage): for both deployed iso-curves, the branch coverings re-root as hyperelliptic models of genus 6 (against FFSTV's 8), the monodromy is full D₄, the exceptional input set is exactly {0}, and the audited bound is |S_f(χ)| ≤ 10·√q + 3.

• Proven (design/weil-constant-derivation.md on the Counting interface for the indifferentiability arc #27 branch), modulo results cited as established mathematics: Weil's theorem in the form of FFSTV's Lemma 1 and Theorem 3, and standard hyperelliptic point bookkeeping. As anticipated in the body, sign-freeness removes the conductor term. The exact boundary bookkeeping sharpens the bound to |S_f(χ)| ≤ 10·√q + 1 at the deployed parameters (where −A·B is a nonsquare; for valid parameter sets with −A·B square the additive constant is 3). The derivation's two former gaps are closed:

  • Φ is squarefree unconditionally: Φ = φ(ta) for a cubic φ with disc(φ) = −A⁶·B²·(4·A³ + 27·B²), nonzero from A·B ≠ 0 and ellipticity — so genus 6 holds for every valid parameter set, not just the deployed ones.
  • The point counts over u = 0 and ∞ are derived on the smooth model, via the explicit substitution W = y·s_j(u), rather than asserted.

  The supporting identities are checked symbolically by scripts/weil-derivation-checks.sage.

• Recorded: the module doc of Hashing/WellDistributed.lean states the result and the recorded constant — C = 21/2 absorbs the additive term at the deployed sizes with margin ≈ 2¹²⁷.

Remaining

Formalizing the computation in Lean, with the write-up as its source — Weil's theorem itself stays a cited external input, since formalizing it would require machinery not present in Mathlib. (The issue body's final paragraph originally marked this as separately trackable; it has been edited to keep it in scope here.)

Posted with the assistance of Claude Fable 5