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 rather than counted: the probability analysis prices pairs containing 0 in its zero-repair correction, and the sampler rides the same term. 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 prices 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.

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; card_dev_ge_le and the fibre bound get their consumers in the costed milestone.

🤖 Claude Opus 4.8

[daira]

Self-reACK