Reduce the deployed Weil bound to Weil's theorem at the branch covers by daira · Pull Request #29 · daira/CompElliptic

daira · 2026-08-18T02:49:42Z

The formal side of #28: everything between Weil's theorem and the deployed WeilBounded instances is now machine-checked. Follows on from #27 which is now merged.

`Hashing/BranchCovers.lean` — the covers as finite objects

Away from the exceptional input, simplified SWU offers two candidate abscissae and outputs a point over whichever makes the curve equation a square. Each branch gets its hyperelliptic model W² = d_j·(Z·u²+1)·Φ(u), with the identities g(x_j u)·s_j(u)² = H_j(u) and the branch dichotomy g(x₂ u) = (Z·u²)³·g(x₁ u) proven in cleared form. modelPoints1/2 are the covers' rational points in model coordinates: the affine solutions plus the two points at infinity exactly when the leading square class d_j·Z is a square. The covering maps send an affine point over u ≠ 0 to the curve point with abscissa x_j u and ordinate W/s_j u, and everything else to 𝒪.

The counting results, for any commutative-monoid-valued φ:

fibre_sum: over each u ≠ 0, the two covers' fibres together contribute exactly φ(map u) + φ(-(map u)) — the square branch's two roots supply the pair, and the other branch's fibre is empty;
modelPoints_sum: with -A·B a nonsquare, S₁ + S₂ = Σ_{u ≠ 0} (φ(map u) + φ(-(map u))) + 4·φ(𝒪) — the boundary bookkeeping of the design doc's §4.

`Hashing/WeilInstance.lean` — the cited input and the assembly

CharSumBounded s h B is the shape in which Weil's theorem enters: every nontrivial character sums to at most B in squared norm over the images of a finite point set. cover_charSum is the sign-free assembly S₁(ψ) + S₂(ψ) = 2·S(ψ) + 2. weilBounded_zeroRepaired turns the two cover inputs into WeilBounded (zeroRepaired G.map) (c + 1/2), square-root-free, parametrically in the per-cover constant c (inputs at c²·#F, threshold #F ≥ 4·c + 4).

The constant is a parameter because the cited constant depends on which genus fact the citation uses, and the candidates differ in formalization cost. The deployed citation takes c = 10 = 2·6 - 2 from the exact genus (Riemann–Hurwitz tier). Riemann's inequality bounds the genus by 13 from the two field generators alone — elementary divisor counting — giving c = 24 at a cost of (24.5/10.5)² ≈ 2^{2.44} in the regularity distance. Parameterizing keeps every consumer unchanged if the cited constant moves.

The deployed instances

WeilBounded.comp (in WellDistributed.lean) transfers the bound along a bijective homomorphism of the target group. Pallas/Vesta.weilBounded_zeroRepaired_mapToCurve (in PastaSSWU.lean) then derive WeilBounded (zeroRepaired mapToCurve) (21/2) from the two CharSumBounded inputs at 100·#F alone, crossing the 3-isogeny; the instantiation adds Euler certificates for -A·B a nonsquare on both iso-curves (the same fact as the empty w = 0 fibre that weilbound.sage checks).

