Counting interface for the indifferentiability arc

[daira]

The counting side of the indifferentiability arc (#25; the game side is zcash/ironwood#198): everything the ironwood-side sampler and single-query lemma consume, with no probability in this repo.

Hashing/FibreBound.lean — the fibre bound

Away from the input u = 0, every point of the target curve has at most 10 preimages under SSWUParams.map, over any field where -1 is a square (both Pasta base fields, q ≡ 1 (mod 4)). Nonzero inputs are never exceptional there — ta = 0 would exhibit the nonsquare Z as -1 times a square — so a preimage of an abscissa is a root of the explicit product polynomial Φ_x combining the two branch equations cleared of their common denominator: nonzero of degree at most 10, because its second factor has degree exactly 6 with leading coefficient -B·Z³. The input u = 0 is excluded from the count; a consumer needing the unconditional bound adds it back as at most one extra preimage per point, which is how the ironwood sampler instantiates its fibre-size hypothesis at 11. The optimal constant is 4 (oddness pairs ±u across P and -P, and each branch equation is a quadratic in t), recorded in the module doc as a follow-up; the sampler only needs some explicit constant.

The deployed maps, per curve

isSquare_neg_one by Euler's criterion, the generic composition step card_fibre_comp_le (composing with an injective map does not grow fibres), and Pallas/Vesta.card_mapToCurve_fibre_le through iso_map_bijective. The census records both endpoints, whose native leaves are the Tonelli–Shanks validity witnesses and, through the isogeny's bijectivity, the order witnesses.

Hashing/TwoTermUniformity.lean — deviation exports and the transport

sum_abs_prob_dev_le states the L¹ probability deviation unsquared, against any budget whose square dominates the squared bound, so the ℝ≥0∞-side consumer never needs a square root and a concrete budget is checked by squaring, in exact arithmetic. card_dev_ge_le is the Chebyshev-style counting form of the L² bound: regularity does not lower-bound individual fibres, so the rejection sampler's acceptance constant holds only outside a bad set of fibres, whose size this bounds. sum_abs_pairCount_sub_le bounds the zero-repair transport: mappings agreeing away from a single input have two-term pair counts within 4·#F - 2 of each other in L¹. sum_abs_prob_dev_transport_le combines the two: a mapping agreeing away from a single input with a Weil-bounded one has regularity distance at most ε + (4·#F − 2)/(#F)² — the composed form the ironwood side consumes at the deployed mapToCurve.

The absorbed ironwood extras

Two commits adopt the content of zcash/ironwood's Zcash/Circuits/Specs/CompEllipticExtras.lean, closing #12. CurveForms/ShortWeierstrass.lean gains the rfl projection lemmas SWPoint.add_x/SWPoint.add_y, y_eq_pm_of_onCurve_x_eq (two points on the curve sharing an x-coordinate have y-coordinates equal up to sign), SWPoint.onCurve_of_ne_zero, and SWPoint.eq_pm_of_x_eq (nonzero representable points sharing an x-coordinate are equal up to sign) — ironwood's y_eq_or_y_eq_neg_of_onCurve and eq_or_eq_neg_of_x_eq, renamed to name the shared-abscissa premiss. The last subsumes the private copy that Isogenies/Homomorphism.lean carried. Its ≠ 0 premisses are necessary at SWCurve generality: only B ≠ 0 is bundled, so a curve whose B is a square has a genuine point (0, √B) sharing x = 0 with the 𝒪 sentinel.

Fields/Pasta.lean gains the Fp/Fq abbreviations under their pasta_curves letters, reversing the "not to move" note in #12. The Pallas-side twins neg_five_not_isCube/no_onCurve_y_zero that #12 also requested were already added by #19. ironwood drops its copies of all of this when it bumps its pin.

The Weil constant: calculated, and proven on paper

Hashing/WellDistributed.lean now records that the WeilBounded constant for the deployed Z = -13 mappings has been calculated — |S_f(χ)| ≤ 10·√q + 1 on both iso-curves, from genus-6 branch coverings, recorded as C = 21/2 — by zcash/pasta's weilbound.sage. The calculation is proven on paper in design/weil-constant-derivation.md — 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 — with a Background section pointing to material on the relevant algebraic geometry. The symbolic identities it relies on are checked by scripts/weil-derivation-checks.sage. What remains of #28 is formalizing the calculation in Lean; Weil's theorem itself stays a cited input.

Per the parallel-iteration plan, this merges once the ironwood side compiles against it. It now does (zcash/ironwood branch fv/indiff-sampler), consuming the L¹ exports through the transport and the fibre bound through the rejection-sampling simulator's deployed instantiation; card_dev_ge_le remains for the planned estimate of the capped simulator's average bias.

🤖 Claude Opus 4.8, Claude Fable 5

[daira]

Self-reACK

[dannywillems]

Post-ACK - good to have it here!

[dannywillems]

Post-ACK note: this is interesting by the way. It is not anywhere in the RFC if I paid attention enough.