The supporting facts (#28)

Hashing/WeilSupport.lean proves the checkable inputs of the cited steps. For the genus (§2): phiPoly_squarefree (by a Bézout certificate whose constant is A³·B²·(4·A³ + 27·B²), transported along comp ta, with the two critical-value cases), and the models squarefree of degree exactly 14. For the ramification (§3): the Eisenstein patterns of the branch quartics at the ideal (w), and g(-B/A) = -(B/A)³ ≠ 0. For the monodromy cross-check (§3): neither B·(A·x + B) nor B·(A·x - 3·B) is a square in the function field, presented as the quadratic algebra K[Y]/(Y² - ĝ) over K = F_q(x) — the divisor-parity step in its affine form, polynomial vocabulary only. CharacterSum.lean gains the §4 realness facts (IsOdd.conj_charSum, IsOdd.two_mul_charSum). WeilSupport.lean reads in the design doc's order.

The design doc weaves references to the proven facts into its argument at their points of use — the supporting facts and the already-proven statements of the cover and assembly modules alike. The weil-support-refs CI job checks the correspondence in three directions:

every declaration in WeilSupport.lean is referenced somewhere in the doc;
every backticked identifier in the doc (dot-qualified ones included) resolves to a declaration: an exact fully qualified name, or a dot-path suffix of one under CompElliptic.{Hashing,Curves} (the two RFC 9380 operation names are allowlisted; filenames are skipped); a citation that also matches a name outside those modules must qualify itself;
every declaration a citation can refer to is pinned directly in the axiom census (TrustBoundary.lean): the doc's reader relies on everything it cites, so an unpinned citation would be a gap in axiom-checking.

What stays cited

The two CharSumBounded inputs bundle Weil's theorem in the form of FFSTV's Theorem 3, applied at genus 6 with the no-unramified-subcover condition; both applicability conditions are derived on paper in design/weil-constant-derivation.md §2–3. Mathlib does not yet have the vocabulary to state them (genus, places, covers of curves); that vocabulary is out of #28's scope and tracked at #30 — the Riemann's-inequality route, which would replace the paper genus with a formal bound of 13, i.e. per-cover constant c = 24 and recorded constant C = 24.5. The monodromy paragraph's Kappe–Warren classification is cited likewise; its two square-class failures are now machine-checked, and the reductions to them are checked symbolically.

Housekeeping

The FFSTV citation appears in full at its first use.
Every declaration in the PR's files carries a doc comment; the field-file docstrings are emitted by the generators, so the reproduction job stays exact.
Module docs quote the derived bound (C = 21/2, statistical distance near 2^{-120}) where they previously said none had been derived; the Derive and prove the Weil constant for the deployed SSWU variant #28 tracking pointers are retired; and the recorded absorption margin is corrected to ≈ 2^{126} (the earlier 2^{127} quoted √q's exponent and dropped the half).
The sage job gained steps running scripts/check_weil_derivations.sage (the design doc's symbolic identities and the WeilSupport certificates) and scripts/check_sswu_small_curves.sage (the book's small-curve branch statistics). The job's check-run name changed to "sage checks - Vélu certificates and Weil-derivation identities"; branch protection may want the rename.

The ironwood side consumes these in zcash/ironwood#199: concrete endpoints (pallas_indiffFromRO, vesta_indiffFromRO) at advantage q/2^120, taking only these cover inputs.

🤖 Claude Fable 5

daira · 2026-08-18T16:54:32Z

This depends on #27 but its base is main. To see the diff relative to #27: indiff-counting...weil-covers

PR #29 closes #28, so module docs should not point at it as pending work. BranchCovers now names WeilInstance as the consumer it once tracked; WeilInstance keeps only the #30 vocabulary pointer; and WellDistributed's "what remains of #28" claim — stale since the calculation landed — becomes the present state, naming the files that formalize the calculation and the supporting facts. WeilSupport's #28 mention stays: it is provenance, not a tracking claim. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

daira

Self-ACK

The algebraic core of the Weil-constant derivation (design/weil-constant-derivation.md §2), at SSWUParams generality: the branch abscissae x1 and x2, the shared degree-12 core Φ (phiCore), the models H_j = d_j·(Z·u²+1)·Φ (model1/model2, twist1/twist2), and the scalings s_j (scale1/scale2). The identities g(x_j u)·(s_j u)² = H_j u (model1_eq/model2_eq) put the model value and the curve equation at the branch abscissa in the same square class away from u = 0; g_x2_eq is the branch dichotomy g(x₂ u) = (Z·u²)³·g(x₁ u). Zuu_add_one_ne_zero is the empty t = -1 fibre: on a field where -1 is a square, Z·u²+1 never vanishes, so the scalings vanish only at u = 0. The cleared-form proofs eliminate the abscissa's denominator through x1_mul_den and discharge each identity by linear_combination with an explicit cofactor. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

modelPoints1/2 are each cover's rational points in model coordinates. They hold the affine solutions of W² = H_j(u), plus the two points at infinity exactly when the leading square class d_j·Z is a square. Membership simp lemmas are included. cover1Map/cover2Map send a model point to the curve: * an affine point over u ≠ 0 goes to the point with abscissa x_j u and ordinate W/s_j u, on the curve by the model identities; * everything else goes to 𝒪: the u = 0 fibre, the points at infinity, and junk off the model. The 𝒪 image is genuine on the parameter range the correspondence targets (-A·B a nonsquare). Supporting facts: * the models never vanish (model1_ne_zero, model2_ne_zero): a zero away from u = 0 would put a zero-ordinate point on the curve, against the no-2-torsion hypothesis, and at u = 0 the values are d_j·B²; * nonsquares force odd characteristic (ringChar_ne_two); * a nonzero square has exactly the two roots ±r, and a nonsquare has none (filter_sq_eq_pair, filter_sq_card_of_isSquare, filter_sq_eq_empty) — the counting the fibre analysis consumes. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

map_x is the branch selection: for u ≠ 0 the mapping outputs the branch whose curve-equation value is a square. The square-root split tests IsSquare (U/xdiv³), and U/xdiv³ = g(x₁ u) by a cleared-form identity. map_y_sq restates the on-curve fact through map. fibre_sum is the heart of the correspondence. Over u ≠ 0, summed across both covers, the affine model fibres contribute exactly φ(map u) + φ(-(map u)): * the square branch's fibre is the two roots ±((map u).y·s_j u), and the covering map sends them to map u and -(map u); * the other branch's fibre is empty, because its model value is a nonsquare. The dichotomy rests on not_isSquare_mul_sq (a nonsquare times a nonzero square is a nonsquare; Mathlib has no such lemma) and, for the two-nonsquares direction, isSquare_mul_of_not_isSquare. The evaluation lemmas cover1Map_inl_x/_y and cover2Map_inl_x/_y compute the covering maps at genuine affine points. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

modelPoints_sum: on the parameter range with -A·B a nonsquare, S₁ + S₂ = Σ_{u ≠ 0} (φ(map u) + φ(-(map u))) + 4·φ(𝒪), where S_j sums any commutative-monoid-valued φ of the covering-map images over cover j's full point set. The boundary bookkeeping supplies the 4·φ(𝒪): * cover 1 has no points at infinity (twist1·Z ≡ -A·B, a nonsquare), and its u = 0 fibre is a rational pair (model1 0 ≡ -A·B·Z, a square) mapping to 𝒪; * cover 2 has an empty u = 0 fibre (model2 0 ≡ -A·B) and a rational pair at infinity (twist2·Z ≡ -A·B·Z) mapping to 𝒪. The affine parts decompose through sum_filter_prod (a filtered product sum as a double sum), and the u ≠ 0 columns collapse pairwise by fibre_sum. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

WeilInstance.lean states the shape in which Weil's theorem enters and derives the deployed Weil bound from it. CharSumBounded s h B is the squared curve character-sum bound: every nontrivial character sums to at most B in squared norm over the images of the point set. The intended instantiations take B = 100·#F, the squared (2·6 - 2)·√q of the genus-6 branch coverings. The genus and the no-unramified-subcover condition are cited from design/weil-constant-derivation.md §2-3: even their statements need machinery absent from Mathlib (genus, places, covers). cover_charSum is the sign-free assembly (§4): for every character ψ, S₁(ψ) + S₂(ψ) = 2·S(ψ) + 2, with S the zero-repaired mapping's character sum. Negating the input permutes the nonzero inputs and negates the output, so each input's pair ±(map u) contributes twice the mapping's sum; the four boundary points give ψ(𝒪) = 1 each, and the repaired u = 0 input supplies the -2 that turns `+ 4` into `+ 2`. weilBounded_zeroRepaired combines the assembly with the two cover bounds, square-root-free: ‖S‖² ≤ (21/2)²·#F for #F ≥ 44, i.e. WeilBounded (zeroRepaired G.map) (21/2). The margin between the sharp 10·√q + 1 and the recorded (21/2)·√q absorbs the boundary terms. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

WeilBounded.comp transfers the Weil bound along a bijective homomorphism of the target group: characters pull back along the homomorphism, surjectivity keeps nontrivial characters nontrivial, and the pulled-back sum is the original one. Per curve, weilBounded_zeroRepaired_mapToCurve derives WeilBounded (zeroRepaired mapToCurve) (21/2) from the two CharSumBounded inputs at 100·#F alone. The instantiation supplies: * -A·B a nonsquare (neg_AB_not_isSquare): Euler's criterion, with the compound term first reduced to a hex literal — reduce_mod_char does not normalize projection-headed bases; * the no-2-torsion fact (iso_no_onCurve_y_zero) and the sign-function property (isSignFunction_sgn0); * the field-size floor 44 ≤ #F, by ZMod.card and decide. The bound crosses the 3-isogeny through WeilBounded.comp, because the isogeny is a bijective homomorphism on rational points; zero-repair commutes with it since homomorphisms preserve 𝒪. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

weilBounded_zeroRepaired now takes an arbitrary per-cover constant c > 0: inputs at c²·#F, conclusion at c + 1/2, and threshold #F ≥ 4·c + 4 (the deployed 44 is 4·10 + 4). The per-curve endpoints keep the deployed constants (100·#F, 21/2) and invoke the general theorem at c := 10. Why: the cited constant depends on which genus fact the citation uses, and the candidates differ in formalization cost, not just in value. The deployed citation takes c = 10 = 2·6 - 2 from the exact genus. Riemann's inequality (Stichtenoth §3.11) bounds the genus by (2-1)·(14-1) = 13 from the two field generators alone. That is elementary divisor counting, far below the Riemann–Hurwitz tier that exact genus 6 needs. The corresponding constant is c = 24; the regularity distance scales with the square of the consumed constant c + 1/2, so the cost is (24.5/10.5)² ≈ 2^{2.44}. Parameterizing keeps every consumer unchanged if the cited constant moves. The module doc also drops an overclaim: the cited statements are not inexpressible in principle — Mathlib lacks the genus/places/covers vocabulary today, and building the function-field layer is a tractable project. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

WeilSupport.lean proves the checkable inputs of the design doc's two cited steps, so that only the genuinely geometric arguments remain on paper (#28; the vocabulary itself is #30). For the genus computation (§2): * phiPoly_squarefree, by the doc's own argument. The cubic factor is separable by a Bézout certificate whose constant is A³·B²·(4·A³ + 27·B²) —exactly the standing nonzero quantities— and separability transports along comp ta. The u = 0 case has Φ(0) = B²; the Z·u² = -1/2 case re-expands 64·Φ = Ψ(2·Z·X² + 1), whose constant term is the ellipticity. * The models are squarefree of degree exactly 14 (model1/2Poly_squarefree, model1/2Poly_natDegree) — the inputs to the cited genus formula g = ⌊(14-1)/2⌋ = 6 (Galbraith ch. 10; Stichtenoth ch. 6). For the ramification argument (§3): * The branch quartics over F[w] are Eisenstein at (w) (p2Poly_isEisensteinAt, p1RecipPoly_isEisensteinAt), in Mathlib's IsEisensteinAt sense. * g(-B/A) = -(B/A)³ ≠ 0 (eval_g_neg_B_div_A, g_neg_B_div_A_ne_zero): w is a uniformizer at both points over w = 0. Evaluation lemmas tie each polynomial to BranchCovers' pointwise functions. New Hashing-level helpers: isCoprime_of_bezout, isCoprime_X_of_coeff_zero, isCoprime_C_of_ne_zero, not_X_sq_dvd. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

The design doc now references the formalized supporting facts at their points of use, woven into the argument: the §2 squarefreeness lemma names its formal counterpart step for step (the composition, the Bézout certificate replacing the discriminant, the two critical-value cases, and the assembled phiPoly_squarefree with the degree-14 squarefree models); §3's Eisenstein bullets and the fibre ordinate name theirs. The Status paragraph records the machine-checked state: the calculation from the per-cover Weil inputs to the deployed constants, and the checkable inputs of the two cited steps; the cited steps themselves and Weil's theorem stay on paper, with the vocabulary tracked at #30. scripts/check_weil_support_refs.py, run as the weil-support-refs CI job, checks two directions over the whole doc: every WeilSupport declaration is referenced somewhere, and every backticked identifier resolves to a CompElliptic declaration or is on the explicit allowlist of non-Lean names (RFC function names; filenames exclude themselves by their extensions). The certificates that WeilSupport.lean transcribes —φ's Bézout cofactors, the re-expansion 64·Φ = Ψ(2·z·u² + 1), and the coprimality decomposition of Φ against z·u² + 1— are checked symbolically in weil-derivation-checks.sage. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

Statements that BranchCovers, WeilInstance, PastaSSWU, WellDistributed, CharacterSum, and TwoTermUniformity already prove now cite their Lean names at the point of use: the abscissae and the branch dichotomy and the exceptional set (§1), the pointwise core, the twist constants, and the clearing identities (§2), the model point sets, scalings, fibre sum, boundary values, Euler certificates, and assembly (§4), and the parametric bound, isogeny transfer, and regularity budget (§5). The checker now resolves dot-qualified names by their final segment and skips backticked filenames explicitly; both were previously invisible to its soundness pass. Multi-digit Unicode superscripts in the doc become braced ASCII exponents, per the notation convention. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

`IsOdd.conj_charSum`: complex conjugation fixes `∑ u, ψ (f u)` — conjugating a term negates the output (`addChar_map_neg_eq_conj`, since every character value on a finite group is a root of unity), oddness trades that for negating the input, and input negation permutes the domain. `IsOdd.two_mul_charSum` is the doubled sign-free form `2·S = ∑ u, (ψ (f u) + conj (ψ (f u)))`. These formalize the design doc's §4 passage "substituting u → −u shows S_f(χ) is real" and its displayed identity, which now cite them. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

Design doc §3 pins the monodromy at full D₄ by refuting the biquadratic V₄/C₄ square-class tests: neither B·(A·x + B) nor B·(A·x - 3·B) is a square in the function field F_q(E′). The failures are now formalized (`v4TestPoly_not_isSquare`, `c4TestPoly_not_isSquare`), with no vocabulary beyond polynomials: F_q(E′) is the quadratic algebra K[Y]/(Y² - ĝ) over K = F_q(x), where a base-field square decomposes as p² or ĝ·p² (`sq_or_mul_sq_of_isSquare_adjoinRoot`), rational square roots of polynomials are polynomial (`exists_sq_eq_of_ratFunc_sq`, as F[X] is integrally closed), and squarefree polynomials of positive degree are not squares (`not_isSquare_ratFunc_of_squarefree`) — the affine shadow of the paper's divisor parity. `gPoly_separable` and the two linear coprimality certificates supply the squarefree products; `gPoly_not_isSquare_ratFunc` is why the algebra is the field itself. The Bézout certificates and the Kappe–Warren reductions to the two square classes are checked in scripts/weil-derivation-checks.sage; the design doc weaves the new names into §3. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

The file now follows design/weil-constant-derivation.md: the core and the model polynomials with their evaluations first, then the genus inputs (Φ at u = 0, coprimality with Z·X² + 1), then the squarefreeness lemma's development (the cubic and its certificate, the critical-locus cases, separability), then the models' squarefreeness and degrees, and in §3 the fibre ordinate before the Eisenstein patterns. Pure moves plus retitled section headers; no statement or proof changes. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

PR #29 closes #28, so module docs should not point at it as pending work. BranchCovers now names WeilInstance as the consumer it once tracked; WeilInstance keeps only the #30 vocabulary pointer; and WellDistributed's "what remains of #28" claim — stale since the calculation landed — becomes the present state, naming the files that formalize the calculation and the supporting facts. WeilSupport's #28 mention stays: it is provenance, not a tracking claim. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

`fibrePoly_natDegree_le` and the six field-file core declarations (`*_CARD`, the field abbreviations, and the primality theorems) were the PR's only declarations without doc comments. The field files are generated, so the docstrings come from the generators: `field_block` now takes the three docstrings explicitly, and both field files are regenerated (Jubjub picks up the same pattern). Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

The module doc and the `sq_sum_abs_prob_dev_le` docstring still said no constant had been derived for the deployed mappings — stale since the derivation landed. Both now state the present bound: C = 21/2 puts the statistical distance near 2^{-120}. The FFSTV comparisons are dropped here; `WellDistributed.lean`'s reference block and the design doc's §5 already make them. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

scripts/weil-derivation-checks.sage — the design doc's symbolic identities and the WeilSupport Bézout and Kappe–Warren certificates — ran only locally. Fold it into the existing sage job as a further step after the Vélu regeneration, so both share one environment setup rather than each restoring the cache. Every script that makes load-bearing correctness assertions now has a CI step. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

The book's group-hash page says the heuristic branch proportions were confirmed by exact computation on small curves; this is that computation (scripts/check_sswu_small_curves.sage), committed so the claim has a linkable artifact. For each small deployed-shape instance it enumerates the mapping and checks: the branch images coincide (single-branch points reported — zero at every instance here), about 3/8 of the group is reached with the 1/8-vs-1/4 split of 4- and 2-preimage points (within a Lang–Weil-shaped tolerance), and every reached point other than 𝒪 has exactly 2 or 4 preimages (exact, not statistical). It runs as a further step of the sage job: the assertions are not load-bearing for the correctness chain, but they are assertions. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

scripts/weil-derivation-checks.sage becomes scripts/check_weil_derivations.sage, matching the check_* snake_case convention of the other check scripts; the CI step, the design doc, and the WeilSupport module references follow. (Its sibling check_sswu_small_curves.sage was renamed at introduction.) Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

(10·√q + 1)² ≤ (21/2)²·q reduces to 10.25·q ≥ 20·√q + 1, whose sides are in ratio ≈ 2^{126} at the deployed sizes — equivalently, the extra half buys 0.5·√q ≈ 2^{126} of unsquared headroom against the trailing +1. The recorded 2^{127} quoted √q's exponent and dropped the half. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

The full Farashahi–Fouque–Shparlinski–Tibouchi–Voloch citation lived in the notation paragraph before §1, but the Status paragraph had already been using the "FFSTV" abbreviation, and the Background section's "FFSTV as above" had nothing above to point to. Move the full citation to the first use and abbreviate the later mention. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

The design doc is a pencil-and-paper proof whose reader relies on every Lean declaration it cites, so an unpinned citation would be a gap in axiom-checking: a cited fact could widen its trusted base with no census entry noticing. TrustBoundary.lean gains a section pinning all of the doc's citations, and check_weil_support_refs.py gains the matching third direction: it fails when the doc cites a declaration that no census entry names directly. An ambiguous short reference (mapToCurve) is satisfied by any of its instantiations; the census pins all of them. Definitions whose point is usable data carry assert_computable. The model point sets and covering maps reach Classical.choice through erased Prop fields; the deployed mapToCurve forms additionally trust the Tonelli–Shanks native certificates. The supporting polynomials are noncomputable, so they take assert_axioms like the theorems and the Prop-shaped definitions. The per-curve Weil endpoints trust the Tonelli–Shanks certificates and the group-order witnesses; the Euler certificates behind neg_AB_not_isSquare are kernel decides, so those entries need no flags. The CI step name follows; the job's check-run name is unchanged. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

Final-segment matching let a bogus qualified citation resolve against any declaration with the same last segment — e.g. `junk.gPoly` would match any declaration ending in gPoly. A citation now resolves, and satisfies the census-pin check, only when it is a dot-path suffix of some fully qualified name. The checker reconstructs those from the namespace/end pairs — the same reconstruction logic as ironwood's check_endpoint_census.sh. The declaration matcher gains the modifier and keyword handling of that script too: private declarations are not citable, so they are no longer collected. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

A dot-path-suffix citation now resolves only against declarations under CompElliptic.{Hashing,Curves}; allowing matches in any module would incur a greater risk of typos accidentally matching unrelated names. A fully qualified citation may still name any declaration. Three consequences are checked: * a citation that also matches a name outside the relevant modules must qualify itself — the doc's map_neg did, and now cites SSWUParams.map_neg to disambiguate from the isogeny lemma; * a reference is pinned only when every declaration it can refer to is in the census, not just one of them; * a declared Lean name that could be mistaken for a filename or an allowlisted non-Lean term is rejected — at any namespace depth, so the citation filters cannot silently mask a real declaration. An unknown citation selects no referents: its remedy is fixing the citation, so it does not also demand qualification or pins for its suffix matches. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

dannywillems

Post-merge ACK

daira force-pushed the weil-covers branch from ac602c7 to db3b802 Compare August 18, 2026 09:10

daira mentioned this pull request Aug 18, 2026

Function-field vocabulary and Riemann's inequality: a formal genus bound for the Weil input #30

Open

daira force-pushed the weil-covers branch from db3b802 to 0f9324a Compare August 18, 2026 16:48

daira force-pushed the weil-covers branch 2 times, most recently from 558ca58 to 7f965ed Compare August 18, 2026 23:20

daira mentioned this pull request Aug 18, 2026

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

Closed

daira linked an issue Aug 18, 2026 that may be closed by this pull request

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

Closed

daira marked this pull request as ready for review August 18, 2026 23:35

daira force-pushed the weil-covers branch 2 times, most recently from 7f7d04d to 54ae620 Compare August 19, 2026 01:20

daira commented Aug 19, 2026

View reviewed changes

daira mentioned this pull request Aug 19, 2026

Group-hash indifferentiability: security games, rejection-sampling simulator, and concrete endpoints zcash/ironwood#199

Merged

daira force-pushed the weil-covers branch 2 times, most recently from a8acc8b to 75ef7a2 Compare August 19, 2026 12:18

daira commented Aug 19, 2026

View reviewed changes

Comment thread design/weil-constant-derivation.md Outdated

daira commented Aug 19, 2026

View reviewed changes

Comment thread scripts/check_weil_support_refs.py

daira commented Aug 20, 2026

View reviewed changes

Comment thread .github/workflows/ci.yml Outdated

daira and others added 11 commits August 20, 2026 06:42

daira and others added 14 commits August 20, 2026 06:42

ci: one sage environment for all steps — the job has three now

45607a0

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

daira force-pushed the weil-covers branch from 2d7ea65 to 45607a0 Compare August 20, 2026 05:42

daira merged commit 2c04440 into main Aug 20, 2026
11 checks passed

daira deleted the weil-covers branch August 20, 2026 06:03

daira mentioned this pull request Aug 20, 2026

Justify indifferentiability of mapHashOutputsToCurve from an RO wrt the hash_to_field outputs #25

Closed

dannywillems reviewed Aug 20, 2026

View reviewed changes

Navigation Menu

Reduce the deployed Weil bound to Weil's theorem at the branch covers - #29

Reduce the deployed Weil bound to Weil's theorem at the branch covers#29
daira merged 25 commits into
mainfrom
weil-covers

daira commented Aug 18, 2026 •

edited

Loading

Uh oh!

daira commented Aug 18, 2026 •

edited

Loading

Uh oh!

daira left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

dannywillems left a comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

daira commented Aug 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Hashing/BranchCovers.lean — the covers as finite objects

Hashing/WeilInstance.lean — the cited input and the assembly

The deployed instances

The supporting facts (#28)

What stays cited

Housekeeping

Uh oh!

daira commented Aug 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

daira left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

dannywillems left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

daira commented Aug 18, 2026 •

edited

Loading

`Hashing/BranchCovers.lean` — the covers as finite objects

`Hashing/WeilInstance.lean` — the cited input and the assembly

daira commented Aug 18, 2026 •

edited

Loading