From 13dd9e4c4339df2ac4a65ecdb1c80e58f19c930c Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Mon, 17 Aug 2026 22:33:18 +0100 Subject: [PATCH 01/25] feat(Hashing): the branch covers' hyperelliptic models MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- CompElliptic.lean | 1 + CompElliptic/Hashing/BranchCovers.lean | 204 +++++++++++++++++++++++++ 2 files changed, 205 insertions(+) create mode 100644 CompElliptic/Hashing/BranchCovers.lean diff --git a/CompElliptic.lean b/CompElliptic.lean index 47774e4..f72357d 100644 --- a/CompElliptic.lean +++ b/CompElliptic.lean @@ -19,6 +19,7 @@ import CompElliptic.Isogenies.ThreeIsogeny import CompElliptic.Curves.Pasta import CompElliptic.Curves.IsoPasta import CompElliptic.Curves.PastaOrder +import CompElliptic.Hashing.BranchCovers import CompElliptic.Hashing.CharacterSum import CompElliptic.Hashing.PastaSSWU import CompElliptic.Hashing.SignedLift diff --git a/CompElliptic/Hashing/BranchCovers.lean b/CompElliptic/Hashing/BranchCovers.lean new file mode 100644 index 0000000..afe8dda --- /dev/null +++ b/CompElliptic/Hashing/BranchCovers.lean @@ -0,0 +1,204 @@ +/- +Copyright (c) 2026 CompElliptic Contributors. +Released under the Apache License, Version 2.0, or the MIT license, at your option, +as described in the files LICENSE-APACHE and LICENSE-MIT. +Authors: Daira-Emma Hopwood +-/ +import CompElliptic.Hashing.FibreBound + +/-! +# The branch covers of the simplified SWU mapping + +Away from the exceptional input, the simplified SWU mapping offers two +candidate abscissae `x₁ u` and `x₂ u`, and outputs a point over whichever one +makes the curve equation `g x = x³ + A·x + B` a square. This file gives each +branch its hyperelliptic model: the curve equation at the branch abscissa, +cleared of denominators. Writing `ta = (Z·u²)² + Z·u²`, both branches share +the degree-12 core + +`Φ(u) = B²·(ta + 1)³ + A³·ta²` (`phiCore`), + +and the two models are `W² = d_j·(Z·u²+1)·Φ(u)` (`model1`, `model2`) with +twist constants `d₁ = -A³·B·Z³` and `d₂ = -A³·B` (`twist1`, `twist2`). The +main identities `model1_eq` and `model2_eq` state that the model value is +the curve equation at the branch abscissa times the square of an explicit +scaling (`scale1`, `scale2`). `g_x2_eq` is the branch dichotomy in algebraic +form: `g (x₂ u) = (Z·u²)³ · g (x₁ u)`. + +The notation follows `design/weil-constant-derivation.md` §2, which derives +the Weil character-sum bound for the deployed mappings from these models; +formal consumption of that bound is tracked at +. + +On a field where `-1` is a square (both Pasta base fields), `Z·u² + 1` never +vanishes (`Zuu_add_one_ne_zero`), so the scalings vanish only at `u = 0` and +the models are nonzero wherever `Φ` is. +-/ + +namespace CompElliptic.Hashing + +namespace SSWUParams + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] + +/-- The first branch abscissa `x₁ u = B·(ta + 1) / (A·(-ta))`, the value +`(G.mapXYUpToSign u).1` takes when the square-root split chooses the first +branch (and `ta ≠ 0`). -/ +def x1 (G : SSWUParams F) (u : F) : F := + G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1) + / (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2)) + +/-- The second branch abscissa `x₂ u = Z·u² · x₁ u`. -/ +def x2 (G : SSWUParams F) (u : F) : F := G.Z * u^2 * G.x1 u + +/-- The shared degree-12 core `Φ(u) = B²·(ta + 1)³ + A³·ta²` of the two +branch models, with `ta = (Z·u²)² + Z·u²`. -/ +def phiCore (G : SSWUParams F) (u : F) : F := + G.E.B^2 * (((G.Z * u^2)^2 + G.Z * u^2) + 1)^3 + + G.E.A^3 * ((G.Z * u^2)^2 + G.Z * u^2)^2 + +/-- The twist constant `d₁ = -A³·B·Z³` of the first branch model. -/ +def twist1 (G : SSWUParams F) : F := -(G.E.A^3 * G.E.B * G.Z^3) + +/-- The twist constant `d₂ = -A³·B` of the second branch model. `twist1` and +`twist2` differ by `Z³`, which is `Z` times a square: the two models are +quadratic twists of one another by the nonsquare `Z`. -/ +def twist2 (G : SSWUParams F) : F := -(G.E.A^3 * G.E.B) + +/-- The first branch model `H₁(u) = d₁·(Z·u²+1)·Φ(u)`. -/ +def model1 (G : SSWUParams F) (u : F) : F := + G.twist1 * (G.Z * u^2 + 1) * G.phiCore u + +/-- The second branch model `H₂(u) = d₂·(Z·u²+1)·Φ(u)`. -/ +def model2 (G : SSWUParams F) (u : F) : F := + G.twist2 * (G.Z * u^2 + 1) * G.phiCore u + +/-- The scaling `s₁ u = A³·Z³·u³·(Z·u²+1)²` relating the first branch's +ordinate to the model coordinate: `W = y·s₁ u` on the first cover. -/ +def scale1 (G : SSWUParams F) (u : F) : F := + G.E.A^3 * G.Z^3 * u^3 * (G.Z * u^2 + 1)^2 + +/-- The scaling `s₂ u = A³·(Z·u²+1)²` relating the second branch's ordinate +to the model coordinate: `W = y·s₂ u` on the second cover. -/ +def scale2 (G : SSWUParams F) (u : F) : F := + G.E.A^3 * (G.Z * u^2 + 1)^2 + +/-- On a field where `-1` is a square, `Z·u² + 1` never vanishes: a root +would exhibit the nonsquare `Z` as `-1` times a square. This is the +exceptional-set lemma of the derivation: the `t = -1` fibre of the branch +covers has no rational points. -/ +theorem Zuu_add_one_ne_zero (G : SSWUParams F) (hsq : IsSquare (-1 : F)) + (u : F) : G.Z * u^2 + 1 ≠ 0 := by + intro h + rcases eq_or_ne u 0 with rfl | hu + · simp at h + · obtain ⟨s, hs⟩ := hsq + have hZu : G.Z * u^2 = -1 := by linear_combination h + refine G.Z_nonsquare ⟨s/u, ?_⟩ + rw [div_mul_div_comm, show u*u = u^2 from (pow_two u).symm] + exact (eq_div_iff (pow_ne_zero 2 hu)).mpr (hZu.trans hs) + +/-- `Φ(0) = B²`: the core is nonzero at `u = 0`. -/ +theorem phiCore_zero (G : SSWUParams F) : G.phiCore 0 = G.E.B^2 := by + simp [phiCore] + +/-- The first model at `u = 0` is `d₁·B²`, in the square class of `d₁`. -/ +theorem model1_zero (G : SSWUParams F) : G.model1 0 = G.twist1 * G.E.B^2 := by + simp [model1, phiCore_zero] + +/-- The second model at `u = 0` is `d₂·B²`, in the square class of `d₂`. -/ +theorem model2_zero (G : SSWUParams F) : G.model2 0 = G.twist2 * G.E.B^2 := by + simp [model2, phiCore_zero] + +/-- The first scaling vanishes exactly at `u = 0` (on a field where `-1` is +a square). -/ +theorem scale1_ne_zero (G : SSWUParams F) (hsq : IsSquare (-1 : F)) {u : F} + (hu : u ≠ 0) : G.scale1 u ≠ 0 := by + unfold scale1 + exact mul_ne_zero (mul_ne_zero (mul_ne_zero (pow_ne_zero 3 G.A_nonzero) + (pow_ne_zero 3 G.Z_nonzero)) (pow_ne_zero 3 hu)) + (pow_ne_zero 2 (G.Zuu_add_one_ne_zero hsq u)) + +/-- The second scaling never vanishes (on a field where `-1` is a square). -/ +theorem scale2_ne_zero (G : SSWUParams F) (hsq : IsSquare (-1 : F)) (u : F) : + G.scale2 u ≠ 0 := by + unfold scale2 + exact mul_ne_zero (pow_ne_zero 3 G.A_nonzero) + (pow_ne_zero 2 (G.Zuu_add_one_ne_zero hsq u)) + +section ClearedIdentities + +variable (G : SSWUParams F) + +/-- The defining equation of `x₁ u`, cleared of its denominator: +`x₁ u · (A·(-ta)) = B·(ta + 1)`. -/ +theorem x1_mul_den (hsq : IsSquare (-1 : F)) {u : F} (hu : u ≠ 0) : + G.x1 u * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2)) + = G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1) := by + have hden : G.E.A * -((G.Z * u^2)^2 + G.Z * u^2) ≠ 0 := + mul_ne_zero G.A_nonzero + (neg_ne_zero.mpr (G.ta_ne_zero_of_u_ne_zero hsq hu)) + unfold x1 + exact div_mul_cancel₀ _ hden + +/-- **The first branch model identity**: the curve equation at `x₁ u`, times +the square of the scaling `s₁ u`, is the model value `H₁(u)`. Away from +`u = 0` the scaling is nonzero, so `H₁(u)` and `g (x₁ u)` are in the same +square class. -/ +theorem model1_eq (hsq : IsSquare (-1 : F)) {u : F} (hu : u ≠ 0) : + ((G.x1 u)^3 + G.E.A * G.x1 u + G.E.B) * (G.scale1 u)^2 = G.model1 u := by + have hden : G.E.A * -((G.Z * u^2)^2 + G.Z * u^2) ≠ 0 := + mul_ne_zero G.A_nonzero + (neg_ne_zero.mpr (G.ta_ne_zero_of_u_ne_zero hsq hu)) + have hX := G.x1_mul_den hsq hu + unfold scale1 model1 twist1 phiCore + refine mul_left_cancel₀ (pow_ne_zero 3 hden) ?_ + linear_combination ((G.E.A^3 * G.Z^3 * u^3 * (G.Z * u^2 + 1)^2)^2 * + ((G.x1 u * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2)))^2 + + G.x1 u * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2)) + * (G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1)) + + (G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1))^2 + + G.E.A * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2))^2)) * hX + +/-- **The second branch model identity**: the curve equation at `x₂ u`, times +the square of the scaling `s₂ u`, is the model value `H₂(u)`. The scaling is +nowhere zero, so `H₂(u)` and `g (x₂ u)` are in the same square class at every +`u ≠ 0`. -/ +theorem model2_eq (hsq : IsSquare (-1 : F)) {u : F} (hu : u ≠ 0) : + ((G.x2 u)^3 + G.E.A * G.x2 u + G.E.B) * (G.scale2 u)^2 = G.model2 u := by + have hden : G.E.A * -((G.Z * u^2)^2 + G.Z * u^2) ≠ 0 := + mul_ne_zero G.A_nonzero + (neg_ne_zero.mpr (G.ta_ne_zero_of_u_ne_zero hsq hu)) + have hX := G.x1_mul_den hsq hu + unfold x2 scale2 model2 twist2 phiCore + refine mul_left_cancel₀ (pow_ne_zero 3 hden) ?_ + linear_combination ((G.E.A^3 * (G.Z * u^2 + 1)^2)^2 * + ((G.Z * u^2)^3 + * ((G.x1 u * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2)))^2 + + G.x1 u * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2)) + * (G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1)) + + (G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1))^2) + + G.E.A * (G.Z * u^2) + * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2))^2)) * hX + +/-- **The branch dichotomy, in algebraic form**: the curve equation at `x₂ u` +is `(Z·u²)³` times the curve equation at `x₁ u`. The factor +`(Z·u²)³ = Z·(Z·u³)²` is `Z` times a nonzero square for `u ≠ 0`, so exactly +one of the two curve-equation values is a square whenever both are nonzero. -/ +theorem g_x2_eq (hsq : IsSquare (-1 : F)) {u : F} (hu : u ≠ 0) : + (G.x2 u)^3 + G.E.A * G.x2 u + G.E.B + = (G.Z * u^2)^3 * ((G.x1 u)^3 + G.E.A * G.x1 u + G.E.B) := by + have hden : G.E.A * -((G.Z * u^2)^2 + G.Z * u^2) ≠ 0 := + mul_ne_zero G.A_nonzero + (neg_ne_zero.mpr (G.ta_ne_zero_of_u_ne_zero hsq hu)) + have hX := G.x1_mul_den hsq hu + unfold x2 + refine mul_left_cancel₀ (pow_ne_zero 3 hden) ?_ + linear_combination (G.E.A * (G.Z * u^2) + * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2))^2 * (1 - (G.Z * u^2)^2)) * hX + +end ClearedIdentities + +end SSWUParams + +end CompElliptic.Hashing From 2c860ae92120c3c5053db5d2debd1e66da3ea905 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Mon, 17 Aug 2026 23:39:08 +0100 Subject: [PATCH 02/25] feat(Hashing): the covers' point sets and covering maps MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- CompElliptic/Hashing/BranchCovers.lean | 224 +++++++++++++++++++++++++ 1 file changed, 224 insertions(+) diff --git a/CompElliptic/Hashing/BranchCovers.lean b/CompElliptic/Hashing/BranchCovers.lean index afe8dda..b7a590e 100644 --- a/CompElliptic/Hashing/BranchCovers.lean +++ b/CompElliptic/Hashing/BranchCovers.lean @@ -33,10 +33,38 @@ formal consumption of that bound is tracked at On a field where `-1` is a square (both Pasta base fields), `Z·u² + 1` never vanishes (`Zuu_add_one_ne_zero`), so the scalings vanish only at `u = 0` and the models are nonzero wherever `Φ` is. + +`modelPoints1`/`modelPoints2` collect each cover's rational points in model +coordinates, as a `Finset ((F × F) ⊕ Bool)`. `Sum.inl` carries an affine +model point `(u, W)`, so each set holds the affine solutions of +`W² = H_j(u)`. The models have even degree 14, so each smooth model also +has two points at infinity; they are rational —and included, as +`Sum.inr false` and `Sum.inr true`— exactly when the leading square class +`d_j·Z` is a square. + +The `Bool` is a bare tag: the two points at infinity +are the conjugate pair of places over `u = ∞`, swapped by the hyperelliptic +involution, and the formalization fixes no correspondence between the tags +and the places. Only the pair's cardinality and its common image `𝒪` enter +any statement, so every result is invariant under swapping the tags, and +the cited input's faithfulness needs only some bijection — which either +labelling provides. + +`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`; +* everything else goes to `𝒪`: the `u = 0` fibre, the points at infinity, + and junk values off the model. + +On the parameter range the derivation targets (`-A·B` a nonsquare, which +holds at the deployed instantiations) the points at infinity genuinely map +to `𝒪`. The correspondence theorems carry that hypothesis. -/ namespace CompElliptic.Hashing +open Finset CompElliptic.CurveForms.ShortWeierstrass + namespace SSWUParams variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] @@ -199,6 +227,202 @@ theorem g_x2_eq (hsq : IsSquare (-1 : F)) {u : F} (hu : u ≠ 0) : end ClearedIdentities +section ModelPoints + +variable (G : SSWUParams F) + +include G in +/-- A nonsquare exists only in odd characteristic: in characteristic 2 every +element of a finite field is a square, against `Z_nonsquare`. -/ +theorem ringChar_ne_two : ringChar F ≠ 2 := fun h => + G.Z_nonsquare (FiniteField.isSquare_of_char_two h G.Z) + +/-- The first twist constant is nonzero. -/ +theorem twist1_ne_zero : G.twist1 ≠ 0 := by + unfold twist1 + exact neg_ne_zero.mpr (mul_ne_zero (mul_ne_zero (pow_ne_zero 3 G.A_nonzero) + G.E.B_nonzero) (pow_ne_zero 3 G.Z_nonzero)) + +/-- The second twist constant is nonzero. -/ +theorem twist2_ne_zero : G.twist2 ≠ 0 := by + unfold twist2 + exact neg_ne_zero.mpr (mul_ne_zero (pow_ne_zero 3 G.A_nonzero) G.E.B_nonzero) + +/-- The first model never vanishes. At `u = 0` its value is `d₁·B² ≠ 0`. At +`u ≠ 0`, a zero would put the zero-ordinate point `(x₁ u, 0)` on the curve, +which the no-2-torsion hypothesis `hy0` excludes. So the model's rational +points never have `W = 0`: the merged boundary case of the derivation is +empty. -/ +theorem model1_ne_zero (hsq : IsSquare (-1 : F)) + (hy0 : ∀ x : F, ¬ OnCurve G.E.A G.E.B (x, 0)) (u : F) : + G.model1 u ≠ 0 := by + rcases eq_or_ne u 0 with rfl | hu + · rw [G.model1_zero] + exact mul_ne_zero G.twist1_ne_zero (pow_ne_zero 2 G.E.B_nonzero) + · intro h + rcases mul_eq_zero.mp ((G.model1_eq hsq hu).trans h) with hg | hs + · exact hy0 (G.x1 u) (by simpa [OnCurve] using hg.symm) + · exact pow_ne_zero 2 (G.scale1_ne_zero hsq hu) hs + +/-- The second model never vanishes; see `model1_ne_zero`. -/ +theorem model2_ne_zero (hsq : IsSquare (-1 : F)) + (hy0 : ∀ x : F, ¬ OnCurve G.E.A G.E.B (x, 0)) (u : F) : + G.model2 u ≠ 0 := by + rcases eq_or_ne u 0 with rfl | hu + · rw [G.model2_zero] + exact mul_ne_zero G.twist2_ne_zero (pow_ne_zero 2 G.E.B_nonzero) + · intro h + rcases mul_eq_zero.mp ((G.model2_eq hsq hu).trans h) with hg | hs + · exact hy0 (G.x2 u) (by simpa [OnCurve] using hg.symm) + · exact pow_ne_zero 2 (G.scale2_ne_zero hsq u) hs + +/-- The point set of the first cover, in model coordinates: the affine +solutions of `W² = H₁(u)`, plus the two points at infinity —tagged by a +bare `Bool`, since neither has a distinguished coordinate— exactly when +the leading square class `d₁·Z` is a square. -/ +def modelPoints1 : Finset ((F × F) ⊕ Bool) := + ((univ.filter fun p : F × F => p.2^2 = G.model1 p.1).image Sum.inl) + ∪ (if IsSquare (G.twist1 * G.Z) then {Sum.inr false, Sum.inr true} else ∅) + +/-- The point set of the second cover, in model coordinates; see +`modelPoints1`. -/ +def modelPoints2 : Finset ((F × F) ⊕ Bool) := + ((univ.filter fun p : F × F => p.2^2 = G.model2 p.1).image Sum.inl) + ∪ (if IsSquare (G.twist2 * G.Z) then {Sum.inr false, Sum.inr true} else ∅) + +/-- The affine members of the first cover's point set: `(u, W)` is in the +set exactly when it solves the model, `W² = H₁(u)`. -/ +@[simp] theorem mem_modelPoints1_inl {p : F × F} : + Sum.inl p ∈ G.modelPoints1 ↔ p.2^2 = G.model1 p.1 := by + unfold modelPoints1 + simp only [mem_union, mem_image, mem_filter, mem_univ, true_and, + Sum.inl.injEq] + constructor + · rintro (⟨q, hq, rfl⟩ | hbad) + · exact hq + · exfalso; revert hbad; split_ifs <;> simp + · intro hp + exact Or.inl ⟨p, hp, rfl⟩ + +/-- The affine members of the second cover's point set: `(u, W)` is in the +set exactly when it solves the model, `W² = H₂(u)`. -/ +@[simp] theorem mem_modelPoints2_inl {p : F × F} : + Sum.inl p ∈ G.modelPoints2 ↔ p.2^2 = G.model2 p.1 := by + unfold modelPoints2 + simp only [mem_union, mem_image, mem_filter, mem_univ, true_and, + Sum.inl.injEq] + constructor + · rintro (⟨q, hq, rfl⟩ | hbad) + · exact hq + · exfalso; revert hbad; split_ifs <;> simp + · intro hp + exact Or.inl ⟨p, hp, rfl⟩ + +/-- The infinite members of the first cover's point set: both points at +infinity are present exactly when the leading square class `d₁·Z` is a +square. -/ +@[simp] theorem mem_modelPoints1_inr {b : Bool} : + Sum.inr b ∈ G.modelPoints1 ↔ IsSquare (G.twist1 * G.Z) := by + unfold modelPoints1 + simp only [mem_union, mem_image] + constructor + · rintro (⟨q, _, hq⟩ | h) + · exact absurd hq (by simp) + · revert h; split_ifs with hsq <;> intro h + · exact hsq + · simp at h + · intro hsq + refine Or.inr ?_ + rw [if_pos hsq] + rcases b <;> simp + +/-- The infinite members of the second cover's point set: both points at +infinity are present exactly when the leading square class `d₂·Z` is a +square. -/ +@[simp] theorem mem_modelPoints2_inr {b : Bool} : + Sum.inr b ∈ G.modelPoints2 ↔ IsSquare (G.twist2 * G.Z) := by + unfold modelPoints2 + simp only [mem_union, mem_image] + constructor + · rintro (⟨q, _, hq⟩ | h) + · exact absurd hq (by simp) + · revert h; split_ifs with hsq <;> intro h + · exact hsq + · simp at h + · intro hsq + refine Or.inr ?_ + rw [if_pos hsq] + rcases b <;> simp + +/-- The covering map of the first cover, in model coordinates. An affine +model point over `u ≠ 0` goes to the curve point with abscissa `x₁ u` and +ordinate `W / s₁ u`. Everything else goes to `𝒪`: the `u = 0` fibre, the +points at infinity, and junk values off the model. The `𝒪` images are +genuine on the parameter range the correspondence theorems target (`-A·B` +a nonsquare). There this cover's rational boundary points sit over `u = 0`, +where the abscissa has a pole. -/ +def cover1Map (hsq : IsSquare (-1 : F)) : (F × F) ⊕ Bool → SWPoint G.E + | .inl p => + if h : p.1 ≠ 0 ∧ p.2^2 = G.model1 p.1 then + ⟨G.x1 p.1, p.2 / G.scale1 p.1, Or.inl (by + show (p.2 / G.scale1 p.1)^2 = (G.x1 p.1)^3 + G.E.A * G.x1 p.1 + G.E.B + rw [div_pow, h.2, ← G.model1_eq hsq h.1, + mul_div_cancel_right₀ _ (pow_ne_zero 2 (G.scale1_ne_zero hsq h.1))])⟩ + else 0 + | .inr _ => 0 + +/-- The covering map of the second cover; see `cover1Map`. On the targeted +parameter range this cover's rational boundary points are at infinity, where +the abscissa has a pole. -/ +def cover2Map (hsq : IsSquare (-1 : F)) : (F × F) ⊕ Bool → SWPoint G.E + | .inl p => + if h : p.1 ≠ 0 ∧ p.2^2 = G.model2 p.1 then + ⟨G.x2 p.1, p.2 / G.scale2 p.1, Or.inl (by + show (p.2 / G.scale2 p.1)^2 = (G.x2 p.1)^3 + G.E.A * G.x2 p.1 + G.E.B + rw [div_pow, h.2, ← G.model2_eq hsq h.1, + mul_div_cancel_right₀ _ (pow_ne_zero 2 (G.scale2_ne_zero hsq p.1))])⟩ + else 0 + | .inr _ => 0 + +end ModelPoints + end SSWUParams +/-! ## Counting square roots + +The fibre of a model over `u₀` is the solution set of `W² = H(u₀)`; these +helpers count it. In odd characteristic, a nonzero square has exactly the +two roots `±r`, and a nonsquare has none. -/ + +/-- The solutions of `W² = a` for a nonzero `a` with a root `r`: exactly +`{r, -r}`. -/ +theorem filter_sq_eq_pair {F : Type*} [Field F] [Fintype F] [DecidableEq F] + {a r : F} (hr : r^2 = a) : + (univ.filter fun W : F => W^2 = a) = {r, -r} := by + ext W + simp only [mem_filter, mem_univ, true_and, mem_insert, mem_singleton] + rw [← hr, sq_eq_sq_iff_eq_or_eq_neg] + +/-- In odd characteristic, a nonzero square has exactly two square roots. -/ +theorem filter_sq_card_of_isSquare {F : Type*} [Field F] [Fintype F] + [DecidableEq F] {a : F} (hchar : ringChar F ≠ 2) (ha : a ≠ 0) + (hsq : IsSquare a) : + (univ.filter fun W : F => W^2 = a).card = 2 := by + obtain ⟨r, hr⟩ := hsq + have hr2 : r^2 = a := by rw [sq]; exact hr.symm + have hr0 : r ≠ 0 := by + rintro rfl + exact ha (by rw [← hr2]; ring) + rw [filter_sq_eq_pair hr2] + refine card_pair_eq_two_iff.mpr fun h => hr0 ?_ + exact (Ring.eq_self_iff_eq_zero_of_char_ne_two hchar).mp h.symm + +/-- A nonsquare has no square roots. -/ +theorem filter_sq_eq_empty {F : Type*} [Field F] [Fintype F] [DecidableEq F] + {a : F} (hns : ¬ IsSquare a) : + (univ.filter fun W : F => W^2 = a) = ∅ := by + rw [filter_eq_empty_iff] + intro W _ + exact fun hW => hns ⟨W, by rw [← hW]; ring⟩ + end CompElliptic.Hashing From a5085665b2247df200ef6898fe7e7550d6f8087a Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Tue, 18 Aug 2026 00:02:36 +0100 Subject: [PATCH 03/25] feat(Hashing): the fibre over a nonzero input MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- CompElliptic/Hashing/BranchCovers.lean | 195 +++++++++++++++++++++++++ 1 file changed, 195 insertions(+) diff --git a/CompElliptic/Hashing/BranchCovers.lean b/CompElliptic/Hashing/BranchCovers.lean index b7a590e..4c15a3d 100644 --- a/CompElliptic/Hashing/BranchCovers.lean +++ b/CompElliptic/Hashing/BranchCovers.lean @@ -425,4 +425,199 @@ theorem filter_sq_eq_empty {F : Type*} [Field F] [Fintype F] [DecidableEq F] intro W _ exact fun hW => hns ⟨W, by rw [← hW]; ring⟩ +/-- A nonsquare times a nonzero square is a nonsquare. -/ +theorem not_isSquare_mul_sq {F : Type*} [Field F] {z c : F} + (hz : ¬ IsSquare z) (hc : c ≠ 0) : ¬ IsSquare (z * c^2) := by + rintro ⟨t, ht⟩ + refine hz ⟨t/c, ?_⟩ + field_simp + linear_combination ht + +namespace SSWUParams + +/-! ## The fibre over a nonzero input + +Fix `u ≠ 0`. Exactly one branch's curve-equation value `g (x_j u)` is a +nonzero square, and the mapping outputs a point over that branch's abscissa +(`map_x`). On the square branch the model fibre `W² = H_j(u)` has the two +roots `±(map u).y · s_j u`, whose covering-map images are `map u` and +`-(map u)`; on the other branch the fibre is empty. `fibre_sum` packages +this: summed over both covers, any function of the images contributes +exactly `φ (map u) + φ (-(map u))`. -/ + +section FibreSum + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] +variable (G : SSWUParams F) + +/-- The candidate ordinate squares to the curve equation at the output +abscissa: the on-curve fact `onCurve_mapXY`, restated through `map`. -/ +theorem map_y_sq (u : F) : + ((G.map u).y)^2 = ((G.map u).x)^3 + G.E.A * (G.map u).x + G.E.B := + G.onCurve_mapXY u + +/-- **The branch selection.** For `u ≠ 0`, the mapping outputs the branch +whose curve-equation value is a square: the abscissa is `x₁ u` when +`g (x₁ u)` is a square, else `x₂ u`. The square-root split tests exactly +`IsSquare (U / xdiv³)`, and `U / xdiv³ = g (x₁ u)`. -/ +theorem map_x (hsq : IsSquare (-1 : F)) {u : F} (hu : u ≠ 0) : + (G.map u).x + = if IsSquare ((G.x1 u)^3 + G.E.A * G.x1 u + G.E.B) then G.x1 u + else G.x2 u := by + have hta : (G.Z * u^2)^2 + G.Z * u^2 ≠ 0 := G.ta_ne_zero_of_u_ne_zero hsq hu + have hden : G.E.A * -((G.Z * u^2)^2 + G.Z * u^2) ≠ 0 := + mul_ne_zero G.A_nonzero (neg_ne_zero.mpr hta) + have hX := G.x1_mul_den hsq hu + -- The ratio the square-root split tests is the curve equation at `x₁ u`. + have hUdiv : ((G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1))^2 + + G.E.A * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2))^2) + * (G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1)) + + G.E.B * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2))^3 + = ((G.x1 u)^3 + G.E.A * G.x1 u + G.E.B) + * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2))^3 := by + linear_combination (-((G.x1 u * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2)))^2 + + G.x1 u * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2)) + * (G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1)) + + (G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1))^2 + + G.E.A * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2))^2)) * hX + have hbiff : (sqrtRatio G.d G.lam + (((G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1))^2 + + G.E.A * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2))^2) + * (G.E.B * (((G.Z * u^2)^2 + G.Z * u^2) + 1)) + + G.E.B * (G.E.A * -((G.Z * u^2)^2 + G.Z * u^2))^3) + ((G.E.A * -((G.Z * u^2)^2 + G.Z * u^2))^3)).2 = true + ↔ IsSquare ((G.x1 u)^3 + G.E.A * G.x1 u + G.E.B) := by + rw [sqrtRatio_true_iff, hUdiv, + mul_div_cancel_right₀ _ (pow_ne_zero 3 hden)] + show (G.mapXYUpToSign u).1 = _ + simp only [mapXYUpToSign] + rw [if_neg hta] + by_cases hgs : IsSquare ((G.x1 u)^3 + G.E.A * G.x1 u + G.E.B) + · rw [if_pos hgs, hbiff.mpr hgs, if_pos rfl] + rfl + · rw [if_neg hgs, Bool.eq_false_iff.mpr fun h => hgs (hbiff.mp h), + if_neg (by simp)] + unfold x2 x1 + ring + +/-- The first covering map's abscissa at a genuine affine model point. -/ +theorem cover1Map_inl_x (hsq : IsSquare (-1 : F)) {u W : F} (hu : u ≠ 0) + (hW : W^2 = G.model1 u) : + (G.cover1Map hsq (Sum.inl (u, W))).x = G.x1 u := by + simp [cover1Map, hu, hW] + +/-- The first covering map's ordinate at a genuine affine model point. -/ +theorem cover1Map_inl_y (hsq : IsSquare (-1 : F)) {u W : F} (hu : u ≠ 0) + (hW : W^2 = G.model1 u) : + (G.cover1Map hsq (Sum.inl (u, W))).y = W / G.scale1 u := by + simp [cover1Map, hu, hW] + +/-- The second covering map's abscissa at a genuine affine model point. -/ +theorem cover2Map_inl_x (hsq : IsSquare (-1 : F)) {u W : F} (hu : u ≠ 0) + (hW : W^2 = G.model2 u) : + (G.cover2Map hsq (Sum.inl (u, W))).x = G.x2 u := by + simp [cover2Map, hu, hW] + +/-- The second covering map's ordinate at a genuine affine model point. -/ +theorem cover2Map_inl_y (hsq : IsSquare (-1 : F)) {u W : F} (hu : u ≠ 0) + (hW : W^2 = G.model2 u) : + (G.cover2Map hsq (Sum.inl (u, W))).y = W / G.scale2 u := by + simp [cover2Map, hu, hW] + +/-- **The fibre over a nonzero input, summed.** Over `u ≠ 0`, the two +covers' affine model fibres together contribute the images `map u` and +`-(map u)`, each once: the square branch's two roots supply them, and the +other branch's fibre is empty. -/ +theorem fibre_sum (hsq : IsSquare (-1 : F)) + (hy0 : ∀ x : F, ¬ OnCurve G.E.A G.E.B (x, 0)) + {M : Type*} [AddCommMonoid M] (φ : SWPoint G.E → M) {u : F} (hu : u ≠ 0) : + (∑ W ∈ univ.filter fun W : F => W^2 = G.model1 u, + φ (G.cover1Map hsq (Sum.inl (u, W)))) + + (∑ W ∈ univ.filter fun W : F => W^2 = G.model2 u, + φ (G.cover2Map hsq (Sum.inl (u, W)))) + = φ (G.map u) + φ (-(G.map u)) := by + have hchar := G.ringChar_ne_two + have hH1 := G.model1_ne_zero hsq hy0 u + have hH2 := G.model2_ne_zero hsq hy0 u + have hg1 : (G.x1 u)^3 + G.E.A * G.x1 u + G.E.B ≠ 0 := fun h => + hH1 (by rw [← G.model1_eq hsq hu, h, zero_mul]) + have hg2 : (G.x2 u)^3 + G.E.A * G.x2 u + G.E.B ≠ 0 := fun h => + hH2 (by rw [← G.model2_eq hsq hu, h, zero_mul]) + have hu3 : G.Z * u^3 ≠ 0 := mul_ne_zero G.Z_nonzero (pow_ne_zero 3 hu) + by_cases hgs : IsSquare ((G.x1 u)^3 + G.E.A * G.x1 u + G.E.B) + · -- Branch 1 carries the square; branch 2's fibre is empty. + have hx : (G.map u).x = G.x1 u := by rw [G.map_x hsq hu, if_pos hgs] + have hy2 : ((G.map u).y)^2 = (G.x1 u)^3 + G.E.A * G.x1 u + G.E.B := by + rw [← hx]; exact G.map_y_sq u + have hyne : (G.map u).y ≠ 0 := fun h => hg1 (by rw [← hy2, h]; ring) + have hr2 : ((G.map u).y * G.scale1 u)^2 = G.model1 u := by + rw [mul_pow, hy2, G.model1_eq hsq hu] + have hrne : (G.map u).y * G.scale1 u ≠ 0 := + mul_ne_zero hyne (G.scale1_ne_zero hsq hu) + have hns2 : ¬ IsSquare (G.model2 u) := by + obtain ⟨t, ht⟩ := hgs + have ht0 : t ≠ 0 := fun h => hg1 (by rw [ht, h, mul_zero]) + have hM : G.model2 u = G.Z * (G.Z * u^3 * t * G.scale2 u)^2 := by + rw [← G.model2_eq hsq hu, G.g_x2_eq hsq hu, ht]; ring + rw [hM] + exact not_isSquare_mul_sq G.Z_nonsquare + (mul_ne_zero (mul_ne_zero hu3 ht0) (G.scale2_ne_zero hsq u)) + rw [filter_sq_eq_empty hns2, Finset.sum_empty, _root_.add_zero, + filter_sq_eq_pair hr2, Finset.sum_pair fun h => hrne + ((Ring.eq_self_iff_eq_zero_of_char_ne_two hchar).mp h.symm)] + have hP : G.cover1Map hsq (Sum.inl (u, (G.map u).y * G.scale1 u)) + = G.map u := by + refine SWPoint.ext_pair ?_ + rw [G.cover1Map_inl_x hsq hu hr2, G.cover1Map_inl_y hsq hu hr2, hx, + mul_div_cancel_right₀ _ (G.scale1_ne_zero hsq hu)] + have hQ : G.cover1Map hsq (Sum.inl (u, -((G.map u).y * G.scale1 u))) + = -(G.map u) := by + have hr2' : (-((G.map u).y * G.scale1 u))^2 = G.model1 u := by + rw [neg_sq, hr2] + refine SWPoint.ext_pair ?_ + rw [G.cover1Map_inl_x hsq hu hr2', G.cover1Map_inl_y hsq hu hr2', + SWPoint.neg_x, SWPoint.neg_y, hx, neg_div, + mul_div_cancel_right₀ _ (G.scale1_ne_zero hsq hu)] + rw [hP, hQ] + · -- Branch 2 carries the square; branch 1's fibre is empty. + have hZ3 : ¬ IsSquare ((G.Z * u^2)^3) := by + have h : (G.Z * u^2)^3 = G.Z * (G.Z * u^3)^2 := by ring + rw [h] + exact not_isSquare_mul_sq G.Z_nonsquare hu3 + have hgs2 : IsSquare ((G.x2 u)^3 + G.E.A * G.x2 u + G.E.B) := by + rw [G.g_x2_eq hsq hu] + exact isSquare_mul_of_not_isSquare hZ3 hgs + have hx : (G.map u).x = G.x2 u := by rw [G.map_x hsq hu, if_neg hgs] + have hy2 : ((G.map u).y)^2 = (G.x2 u)^3 + G.E.A * G.x2 u + G.E.B := by + rw [← hx]; exact G.map_y_sq u + have hyne : (G.map u).y ≠ 0 := fun h => hg2 (by rw [← hy2, h]; ring) + have hr2 : ((G.map u).y * G.scale2 u)^2 = G.model2 u := by + rw [mul_pow, hy2, G.model2_eq hsq hu] + have hrne : (G.map u).y * G.scale2 u ≠ 0 := + mul_ne_zero hyne (G.scale2_ne_zero hsq u) + have hns1 : ¬ IsSquare (G.model1 u) := by + rw [← G.model1_eq hsq hu] + exact not_isSquare_mul_sq hgs (G.scale1_ne_zero hsq hu) + rw [filter_sq_eq_empty hns1, Finset.sum_empty, _root_.zero_add, + filter_sq_eq_pair hr2, Finset.sum_pair fun h => hrne + ((Ring.eq_self_iff_eq_zero_of_char_ne_two hchar).mp h.symm)] + have hP : G.cover2Map hsq (Sum.inl (u, (G.map u).y * G.scale2 u)) + = G.map u := by + refine SWPoint.ext_pair ?_ + rw [G.cover2Map_inl_x hsq hu hr2, G.cover2Map_inl_y hsq hu hr2, hx, + mul_div_cancel_right₀ _ (G.scale2_ne_zero hsq u)] + have hQ : G.cover2Map hsq (Sum.inl (u, -((G.map u).y * G.scale2 u))) + = -(G.map u) := by + have hr2' : (-((G.map u).y * G.scale2 u))^2 = G.model2 u := by + rw [neg_sq, hr2] + refine SWPoint.ext_pair ?_ + rw [G.cover2Map_inl_x hsq hu hr2', G.cover2Map_inl_y hsq hu hr2', + SWPoint.neg_x, SWPoint.neg_y, hx, neg_div, + mul_div_cancel_right₀ _ (G.scale2_ne_zero hsq u)] + rw [hP, hQ] + +end FibreSum + +end SSWUParams + end CompElliptic.Hashing From ac84e2a5a280de536c0e8a9acd01fd67f82fab24 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Tue, 18 Aug 2026 00:09:13 +0100 Subject: [PATCH 04/25] feat(Hashing): the covers' sums with the boundary bookkeeping MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- CompElliptic/Hashing/BranchCovers.lean | 114 +++++++++++++++++++++++++ 1 file changed, 114 insertions(+) diff --git a/CompElliptic/Hashing/BranchCovers.lean b/CompElliptic/Hashing/BranchCovers.lean index 4c15a3d..66cce4e 100644 --- a/CompElliptic/Hashing/BranchCovers.lean +++ b/CompElliptic/Hashing/BranchCovers.lean @@ -433,6 +433,16 @@ theorem not_isSquare_mul_sq {F : Type*} [Field F] {z c : F} field_simp linear_combination ht +/-- A sum over a filtered product, decomposed into a double sum: outer over +the first component, inner over the filter at that component. -/ +theorem sum_filter_prod {α β M : Type*} [Fintype α] [Fintype β] + [DecidableEq α] [DecidableEq β] [AddCommMonoid M] + (P : α → β → Prop) [∀ a b, Decidable (P a b)] (f : α × β → M) : + ∑ p ∈ (univ : Finset (α × β)).filter fun p => P p.1 p.2, f p + = ∑ a, ∑ b ∈ univ.filter fun b => P a b, f (a, b) := by + rw [Finset.sum_filter, Fintype.sum_prod_type] + exact Finset.sum_congr rfl fun a _ => (Finset.sum_filter _ _).symm + namespace SSWUParams /-! ## The fibre over a nonzero input @@ -616,6 +626,110 @@ theorem fibre_sum (hsq : IsSquare (-1 : F)) mul_div_cancel_right₀ _ (G.scale2_ne_zero hsq u)] rw [hP, hQ] +/-- **The covers, summed, with the boundary bookkeeping.** On the parameter +range with `-A·B` a nonsquare, + +`S₁ + S₂ = Σ_{u ≠ 0} (φ (map u) + φ (-(map u))) + 4·φ 𝒪`, + +where `S_j` sums `φ` of the covering-map images over the full point set of +cover `j`, for any `φ` into a commutative additive monoid. The boundary +supplies the `4·φ 𝒪`: +* cover 1 has no points at infinity, and its `u = 0` fibre is a rational + pair mapping to `𝒪`; +* cover 2 has an empty `u = 0` fibre, and its rational pair at infinity + maps to `𝒪`. -/ +theorem modelPoints_sum (hsq : IsSquare (-1 : F)) + (hy0 : ∀ x : F, ¬ OnCurve G.E.A G.E.B (x, 0)) + (hAB : ¬ IsSquare (-(G.E.A * G.E.B))) + {M : Type*} [AddCommMonoid M] (φ : SWPoint G.E → M) : + (∑ P ∈ G.modelPoints1, φ (G.cover1Map hsq P)) + + (∑ P ∈ G.modelPoints2, φ (G.cover2Map hsq P)) + = (∑ u ∈ (univ : Finset F).erase 0, + (φ (G.map u) + φ (-(G.map u)))) + 4 • φ 0 := by + have hchar := G.ringChar_ne_two + -- The boundary square classes, under `-A·B` nonsquare: + -- cover 1 has no rational points at infinity … + have hT1 : ¬ IsSquare (G.twist1 * G.Z) := by + have h : G.twist1 * G.Z = -(G.E.A * G.E.B) * (G.E.A * G.Z^2)^2 := by + unfold twist1; ring + rw [h] + exact not_isSquare_mul_sq hAB + (mul_ne_zero G.A_nonzero (pow_ne_zero 2 G.Z_nonzero)) + -- … cover 2 does … + have hT2 : IsSquare (G.twist2 * G.Z) := by + obtain ⟨r, hr⟩ := isSquare_mul_of_not_isSquare hAB G.Z_nonsquare + refine ⟨r * G.E.A, ?_⟩ + unfold twist2 + linear_combination (G.E.A^2) * hr + -- … cover 1's `u = 0` fibre is inhabited … + have h10 : IsSquare (G.model1 0) := by + rw [G.model1_zero] + obtain ⟨r, hr⟩ := isSquare_mul_of_not_isSquare hAB G.Z_nonsquare + refine ⟨r * (G.E.A * G.Z) * G.E.B, ?_⟩ + unfold twist1 + linear_combination (G.E.A^2 * G.Z^2 * G.E.B^2) * hr + -- … and cover 2's is empty. + have h20 : ¬ IsSquare (G.model2 0) := by + rw [G.model2_zero] + have h : G.twist2 * G.E.B^2 = -(G.E.A * G.E.B) * (G.E.A * G.E.B)^2 := by + unfold twist2; ring + rw [h] + exact not_isSquare_mul_sq hAB (mul_ne_zero G.A_nonzero G.E.B_nonzero) + -- Decompose the point-set sums into affine double sums and the boundary. + have hs1 : ∑ P ∈ G.modelPoints1, φ (G.cover1Map hsq P) + = ∑ u, ∑ W ∈ univ.filter fun W : F => W^2 = G.model1 u, + φ (G.cover1Map hsq (Sum.inl (u, W))) := by + unfold modelPoints1 + rw [if_neg hT1, Finset.union_empty, + Finset.sum_image fun _ _ _ _ h => Sum.inl.inj h, + sum_filter_prod (fun u W => W^2 = G.model1 u) + (fun p => φ (G.cover1Map hsq (Sum.inl p)))] + have hs2 : ∑ P ∈ G.modelPoints2, φ (G.cover2Map hsq P) + = (∑ u, ∑ W ∈ univ.filter fun W : F => W^2 = G.model2 u, + φ (G.cover2Map hsq (Sum.inl (u, W)))) + (φ 0 + φ 0) := by + unfold modelPoints2 + rw [if_pos hT2, Finset.sum_union (by simp [Finset.disjoint_left]), + Finset.sum_image fun _ _ _ _ h => Sum.inl.inj h, + Finset.sum_insert (by simp), Finset.sum_singleton, + sum_filter_prod (fun u W => W^2 = G.model2 u) + (fun p => φ (G.cover2Map hsq (Sum.inl p)))] + simp [cover2Map] + -- The `u = 0` inner sums: two `𝒪`-images on cover 1, none on cover 2. + have hA0 : ∑ W ∈ univ.filter fun W : F => W^2 = G.model1 0, + φ (G.cover1Map hsq (Sum.inl (0, W))) = 2 • φ 0 := by + calc ∑ W ∈ univ.filter fun W : F => W^2 = G.model1 0, + φ (G.cover1Map hsq (Sum.inl (0, W))) + = ∑ _W ∈ univ.filter fun W : F => W^2 = G.model1 0, φ 0 := + Finset.sum_congr rfl fun W _ => by simp [cover1Map] + _ = ((univ.filter fun W : F => W^2 = G.model1 0).card) • φ 0 := + Finset.sum_const _ + _ = 2 • φ 0 := by + rw [filter_sq_card_of_isSquare hchar + (G.model1_ne_zero hsq hy0 0) h10] + have hB0 : ∑ W ∈ univ.filter fun W : F => W^2 = G.model2 0, + φ (G.cover2Map hsq (Sum.inl (0, W))) = 0 := by + rw [filter_sq_eq_empty h20, Finset.sum_empty] + -- Assemble: split `u = 0` off both outer sums and merge the rest. + rw [hs1, hs2, + ← Finset.add_sum_erase _ _ (mem_univ (0 : F)), + ← Finset.add_sum_erase _ + (fun u => ∑ W ∈ univ.filter fun W : F => W^2 = G.model2 u, + φ (G.cover2Map hsq (Sum.inl (u, W)))) (mem_univ (0 : F)), + hA0, hB0] + have hmerge : (∑ u ∈ (univ : Finset F).erase 0, + ∑ W ∈ univ.filter fun W : F => W^2 = G.model1 u, + φ (G.cover1Map hsq (Sum.inl (u, W)))) + + (∑ u ∈ (univ : Finset F).erase 0, + ∑ W ∈ univ.filter fun W : F => W^2 = G.model2 u, + φ (G.cover2Map hsq (Sum.inl (u, W)))) + = ∑ u ∈ (univ : Finset F).erase 0, + (φ (G.map u) + φ (-(G.map u))) := by + rw [← Finset.sum_add_distrib] + exact Finset.sum_congr rfl fun u hu => + G.fibre_sum hsq hy0 φ (Finset.mem_erase.mp hu).1 + rw [← hmerge] + abel + end FibreSum end SSWUParams From d64b4727f811449985f867c254b618bf90dd24c9 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Tue, 18 Aug 2026 00:16:38 +0100 Subject: [PATCH 05/25] feat(Hashing): WeilBounded from the Weil input at the branch covers MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- CompElliptic.lean | 1 + CompElliptic/Hashing/WeilInstance.lean | 142 +++++++++++++++++++++++++ 2 files changed, 143 insertions(+) create mode 100644 CompElliptic/Hashing/WeilInstance.lean diff --git a/CompElliptic.lean b/CompElliptic.lean index f72357d..90e3a84 100644 --- a/CompElliptic.lean +++ b/CompElliptic.lean @@ -25,5 +25,6 @@ import CompElliptic.Hashing.PastaSSWU import CompElliptic.Hashing.SignedLift import CompElliptic.Hashing.SimplifiedSWU import CompElliptic.Hashing.TwoTermUniformity +import CompElliptic.Hashing.WeilInstance import CompElliptic.Hashing.WellDistributed import CompElliptic.TrustBoundary diff --git a/CompElliptic/Hashing/WeilInstance.lean b/CompElliptic/Hashing/WeilInstance.lean new file mode 100644 index 0000000..c2e2279 --- /dev/null +++ b/CompElliptic/Hashing/WeilInstance.lean @@ -0,0 +1,142 @@ +/- +Copyright (c) 2026 CompElliptic Contributors. +Released under the Apache License, Version 2.0, or the MIT license, at your option, +as described in the files LICENSE-APACHE and LICENSE-MIT. +Authors: Daira-Emma Hopwood +-/ +import CompElliptic.Hashing.BranchCovers +import CompElliptic.Hashing.WellDistributed + +/-! +# The Weil input at the branch covers + +This file states the shape in which Weil's theorem enters the formalization, +and derives `WeilBounded` for the zero-repaired mapping from it. + +`CharSumBounded s h B` says every nontrivial character of the target group +sums to at most `B` on the images of the point set `s` under `h`, in squared +norm. Weil's theorem — in the form of FFSTV's Lemma 1 and Theorem 3 +() — bounds such a sum over a genus-`g̃` +covering of an elliptic curve by `(2·g̃ - 2)·√q`, provided the covering does +not factor through a nontrivial unramified subcover. The branch covers have +genus 6, and their total ramification over `A·x + B = 0` rules every +unramified subcover out; both derivations are cited from +`design/weil-constant-derivation.md` §2–3, because even their statements +need machinery absent from Mathlib (genus, places, covers). So the intended +instantiations take `B = 100·#F`, the squared form of `10·√q` with +`10 = 2·6 - 2`; this hypothesis is the cited boundary. Progress is tracked +at . + +`cover_charSum` is the sign-free assembly (design doc §4): for every +character `ψ`, + +`S₁(ψ) + S₂(ψ) = 2·S(ψ) + 2`, + +where `S_j` sums `ψ` over cover `j`'s images and `S` sums it over the +zero-repaired mapping's outputs. `weilBounded_zeroRepaired` combines the +assembly with the two cover bounds and exact square-free arithmetic: + +`‖S(ψ)‖² ≤ (21/2)²·#F` for every nontrivial `ψ`, + +that is, `WeilBounded (zeroRepaired G.map) (21/2)`, on any field with +`#F ≥ 44` where `-1` is a square, `-A·B` is a nonsquare, the curve has no +2-torsion, and the sign function is genuine. +-/ + +namespace CompElliptic.Hashing + +open Finset CompElliptic.CurveForms.ShortWeierstrass + +/-- A squared character-sum bound over a finite point set: every nontrivial +character of the target group sums to at most `B` on the images, in squared +norm. Weil's theorem supplies such bounds for the rational points of curve +coverings, with `B = ((2·g̃ - 2))²·q` for a genus-`g̃` covering over a field +of size `q`; see the module docstring. -/ +def CharSumBounded {ι G' : Type*} [AddCommGroup G'] (s : Finset ι) + (h : ι → G') (B : ℝ) : Prop := + ∀ ψ : AddChar G' ℂ, ψ ≠ 1 → ‖∑ P ∈ s, ψ (h P)‖^2 ≤ B + +namespace SSWUParams + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] +variable (G : SSWUParams F) + +/-- **The sign-free assembly** (design doc §4): for every character `ψ` of +the curve group, the two covers' character sums combine to + +`S₁(ψ) + S₂(ψ) = 2·S(ψ) + 2`, + +with `S(ψ)` the character sum of the zero-repaired mapping. Negating the +input permutes the nonzero inputs and negates the output, so the two +per-input images `±(map u)` sum to twice the mapping's character sum; the +four boundary points contribute `ψ 𝒪 = 1` each, and the repaired `u = 0` +input supplies the `-2` that turns `+ 4` into `+ 2`. -/ +theorem cover_charSum (hsq : IsSquare (-1 : F)) + (hy0 : ∀ x : F, ¬ OnCurve G.E.A G.E.B (x, 0)) + (hAB : ¬ IsSquare (-(G.E.A * G.E.B))) (hsgn : IsSignFunction G.sgn) + (ψ : AddChar (SWPoint G.E) ℂ) : + (∑ P ∈ G.modelPoints1, ψ (G.cover1Map hsq P)) + + (∑ P ∈ G.modelPoints2, ψ (G.cover2Map hsq P)) + = 2 * (∑ u, ψ (zeroRepaired G.map u)) + 2 := by + rw [G.modelPoints_sum hsq hy0 hAB (fun P => ψ P), Finset.sum_add_distrib] + have hneg : (∑ u ∈ (univ : Finset F).erase 0, ψ (-(G.map u))) + = ∑ u ∈ (univ : Finset F).erase 0, ψ (G.map u) := by + refine Finset.sum_equiv (Equiv.neg F) (fun u => ?_) (fun u hu => ?_) + · simp [Finset.mem_erase] + · simp only [Equiv.neg_apply, + G.map_neg hsgn (Finset.mem_erase.mp hu).1] + have hfull : (∑ u, ψ (zeroRepaired G.map u)) + = 1 + ∑ u ∈ (univ : Finset F).erase 0, ψ (G.map u) := by + rw [← Finset.add_sum_erase _ _ (mem_univ (0 : F))] + congr 1 + · simp [zeroRepaired] + · exact Finset.sum_congr rfl fun u hu => by + simp [zeroRepaired, (Finset.mem_erase.mp hu).1] + rw [hneg, hfull, AddChar.map_zero_eq_one] + push_cast + ring + +/-- **`WeilBounded` from the two cover bounds.** Weil's theorem at the two +branch covers —`CharSumBounded` at `100·#F`, the squared `(2·6 - 2)·√q` of +the genus-6 coverings— yields the deployed Weil bound + +`‖S(ψ)‖² ≤ (21/2)²·#F` + +for the zero-repaired mapping. The margin between the additive-constant +sharp `10·√q + 1` and the recorded `(21/2)·√q` absorbs the boundary terms +once `#F ≥ 44`; the arithmetic stays square-root-free throughout. -/ +theorem weilBounded_zeroRepaired (hsq : IsSquare (-1 : F)) + (hy0 : ∀ x : F, ¬ OnCurve G.E.A G.E.B (x, 0)) + (hAB : ¬ IsSquare (-(G.E.A * G.E.B))) (hsgn : IsSignFunction G.sgn) + (hq : (44 : ℕ) ≤ Fintype.card F) + (h1 : CharSumBounded G.modelPoints1 (G.cover1Map hsq) + (100 * (Fintype.card F : ℝ))) + (h2 : CharSumBounded G.modelPoints2 (G.cover2Map hsq) + (100 * (Fintype.card F : ℝ))) : + WeilBounded (zeroRepaired G.map) (21/2) := by + intro ψ hψ + have hid := G.cover_charSum hsq hy0 hAB hsgn ψ + have ha := h1 ψ hψ + have hb := h2 ψ hψ + set S := ∑ u, ψ (zeroRepaired G.map u) with hS + set S₁ := ∑ P ∈ G.modelPoints1, ψ (G.cover1Map hsq P) with hS₁ + set S₂ := ∑ P ∈ G.modelPoints2, ψ (G.cover2Map hsq P) with hS₂ + have hnorm : 2 * ‖S‖ ≤ ‖S₁‖ + ‖S₂‖ + 2 := by + calc 2 * ‖S‖ = ‖(2 : ℂ) * S‖ := by + rw [norm_mul, RCLike.norm_ofNat] + _ = ‖S₁ + S₂ - 2‖ := by rw [show (2 : ℂ) * S = S₁ + S₂ - 2 from by + linear_combination -hid] + _ ≤ ‖S₁ + S₂‖ + ‖(2 : ℂ)‖ := norm_sub_le _ _ + _ ≤ (‖S₁‖ + ‖S₂‖) + 2 := by + rw [RCLike.norm_ofNat] + gcongr + exact norm_add_le _ _ + have hq' : (44 : ℝ) ≤ (Fintype.card F : ℝ) := by exact_mod_cast hq + have h4 : 4 * ‖S‖^2 ≤ (‖S₁‖ + ‖S₂‖ + 2)^2 := by + nlinarith [hnorm, norm_nonneg S, norm_nonneg S₁, norm_nonneg S₂] + nlinarith [h4, ha, hb, hq', norm_nonneg S₁, norm_nonneg S₂, + sq_nonneg (‖S₁‖ - ‖S₂‖), sq_nonneg (‖S₁‖ + ‖S₂‖ - 20)] + +end SSWUParams + +end CompElliptic.Hashing From 3cd693e7826604a33d113880c651692dd5d53268 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Tue, 18 Aug 2026 02:10:41 +0100 Subject: [PATCH 06/25] feat(Hashing): the deployed Weil bounds for Pallas and Vesta MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- CompElliptic/Hashing/PastaSSWU.lean | 87 +++++++++++++++++++++++ CompElliptic/Hashing/WeilInstance.lean | 1 - CompElliptic/Hashing/WellDistributed.lean | 16 +++++ 3 files changed, 103 insertions(+), 1 deletion(-) diff --git a/CompElliptic/Hashing/PastaSSWU.lean b/CompElliptic/Hashing/PastaSSWU.lean index 03d9abe..8af94b2 100644 --- a/CompElliptic/Hashing/PastaSSWU.lean +++ b/CompElliptic/Hashing/PastaSSWU.lean @@ -10,6 +10,7 @@ import CompElliptic.Curves.PastaOrder import CompElliptic.Hashing.SimplifiedSWU import CompElliptic.Hashing.SignedLift import CompElliptic.Hashing.FibreBound +import CompElliptic.Hashing.WeilInstance import Mathlib.Tactic.ReduceModChar /-! @@ -184,6 +185,49 @@ theorem norm_charSum_mapToCurve_sub_zeroRepaired (ψ : AddChar (SWPoint curve) ‖∑ u, ψ (mapToCurve u) - ∑ u, ψ (zeroRepaired mapToCurve u)‖ ≤ 2 := norm_charSum_sub_zeroRepaired mapToCurve ψ +/-- `-A·B` for iso-Pallas is a quadratic non-residue, by Euler's criterion +with the power evaluated by fast modular exponentiation. This puts the +deployed instantiation in the branch of the boundary bookkeeping where all +four extra cover points map to `𝒪`; it is the same fact as the emptiness of +the `w = 0` fibre that `weilbound.sage` checks. -/ +theorem neg_AB_not_isSquare : + ¬ IsSquare (-(isoCurve.A * isoCurve.B) : PallasBaseField) := by + have h : (-(isoCurve.A * isoCurve.B) : PallasBaseField) + = 0x20ac6f47c8ff2fb79b416dfa18151f9498e4983c291cb11f8c10b822901f9e44 := by + decide + rw [h, ZMod.euler_criterion PALLAS_BASE_CARD (by decide : + (0x20ac6f47c8ff2fb79b416dfa18151f9498e4983c291cb11f8c10b822901f9e44 + : PallasBaseField) ≠ 0)] + reduce_mod_char + decide + +/-- **The deployed Weil bound for the Pallas mapping.** Weil's theorem at +the two branch covers of iso-Pallas —the `CharSumBounded` inputs at +`100·#F`; see `Hashing/WeilInstance.lean`— gives +`WeilBounded (zeroRepaired mapToCurve)` at the recorded constant `21/2`. +The bound crosses the 3-isogeny because the isogeny is a bijective +homomorphism on rational points, so characters pull back along it. -/ +theorem weilBounded_zeroRepaired_mapToCurve + (h1 : CharSumBounded sswu.modelPoints1 (sswu.cover1Map isSquare_neg_one) + (100 * (Fintype.card PallasBaseField : ℝ))) + (h2 : CharSumBounded sswu.modelPoints2 (sswu.cover2Map isSquare_neg_one) + (100 * (Fintype.card PallasBaseField : ℝ))) : + WeilBounded (zeroRepaired mapToCurve) (21/2) := by + have hbase := sswu.weilBounded_zeroRepaired isSquare_neg_one + iso_no_onCurve_y_zero neg_AB_not_isSquare isSignFunction_sgn0 + (by rw [ZMod.card]; decide) h1 h2 + have hcomp := hbase.comp (AddMonoidHom.mk' iso.map iso_map_add) + iso_map_bijective + have hfun : (fun u => (AddMonoidHom.mk' iso.map iso_map_add) + (zeroRepaired sswu.map u)) = zeroRepaired mapToCurve := by + funext u + rcases eq_or_ne u 0 with rfl | hu + · exact ((congrArg (AddMonoidHom.mk' iso.map iso_map_add) + (if_pos rfl)).trans (map_zero _)).trans (if_pos rfl).symm + · simp [zeroRepaired, hu, mapToCurve] + rw [← hfun] + exact hcomp + /-- The deployed hash-to-curve construction for Pallas after `hash_to_field`: add on the iso-curve, apply the isogeny once. -/ def mapHashOutputsToCurve (u₀ u₁ : PallasBaseField) : SWPoint curve := @@ -371,6 +415,49 @@ theorem norm_charSum_mapToCurve_sub_zeroRepaired (ψ : AddChar (SWPoint curve) ‖∑ u, ψ (mapToCurve u) - ∑ u, ψ (zeroRepaired mapToCurve u)‖ ≤ 2 := norm_charSum_sub_zeroRepaired mapToCurve ψ +/-- `-A·B` for iso-Vesta is a quadratic non-residue, by Euler's criterion +with the power evaluated by fast modular exponentiation. This puts the +deployed instantiation in the branch of the boundary bookkeeping where all +four extra cover points map to `𝒪`; it is the same fact as the emptiness of +the `w = 0` fibre that `weilbound.sage` checks. -/ +theorem neg_AB_not_isSquare : + ¬ IsSquare (-(isoCurve.A * isoCurve.B) : VestaBaseField) := by + have h : (-(isoCurve.A * isoCurve.B) : VestaBaseField) + = 0x3722d4398ccc606a2c8a49902dbae3b72c59d02c5890bd61eb2e37c567e5258 := by + decide + rw [h, ZMod.euler_criterion PALLAS_SCALAR_CARD (by decide : + (0x3722d4398ccc606a2c8a49902dbae3b72c59d02c5890bd61eb2e37c567e5258 + : VestaBaseField) ≠ 0)] + reduce_mod_char + decide + +/-- **The deployed Weil bound for the Vesta mapping.** Weil's theorem at +the two branch covers of iso-Vesta —the `CharSumBounded` inputs at +`100·#F`; see `Hashing/WeilInstance.lean`— gives +`WeilBounded (zeroRepaired mapToCurve)` at the recorded constant `21/2`. +The bound crosses the 3-isogeny because the isogeny is a bijective +homomorphism on rational points, so characters pull back along it. -/ +theorem weilBounded_zeroRepaired_mapToCurve + (h1 : CharSumBounded sswu.modelPoints1 (sswu.cover1Map isSquare_neg_one) + (100 * (Fintype.card VestaBaseField : ℝ))) + (h2 : CharSumBounded sswu.modelPoints2 (sswu.cover2Map isSquare_neg_one) + (100 * (Fintype.card VestaBaseField : ℝ))) : + WeilBounded (zeroRepaired mapToCurve) (21/2) := by + have hbase := sswu.weilBounded_zeroRepaired isSquare_neg_one + iso_no_onCurve_y_zero neg_AB_not_isSquare isSignFunction_sgn0 + (by rw [ZMod.card]; decide) h1 h2 + have hcomp := hbase.comp (AddMonoidHom.mk' iso.map iso_map_add) + iso_map_bijective + have hfun : (fun u => (AddMonoidHom.mk' iso.map iso_map_add) + (zeroRepaired sswu.map u)) = zeroRepaired mapToCurve := by + funext u + rcases eq_or_ne u 0 with rfl | hu + · exact ((congrArg (AddMonoidHom.mk' iso.map iso_map_add) + (if_pos rfl)).trans (map_zero _)).trans (if_pos rfl).symm + · simp [zeroRepaired, hu, mapToCurve] + rw [← hfun] + exact hcomp + /-- The deployed hash-to-curve construction for Vesta after `hash_to_field`: add on the iso-curve, apply the isogeny once. -/ def mapHashOutputsToCurve (u₀ u₁ : VestaBaseField) : SWPoint curve := diff --git a/CompElliptic/Hashing/WeilInstance.lean b/CompElliptic/Hashing/WeilInstance.lean index c2e2279..6389377 100644 --- a/CompElliptic/Hashing/WeilInstance.lean +++ b/CompElliptic/Hashing/WeilInstance.lean @@ -93,7 +93,6 @@ theorem cover_charSum (hsq : IsSquare (-1 : F)) · exact Finset.sum_congr rfl fun u hu => by simp [zeroRepaired, (Finset.mem_erase.mp hu).1] rw [hneg, hfull, AddChar.map_zero_eq_one] - push_cast ring /-- **`WeilBounded` from the two cover bounds.** Weil's theorem at the two diff --git a/CompElliptic/Hashing/WellDistributed.lean b/CompElliptic/Hashing/WellDistributed.lean index 09198b3..ddca2a9 100644 --- a/CompElliptic/Hashing/WellDistributed.lean +++ b/CompElliptic/Hashing/WellDistributed.lean @@ -140,4 +140,20 @@ theorem WeilBounded.deviation {f : F → G} {C : ℝ} (h : WeilBounded f C) ‖∑ Q, ((mult f Q : ℂ) - 1) * ψ Q‖^2 ≤ C^2 * (Fintype.card F : ℝ) := by rw [← charSum_eq hψ]; exact h ψ hψ +omit [AddCommGroup F] [DecidableEq F] [Fintype G] [DecidableEq G] in +/-- The Weil bound transfers along a bijective homomorphism of the target +group. Characters of the new target pull back along the homomorphism; +surjectivity keeps nontrivial characters nontrivial, and the pulled-back +sum is the original one. This is what carries the bound across the deployed +isogeny, which is bijective on rational points. -/ +theorem WeilBounded.comp {G' : Type*} [AddCommGroup G'] [Fintype G'] + [DecidableEq G'] {f : F → G} {C : ℝ} (h : WeilBounded f C) (e : G →+ G') + (he : Function.Bijective e) : WeilBounded (fun u => e (f u)) C := by + intro ψ hψ + have hone : (1 : AddChar G' ℂ).compAddMonoidHom e = 1 := by + ext a; simp + have hne : ψ.compAddMonoidHom e ≠ 1 := fun hc => + hψ (AddChar.compAddMonoidHom_injective_left e he.2 (hc.trans hone.symm)) + simpa using h (ψ.compAddMonoidHom e) hne + end CompElliptic.Hashing From 16204b08d3ce7456d20ec63ee176d7c6c0b71772 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Tue, 18 Aug 2026 02:46:19 +0100 Subject: [PATCH 07/25] refactor(Hashing): parameterize the per-cover Weil constant MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- CompElliptic/Hashing/PastaSSWU.lean | 24 ++++++++- CompElliptic/Hashing/WeilInstance.lean | 73 +++++++++++++++++--------- 2 files changed, 70 insertions(+), 27 deletions(-) diff --git a/CompElliptic/Hashing/PastaSSWU.lean b/CompElliptic/Hashing/PastaSSWU.lean index 8af94b2..b68f6ce 100644 --- a/CompElliptic/Hashing/PastaSSWU.lean +++ b/CompElliptic/Hashing/PastaSSWU.lean @@ -213,9 +213,19 @@ theorem weilBounded_zeroRepaired_mapToCurve (h2 : CharSumBounded sswu.modelPoints2 (sswu.cover2Map isSquare_neg_one) (100 * (Fintype.card PallasBaseField : ℝ))) : WeilBounded (zeroRepaired mapToCurve) (21/2) := by + rw [show (21/2 : ℝ) = 10 + 1/2 from by norm_num] + have h1' : CharSumBounded sswu.modelPoints1 (sswu.cover1Map isSquare_neg_one) + ((10 : ℝ)^2 * (Fintype.card PallasBaseField : ℝ)) := by + rw [show ((10 : ℝ)^2) = 100 from by norm_num] + exact h1 + have h2' : CharSumBounded sswu.modelPoints2 (sswu.cover2Map isSquare_neg_one) + ((10 : ℝ)^2 * (Fintype.card PallasBaseField : ℝ)) := by + rw [show ((10 : ℝ)^2) = 100 from by norm_num] + exact h2 have hbase := sswu.weilBounded_zeroRepaired isSquare_neg_one iso_no_onCurve_y_zero neg_AB_not_isSquare isSignFunction_sgn0 - (by rw [ZMod.card]; decide) h1 h2 + (by norm_num : (0 : ℝ) < 10) + (by rw [ZMod.card]; norm_num) h1' h2' have hcomp := hbase.comp (AddMonoidHom.mk' iso.map iso_map_add) iso_map_bijective have hfun : (fun u => (AddMonoidHom.mk' iso.map iso_map_add) @@ -443,9 +453,19 @@ theorem weilBounded_zeroRepaired_mapToCurve (h2 : CharSumBounded sswu.modelPoints2 (sswu.cover2Map isSquare_neg_one) (100 * (Fintype.card VestaBaseField : ℝ))) : WeilBounded (zeroRepaired mapToCurve) (21/2) := by + rw [show (21/2 : ℝ) = 10 + 1/2 from by norm_num] + have h1' : CharSumBounded sswu.modelPoints1 (sswu.cover1Map isSquare_neg_one) + ((10 : ℝ)^2 * (Fintype.card VestaBaseField : ℝ)) := by + rw [show ((10 : ℝ)^2) = 100 from by norm_num] + exact h1 + have h2' : CharSumBounded sswu.modelPoints2 (sswu.cover2Map isSquare_neg_one) + ((10 : ℝ)^2 * (Fintype.card VestaBaseField : ℝ)) := by + rw [show ((10 : ℝ)^2) = 100 from by norm_num] + exact h2 have hbase := sswu.weilBounded_zeroRepaired isSquare_neg_one iso_no_onCurve_y_zero neg_AB_not_isSquare isSignFunction_sgn0 - (by rw [ZMod.card]; decide) h1 h2 + (by norm_num : (0 : ℝ) < 10) + (by rw [ZMod.card]; norm_num) h1' h2' have hcomp := hbase.comp (AddMonoidHom.mk' iso.map iso_map_add) iso_map_bijective have hfun : (fun u => (AddMonoidHom.mk' iso.map iso_map_add) diff --git a/CompElliptic/Hashing/WeilInstance.lean b/CompElliptic/Hashing/WeilInstance.lean index 6389377..83c23f1 100644 --- a/CompElliptic/Hashing/WeilInstance.lean +++ b/CompElliptic/Hashing/WeilInstance.lean @@ -21,11 +21,27 @@ covering of an elliptic curve by `(2·g̃ - 2)·√q`, provided the covering doe not factor through a nontrivial unramified subcover. The branch covers have genus 6, and their total ramification over `A·x + B = 0` rules every unramified subcover out; both derivations are cited from -`design/weil-constant-derivation.md` §2–3, because even their statements -need machinery absent from Mathlib (genus, places, covers). So the intended -instantiations take `B = 100·#F`, the squared form of `10·√q` with -`10 = 2·6 - 2`; this hypothesis is the cited boundary. Progress is tracked -at . +`design/weil-constant-derivation.md` §2–3. Mathlib does not yet have the +vocabulary to state them (genus, places, covers of curves), and that +vocabulary is out of scope for +, which covers +formalizing the computation and the paper proof's supporting facts; the +vocabulary itself, on the Riemann's-inequality route, is +. + +The derivation is parametric in the per-cover constant `c`: inputs at +`c²·#F`, conclusion at `c + 1/2`. The parameter exists because the cited +constant depends on which genus fact the citation uses, and the two +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, *Algebraic Function Fields and Codes*, 2nd ed., +§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. `cover_charSum` is the sign-free assembly (design doc §4): for every character `ψ`, @@ -36,11 +52,12 @@ where `S_j` sums `ψ` over cover `j`'s images and `S` sums it over the zero-repaired mapping's outputs. `weilBounded_zeroRepaired` combines the assembly with the two cover bounds and exact square-free arithmetic: -`‖S(ψ)‖² ≤ (21/2)²·#F` for every nontrivial `ψ`, +`‖S(ψ)‖² ≤ (c + 1/2)²·#F` for every nontrivial `ψ`, -that is, `WeilBounded (zeroRepaired G.map) (21/2)`, on any field with -`#F ≥ 44` where `-1` is a square, `-A·B` is a nonsquare, the curve has no -2-torsion, and the sign function is genuine. +that is, `WeilBounded (zeroRepaired G.map) (c + 1/2)`, on any field with +`#F ≥ 4·c + 4` where `-1` is a square, `-A·B` is a nonsquare, the curve +has no 2-torsion, and the sign function is genuine. The deployed +instantiations take `c = 10`, so `21/2` and `#F ≥ 44`. -/ namespace CompElliptic.Hashing @@ -95,24 +112,25 @@ theorem cover_charSum (hsq : IsSquare (-1 : F)) rw [hneg, hfull, AddChar.map_zero_eq_one] ring -/-- **`WeilBounded` from the two cover bounds.** Weil's theorem at the two -branch covers —`CharSumBounded` at `100·#F`, the squared `(2·6 - 2)·√q` of -the genus-6 coverings— yields the deployed Weil bound - -`‖S(ψ)‖² ≤ (21/2)²·#F` - -for the zero-repaired mapping. The margin between the additive-constant -sharp `10·√q + 1` and the recorded `(21/2)·√q` absorbs the boundary terms -once `#F ≥ 44`; the arithmetic stays square-root-free throughout. -/ +/-- **`WeilBounded` from the two cover bounds, parametrically in the +constant.** For a per-cover constant `c > 0`: if both covers' character +sums are bounded by `c²·#F` in squared norm, the zero-repaired mapping is +Weil-bounded at `c + 1/2`, on any field with `#F ≥ 4·c + 4`. The extra +half absorbs the assembly's boundary terms, square-root-free; its size is +conventional, not forced — the sharp bound is `c·√#F + 1`, so any positive +slack would do at a matching field-size threshold. A half is a round +choice whose cost is invisible at the deployed sizes; the recorded +deployed constant `21/2` is the same convention at `c = 10`. The module +docstring records why `c` is a parameter. -/ theorem weilBounded_zeroRepaired (hsq : IsSquare (-1 : F)) (hy0 : ∀ x : F, ¬ OnCurve G.E.A G.E.B (x, 0)) (hAB : ¬ IsSquare (-(G.E.A * G.E.B))) (hsgn : IsSignFunction G.sgn) - (hq : (44 : ℕ) ≤ Fintype.card F) + {c : ℝ} (hc : 0 < c) (hq : 4*c + 4 ≤ (Fintype.card F : ℝ)) (h1 : CharSumBounded G.modelPoints1 (G.cover1Map hsq) - (100 * (Fintype.card F : ℝ))) + (c^2 * (Fintype.card F : ℝ))) (h2 : CharSumBounded G.modelPoints2 (G.cover2Map hsq) - (100 * (Fintype.card F : ℝ))) : - WeilBounded (zeroRepaired G.map) (21/2) := by + (c^2 * (Fintype.card F : ℝ))) : + WeilBounded (zeroRepaired G.map) (c + 1/2) := by intro ψ hψ have hid := G.cover_charSum hsq hy0 hAB hsgn ψ have ha := h1 ψ hψ @@ -130,11 +148,16 @@ theorem weilBounded_zeroRepaired (hsq : IsSquare (-1 : F)) rw [RCLike.norm_ofNat] gcongr exact norm_add_le _ _ - have hq' : (44 : ℝ) ≤ (Fintype.card F : ℝ) := by exact_mod_cast hq have h4 : 4 * ‖S‖^2 ≤ (‖S₁‖ + ‖S₂‖ + 2)^2 := by nlinarith [hnorm, norm_nonneg S, norm_nonneg S₁, norm_nonneg S₂] - nlinarith [h4, ha, hb, hq', norm_nonneg S₁, norm_nonneg S₂, - sq_nonneg (‖S₁‖ - ‖S₂‖), sq_nonneg (‖S₁‖ + ‖S₂‖ - 20)] + -- The linear term: `4·(‖S₁‖ + ‖S₂‖) + 4 ≤ (4·c + 1)·#F`. + have hlin : 4 * (‖S₁‖ + ‖S₂‖) + 4 ≤ (4*c + 1) * (Fintype.card F : ℝ) := by + nlinarith [ha, hb, hc, sq_nonneg (‖S₁‖ - ‖S₂‖), + sq_nonneg (‖S₁‖ + ‖S₂‖ - 2*c), + mul_nonneg hc.le (sub_nonneg.mpr hq), + norm_nonneg S₁, norm_nonneg S₂] + nlinarith [h4, hlin, ha, hb, sq_nonneg (‖S₁‖ - ‖S₂‖), norm_nonneg S₁, + norm_nonneg S₂] end SSWUParams From c1910652223da5c69b1f6bae10c8969d6dddd182 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Tue, 18 Aug 2026 18:37:02 +0100 Subject: [PATCH 08/25] feat(Hashing): the supporting facts for the Weil derivation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- CompElliptic.lean | 1 + CompElliptic/Hashing/WeilSupport.lean | 480 ++++++++++++++++++++++++++ 2 files changed, 481 insertions(+) create mode 100644 CompElliptic/Hashing/WeilSupport.lean diff --git a/CompElliptic.lean b/CompElliptic.lean index 90e3a84..3922c20 100644 --- a/CompElliptic.lean +++ b/CompElliptic.lean @@ -26,5 +26,6 @@ import CompElliptic.Hashing.SignedLift import CompElliptic.Hashing.SimplifiedSWU import CompElliptic.Hashing.TwoTermUniformity import CompElliptic.Hashing.WeilInstance +import CompElliptic.Hashing.WeilSupport import CompElliptic.Hashing.WellDistributed import CompElliptic.TrustBoundary diff --git a/CompElliptic/Hashing/WeilSupport.lean b/CompElliptic/Hashing/WeilSupport.lean new file mode 100644 index 0000000..ff82906 --- /dev/null +++ b/CompElliptic/Hashing/WeilSupport.lean @@ -0,0 +1,480 @@ +/- +Copyright (c) 2026 CompElliptic Contributors. +Released under the Apache License, Version 2.0, or the MIT license, at your option, +as described in the files LICENSE-APACHE and LICENSE-MIT. +Authors: Daira-Emma Hopwood +-/ +import CompElliptic.Hashing.BranchCovers +import Mathlib.FieldTheory.Separable +import Mathlib.RingTheory.Polynomial.Eisenstein.Basic + +/-! +# Supporting facts for the Weil-constant derivation + +The cited steps of `design/weil-constant-derivation.md` —the genus of the +branch covers (§2) and their total ramification (§3)— cannot be stated in +Lean without vocabulary Mathlib does not yet have. Their *inputs* can. This +file proves those inputs, so that the paper proof's checkable algebra is +machine-checked and only the two genuinely geometric steps remain cited +(; the vocabulary itself +is ). + +The genus computation (§2) consumes: +* `phiPoly_squarefree` — the core `Φ` is squarefree, by the design doc's + own argument: `Φ = φ ∘ ta` for the cubic `φ` (`phiPoly_eq_comp`), `φ` is + separable (`phiCubic_separable`, by a Bézout certificate whose constant + is `A³·B²·(4·A³ + 27·B²)` —exactly the standing nonzero quantities—), + and `Φ` is coprime to each factor of `ta′`; +* `phiPoly_natDegree` and the model degrees — `Φ` has degree 12, and the + models `H_j` degree 14 with squarefreeness (`model1Poly_squarefree`, + `model2Poly_squarefree`), which is what the hyperelliptic genus formula + `g = ⌊(14 - 1)/2⌋ = 6` is applied to (Galbraith, *Mathematics of Public + Key Cryptography*, ch. 10; Stichtenoth, *Algebraic Function Fields and + Codes*, 2nd ed., ch. 6). + +The ramification argument (§3) consumes: +* `p2Poly_isEisensteinAt` and `p1RecipPoly_isEisensteinAt` — the branch + quartics over `F[w]` satisfy the classical Eisenstein irreducibility + criterion (`Polynomial.IsEisensteinAt`) at the ideal `(w)`; +* `eval_g_neg_B_div_A` — `g(-B/A) = -(B/A)³ ≠ 0` (this is why `w` is a + uniformizer at both points over `w = 0`). + +The Eisenstein criterion is that the leading coefficient lies outside the +ideal, every lower coefficient lies inside it, and the constant coefficient +lies outside its square. The cited total-ramification argument relies on +this criterion's transplant to places of function fields (Stichtenoth, +*Algebraic Function Fields and Codes*, 2nd ed., ch. 3; design doc, +Background). The transplant is a statement about any discrete valuation on +the coefficient field — it instantiates the criterion rather than being a +new theorem. Its hypotheses force the polynomial's Newton polygon to be a +single segment from `(0, 1)` to `(n, 0)`, so every root has valuation `1/n` +(Milne, *Algebraic Number Theory*, course notes, ch. 7, Prop. 7.44 — +stated there for characteristic zero, but the argument is +characteristic-free). This yields irreducibility and ramification index +`n` —total ramification— at once. The classical form instantiates this at +`ℤ` localized at a prime; the function-field form instantiates it at the +local ring of a place of the base curve, a uniformizer standing in for +the prime — here `w` itself, by `g_neg_B_div_A_ne_zero`. Our statements +check the coefficient pattern at the polynomial ring `F[w]`; the passage +to the valuation at the two places is part of the cited step. + +Everything here is stated over the polynomial rings `F[u]` and `(F[w])[u]`; +the connection from these inputs to genus 6 and to the no-unramified-subcover +condition is the cited part. +-/ + +namespace CompElliptic.Hashing + +open Polynomial + +/-- A Bézout identity with a nonzero constant right-hand side witnesses +coprimality: divide through by the constant. -/ +theorem isCoprime_of_bezout {F : Type*} [Field F] {p q u v : Polynomial F} + {c : F} (hc : c ≠ 0) (h : u*p + v*q = C c) : IsCoprime p q := by + refine ⟨C c⁻¹ * u, C c⁻¹ * v, ?_⟩ + calc C c⁻¹ * u * p + C c⁻¹ * v * q = C c⁻¹ * (u*p + v*q) := by ring + _ = 1 := by rw [h, ← C_mul, inv_mul_cancel₀ hc, C_1] + +namespace SSWUParams + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] +variable (G : SSWUParams F) + +/-! ## The core `Φ` as a polynomial, and its cubic factor through `ta` -/ + +/-- The cubic `φ(T) = B²·(T + 1)³ + A³·T²` through which the core factors: +`Φ = φ ∘ ta` (design doc §2, the squarefreeness lemma). -/ +noncomputable def phiCubic : Polynomial F := + (C G.E.B)^2 * (X + 1)^3 + (C G.E.A)^3 * X^2 + +/-- The core `Φ(u) = B²·(ta + 1)³ + A³·ta²` as a polynomial in `u` +(`phiCore` is its evaluation). -/ +noncomputable def phiPoly : Polynomial F := + (C G.E.B)^2 * (G.taPoly + 1)^3 + (C G.E.A)^3 * G.taPoly^2 + +/-- `Φ` factors through `ta`: `Φ = φ ∘ ta`. -/ +theorem phiPoly_eq_comp : G.phiPoly = G.phiCubic.comp G.taPoly := by + simp only [phiPoly, phiCubic, add_comp, mul_comp, pow_comp, C_comp, X_comp, + one_comp] + +/-- `phiPoly` evaluates to the pointwise core `phiCore`. -/ +theorem eval_phiPoly (u : F) : G.phiPoly.eval u = G.phiCore u := by + simp only [phiPoly, phiCore, taPoly, tPoly, eval_add, eval_mul, eval_pow, + eval_C, eval_X, eval_one] + +/-- `Φ` has degree exactly 12; its leading coefficient is `B²·Z⁶`. -/ +theorem phiPoly_natDegree : G.phiPoly.natDegree = 12 := by + rw [phiPoly, taPoly, tPoly] + compute_degree! + exact ⟨G.E.B_nonzero, G.Z_nonzero⟩ + +/-! ## Separability of the cubic, by Bézout certificate + +The cofactors were computed by `xgcd` in `scripts/weil-derivation-checks.sage`; +the identity's constant is `A³·B²·(4·A³ + 27·B²)`, nonzero exactly from the +standing assumptions plus ellipticity. -/ + +/-- The derivative of the cubic `φ`. -/ +theorem phiCubic_derivative : + G.phiCubic.derivative = 3*(C G.E.B)^2 * (X + 1)^2 + 2*(C G.E.A)^3 * X := by + simp only [phiCubic, derivative_add, derivative_mul, derivative_pow, + derivative_C, derivative_X, derivative_one, Nat.cast_ofNat, map_ofNat] + ring + +/-- **The cubic `φ` is separable**, by the Bézout certificate +`s·φ + t·φ′ = A³·B²·(4·A³ + 27·B²)` computed in +`scripts/weil-derivation-checks.sage`: the identity's constant is a product +of exactly the standing nonzero quantities. -/ +theorem phiCubic_separable (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : + G.phiCubic.Separable := by + refine isCoprime_of_bezout + (u := (6*(C G.E.A)^3*(C G.E.B)^2 + 36*(C G.E.B)^4) * X + + (4*(C G.E.A)^6 + 36*(C G.E.A)^3*(C G.E.B)^2 + 63*(C G.E.B)^4)) + (v := -((2*(C G.E.A)^3*(C G.E.B)^2 + 12*(C G.E.B)^4) * X^2) + - (2*(C G.E.A)^6 + 18*(C G.E.A)^3*(C G.E.B)^2 + 33*(C G.E.B)^4) * X + - (3*(C G.E.A)^3*(C G.E.B)^2 + 21*(C G.E.B)^4)) + (c := G.E.A^3 * G.E.B^2 * (4*G.E.A^3 + 27*G.E.B^2)) + (mul_ne_zero (mul_ne_zero (pow_ne_zero 3 G.A_nonzero) + (pow_ne_zero 2 G.E.B_nonzero)) hdisc) ?_ + have hC : (C (G.E.A^3 * G.E.B^2 * (4*G.E.A^3 + 27*G.E.B^2)) : Polynomial F) + = (C G.E.A)^3 * (C G.E.B)^2 * (4*(C G.E.A)^3 + 27*(C G.E.B)^2) := by + simp only [map_mul, map_pow, map_add, map_ofNat] + rw [phiCubic_derivative, phiCubic, hC] + ring + +/-! ## `Φ` is coprime to the factors of `ta′` -/ + +/-- The derivative of `ta` factors as `(2·Z·X)·(2·Z·X² + 1)` — the critical +points of `ta` are `u = 0` and the locus `Z·u² = -1/2`. -/ +theorem taPoly_derivative : + G.taPoly.derivative = (2 * C G.Z * X) * (2 * C G.Z * X^2 + 1) := by + simp only [taPoly, tPoly, derivative_add, derivative_mul, derivative_pow, + derivative_C, derivative_X, Nat.cast_ofNat, map_ofNat] + ring + +/-- A polynomial with nonzero constant coefficient is coprime to `X`. -/ +theorem _root_.CompElliptic.Hashing.isCoprime_X_of_coeff_zero + {F : Type*} [Field F] {p : Polynomial F} (h : p.coeff 0 ≠ 0) : + IsCoprime p X := by + refine isCoprime_of_bezout (u := 1) (v := -p.divX) (c := p.coeff 0) h ?_ + linear_combination -(X_mul_divX_add p) + +/-- Nonzero constants are coprime to everything. -/ +theorem _root_.CompElliptic.Hashing.isCoprime_C_of_ne_zero + {F : Type*} [Field F] {p : Polynomial F} {c : F} (hc : c ≠ 0) : + IsCoprime p (C c) := + ⟨0, C c⁻¹, by simp [← C_mul, inv_mul_cancel₀ hc]⟩ + +/-- `Φ` has constant coefficient `B²`: it is coprime to `X`. This is the +design doc's `φ(ta(0)) = B² ≠ 0` case of the squarefreeness lemma. -/ +theorem phiPoly_coeff_zero : G.phiPoly.coeff 0 = G.E.B^2 := by + rw [coeff_zero_eq_eval_zero, G.eval_phiPoly, G.phiCore_zero] + +/-- The even-powers polynomial `Ψ` with `64·Φ = Ψ(2·Z·X² + 1)`: the core, +re-expanded around the second critical locus of `ta`. Its constant term is +the ellipticity `4·A³ + 27·B²` — the design doc's `64·φ(-1/4)`. -/ +noncomputable def psiPoly : Polynomial F := + (C G.E.B)^2 * X^6 + (4*(C G.E.A)^3 + 9*(C G.E.B)^2) * X^4 + + (27*(C G.E.B)^2 - 8*(C G.E.A)^3) * X^2 + + (4*(C G.E.A)^3 + 27*(C G.E.B)^2) + +/-- `Ψ`'s constant coefficient is the ellipticity. -/ +theorem psiPoly_coeff_zero : + G.psiPoly.coeff 0 = 4*G.E.A^3 + 27*G.E.B^2 := by + rw [coeff_zero_eq_eval_zero] + simp [psiPoly] + +/-- The re-expansion `64·Φ = Ψ(2·Z·X² + 1)`, checked symbolically in +`scripts/weil-derivation-checks.sage`. -/ +theorem phiPoly_64_eq : + 64 * G.phiPoly = G.psiPoly.comp (2 * C G.Z * X^2 + 1) := by + simp only [psiPoly, phiPoly, taPoly, tPoly, add_comp, mul_comp, pow_comp, + sub_comp, C_comp, X_comp, ofNat_comp, Nat.cast_ofNat] + ring + +/-- `Φ` is coprime to `2·Z·X² + 1`: modulo that factor, `64·Φ` is the +nonzero constant `4·A³ + 27·B²`. This is the design doc's `ta = -1/4` case +of the squarefreeness lemma. -/ +theorem phiPoly_isCoprime_snd (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : + IsCoprime G.phiPoly (2 * C G.Z * X^2 + 1) := by + refine isCoprime_of_bezout (u := 64) + (v := -(G.psiPoly.divX.comp (2 * C G.Z * X^2 + 1))) + (c := 4*G.E.A^3 + 27*G.E.B^2) hdisc ?_ + have h := X_mul_divX_add G.psiPoly + rw [G.psiPoly_coeff_zero] at h + have hcomp : G.psiPoly.comp (2 * C G.Z * X^2 + 1) + = (2 * C G.Z * X^2 + 1) * G.psiPoly.divX.comp (2 * C G.Z * X^2 + 1) + + C (4*G.E.A^3 + 27*G.E.B^2) := by + conv_lhs => rw [← h] + simp only [add_comp, mul_comp, X_comp, C_comp] + calc 64 * G.phiPoly + -(G.psiPoly.divX.comp (2 * C G.Z * X^2 + 1)) + * (2 * C G.Z * X^2 + 1) + = G.psiPoly.comp (2 * C G.Z * X^2 + 1) + - (2 * C G.Z * X^2 + 1) * G.psiPoly.divX.comp (2 * C G.Z * X^2 + 1) + := by rw [G.phiPoly_64_eq]; ring + _ = C (4*G.E.A^3 + 27*G.E.B^2) := by rw [hcomp]; ring + +/-! ## `Φ` is squarefree -/ + +/-- **`Φ` is separable**: its derivative is `(φ′ ∘ ta)·ta′` by the chain +rule, `φ′ ∘ ta` is coprime to `Φ = φ ∘ ta` because the cubic's Bézout +certificate transports along composition, and each factor of `ta′` is +handled by the two critical-value cases. This is the design doc's +squarefreeness lemma (§2), step for step. -/ +theorem phiPoly_separable (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : + G.phiPoly.Separable := by + have h2 : (2 : F) ≠ 0 := Ring.two_ne_zero G.ringChar_ne_two + rw [Polynomial.separable_def, G.phiPoly_eq_comp, derivative_comp, + taPoly_derivative, ← G.phiPoly_eq_comp] + refine IsCoprime.mul_right (IsCoprime.mul_right ?_ ?_) ?_ + · -- `2·Z·X`: a nonzero constant times `X`, and `Φ(0) = B² ≠ 0`. + have hconst : (2 : Polynomial F) * C G.Z = C (2 * G.Z) := by + rw [C_mul, map_ofNat] + rw [hconst] + exact IsCoprime.mul_right + (isCoprime_C_of_ne_zero (mul_ne_zero h2 G.Z_nonzero)) + (isCoprime_X_of_coeff_zero (by + rw [G.phiPoly_coeff_zero] + exact pow_ne_zero 2 G.E.B_nonzero)) + · exact G.phiPoly_isCoprime_snd hdisc + · -- `φ′ ∘ ta`, by transporting the cubic's certificate along `comp ta`. + rw [G.phiPoly_eq_comp] + exact IsCoprime.map (G.phiCubic_separable hdisc) + (eval₂RingHom (C : F →+* Polynomial F) G.taPoly) + +/-- **`Φ` is squarefree** — the input the cited hyperelliptic genus formula +consumes (design doc §2). -/ +theorem phiPoly_squarefree (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : + Squarefree G.phiPoly := + (G.phiPoly_separable hdisc).squarefree + +/-! ## The models: squarefree of degree 14 + +`H_j = d_j·(Z·u²+1)·Φ` — the objects the cited hyperelliptic genus formula +is applied to. -/ + +/-- The first model `H₁ = d₁·(Z·u²+1)·Φ` as a polynomial in `u`. -/ +noncomputable def model1Poly : Polynomial F := + C G.twist1 * ((G.tPoly + 1) * G.phiPoly) + +/-- The second model `H₂ = d₂·(Z·u²+1)·Φ` as a polynomial in `u`. -/ +noncomputable def model2Poly : Polynomial F := + C G.twist2 * ((G.tPoly + 1) * G.phiPoly) + +/-- `model1Poly` evaluates to the pointwise model `model1`. -/ +theorem eval_model1Poly (u : F) : G.model1Poly.eval u = G.model1 u := by + simp only [model1Poly, model1, tPoly, eval_mul, eval_add, eval_C, eval_X, + eval_pow, eval_one, G.eval_phiPoly] + ring + +/-- `model2Poly` evaluates to the pointwise model `model2`. -/ +theorem eval_model2Poly (u : F) : G.model2Poly.eval u = G.model2 u := by + simp only [model2Poly, model2, tPoly, eval_mul, eval_add, eval_C, eval_X, + eval_pow, eval_one, G.eval_phiPoly] + ring + +/-- `Z·X² + 1` is separable: its Bézout certificate against its derivative +`2·Z·X` has the constant `2`. -/ +theorem tPoly_add_one_separable : (G.tPoly + 1).Separable := by + have h2 : (2 : F) ≠ 0 := Ring.two_ne_zero G.ringChar_ne_two + have hd : (G.tPoly + 1).derivative = 2 * C G.Z * X := by + simp only [tPoly, derivative_add, derivative_mul, derivative_pow, + derivative_C, derivative_X, derivative_one, Nat.cast_ofNat, map_ofNat] + ring + rw [Polynomial.separable_def, hd] + refine isCoprime_of_bezout (u := 2) (v := -X) (c := 2) h2 ?_ + have hC2 : (C (2 : F) : Polynomial F) = 2 := map_ofNat _ 2 + rw [tPoly, hC2] + ring + +/-- `Φ` is coprime to `Z·X² + 1`: modulo that factor, `ta = 0` and +`Φ = B²`. This is the design doc's coprimality of `Φ` with the models' +quadratic factor. -/ +theorem phiPoly_isCoprime_tPoly_add_one : + IsCoprime G.phiPoly (G.tPoly + 1) := by + refine isCoprime_of_bezout (u := 1) + (v := -(G.tPoly * ((C G.E.B)^2 * G.taPoly^2 + + (3*(C G.E.B)^2 + (C G.E.A)^3) * G.taPoly + 3*(C G.E.B)^2))) + (c := G.E.B^2) (pow_ne_zero 2 G.E.B_nonzero) ?_ + have hC : (C (G.E.B^2) : Polynomial F) = (C G.E.B)^2 := map_pow _ _ _ + rw [hC, phiPoly, taPoly, tPoly] + ring + +/-- **The first model is squarefree**: a unit times the product of the two +coprime separable factors `Z·X² + 1` and `Φ`. -/ +theorem model1Poly_squarefree (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : + Squarefree G.model1Poly := by + refine Polynomial.Separable.squarefree ?_ + rw [model1Poly] + have hunit : IsUnit (C G.twist1) := isUnit_C.mpr G.twist1_ne_zero.isUnit + refine Polynomial.Separable.mul ((separable_C _).mpr G.twist1_ne_zero.isUnit) + (Polynomial.Separable.mul G.tPoly_add_one_separable + (G.phiPoly_separable hdisc) + ((G.phiPoly_isCoprime_tPoly_add_one).symm)) ?_ + exact (isCoprime_C_of_ne_zero G.twist1_ne_zero).symm + +/-- **The second model is squarefree**; see `model1Poly_squarefree`. -/ +theorem model2Poly_squarefree (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : + Squarefree G.model2Poly := by + refine Polynomial.Separable.squarefree ?_ + rw [model2Poly] + refine Polynomial.Separable.mul ((separable_C _).mpr G.twist2_ne_zero.isUnit) + (Polynomial.Separable.mul G.tPoly_add_one_separable + (G.phiPoly_separable hdisc) + ((G.phiPoly_isCoprime_tPoly_add_one).symm)) ?_ + exact (isCoprime_C_of_ne_zero G.twist2_ne_zero).symm + +/-- **The first model has degree 14** — with squarefreeness, the input to +the cited genus formula `g = ⌊(14 - 1)/2⌋ = 6` (Galbraith ch. 10; +Stichtenoth ch. 6). -/ +theorem model1Poly_natDegree : G.model1Poly.natDegree = 14 := by + rw [model1Poly, phiPoly, taPoly, tPoly] + compute_degree! + repeat' constructor + all_goals first + | exact G.E.B_nonzero + | exact G.Z_nonzero + | exact G.twist1_ne_zero + +/-- **The second model has degree 14**; see `model1Poly_natDegree`. -/ +theorem model2Poly_natDegree : G.model2Poly.natDegree = 14 := by + rw [model2Poly, phiPoly, taPoly, tPoly] + compute_degree! + repeat' constructor + all_goals first + | exact G.E.B_nonzero + | exact G.Z_nonzero + | exact G.twist2_ne_zero + +/-! ## The branch quartics are Eisenstein at `w = 0` + +The design doc's §3 works over the function field of the curve, where `w` +vanishes simply at the two points over `w = 0` (because +`g(-B/A) = -(B/A)³ ≠ 0`). The checkable input is the Eisenstein coefficient +pattern of the quartics over `F[w]`, at the ideal `(w)`; the step from the +pattern to total ramification —and from there to the absence of unramified +subcovers— is the cited part. -/ + +/-- The second branch quartic `P₂ = B·Z²·u⁴ + Z·w·u² + w`, over `F[w]` +(the inner variable is `w`, the outer `u`). -/ +noncomputable def p2Poly : Polynomial (Polynomial F) := + C (C (G.E.B * G.Z^2)) * X^4 + C (C G.Z * X) * X^2 + C (X : Polynomial F) + +/-- The reciprocal of the first branch quartic: +`B·u⁴ + Z·w·u² + Z²·w`. -/ +noncomputable def p1RecipPoly : Polynomial (Polynomial F) := + C (C G.E.B) * X^4 + C (C G.Z * X) * X^2 + C (C (G.Z^2) * X) + +/-- `P₂` has degree 4. -/ +theorem p2Poly_natDegree : G.p2Poly.natDegree = 4 := by + rw [p2Poly] + compute_degree! + exact ⟨G.E.B_nonzero, G.Z_nonzero⟩ + +/-- The reciprocal quartic has degree 4. -/ +theorem p1RecipPoly_natDegree : G.p1RecipPoly.natDegree = 4 := by + rw [p1RecipPoly] + compute_degree! + exact G.E.B_nonzero + +/-- Coefficients of `P₂`, by direct computation. -/ +theorem p2Poly_coeff : + G.p2Poly.coeff 0 = (X : Polynomial F) ∧ G.p2Poly.coeff 1 = 0 + ∧ G.p2Poly.coeff 2 = C G.Z * X ∧ G.p2Poly.coeff 3 = 0 + ∧ G.p2Poly.coeff 4 = C (G.E.B * G.Z^2) := by + refine ⟨?_, ?_, ?_, ?_, ?_⟩ <;> + · simp only [p2Poly, coeff_add, coeff_C_mul, coeff_X_pow, coeff_C] + norm_num + +/-- Coefficients of the reciprocal quartic, by direct computation. -/ +theorem p1RecipPoly_coeff : + G.p1RecipPoly.coeff 0 = C (G.Z^2) * X ∧ G.p1RecipPoly.coeff 1 = 0 + ∧ G.p1RecipPoly.coeff 2 = C G.Z * X ∧ G.p1RecipPoly.coeff 3 = 0 + ∧ G.p1RecipPoly.coeff 4 = C G.E.B := by + refine ⟨?_, ?_, ?_, ?_, ?_⟩ <;> + · simp only [p1RecipPoly, coeff_add, coeff_C_mul, coeff_X_pow, coeff_C] + norm_num + +/-- `X² ∤ c·X` in `F[w]` for a nonzero constant `c`: degree comparison. -/ +theorem _root_.CompElliptic.Hashing.not_X_sq_dvd {F : Type*} [Field F] + {c : Polynomial F} (hc : c ≠ 0) + (hdeg : c.natDegree = 0) : ¬ (X:Polynomial F)^2 ∣ c * X := by + intro hdvd + have hne : c * (X:Polynomial F) ≠ 0 := + mul_ne_zero hc X_ne_zero + have := Polynomial.natDegree_le_of_dvd hdvd hne + rw [natDegree_mul hc X_ne_zero, hdeg, natDegree_X, natDegree_pow, + natDegree_X] at this + omega + +/-- **`P₂` is Eisenstein at `(w)`** — the checkable input to the cited +total-ramification argument over the two points with `w = 0` (design doc +§3). Concretely: the leading coefficient `B·Z²` is not divisible by `w`, +the lower coefficients `w`, `0`, `Z·w`, `0` all are, and the constant +coefficient `w` is not divisible by `w²`. -/ +theorem p2Poly_isEisensteinAt : + G.p2Poly.IsEisensteinAt (Ideal.span {(X : Polynomial F)}) := by + obtain ⟨h0, h1, h2, h3, h4⟩ := G.p2Poly_coeff + have hdeg := G.p2Poly_natDegree + constructor + · -- The leading coefficient `B·Z²` is a unit, not in `(w)`. + rw [Polynomial.leadingCoeff, hdeg, h4, Ideal.mem_span_singleton, + X_dvd_iff, coeff_C] + exact fun h => G.E.B_nonzero (by + rcases mul_eq_zero.mp h with hB | hZ + · exact hB + · exact absurd hZ (pow_ne_zero 2 G.Z_nonzero)) + · -- Every lower coefficient is divisible by `w`. + intro n hn + rw [hdeg] at hn + interval_cases n <;> + simp [h0, h1, h2, h3, Ideal.mem_span_singleton, dvd_mul_left] + · -- The constant coefficient `w` is not in `(w)²`. + rw [h0, Ideal.span_singleton_pow, Ideal.mem_span_singleton] + intro hdvd + have := Polynomial.natDegree_le_of_dvd hdvd X_ne_zero + rw [natDegree_pow, natDegree_X] at this + omega + +/-- **The reciprocal of `P₁` is Eisenstein at `(w)`**; with +`p2Poly_isEisensteinAt`, both covers are totally ramified over `w = 0` in +the cited argument. -/ +theorem p1RecipPoly_isEisensteinAt : + G.p1RecipPoly.IsEisensteinAt (Ideal.span {(X : Polynomial F)}) := by + obtain ⟨h0, h1, h2, h3, h4⟩ := G.p1RecipPoly_coeff + have hdeg := G.p1RecipPoly_natDegree + constructor + · rw [Polynomial.leadingCoeff, hdeg, h4, Ideal.mem_span_singleton, + X_dvd_iff, coeff_C] + exact G.E.B_nonzero + · intro n hn + rw [hdeg] at hn + interval_cases n <;> + simp [h0, h1, h2, h3, Ideal.mem_span_singleton, dvd_mul_left] + · rw [h0, Ideal.span_singleton_pow, Ideal.mem_span_singleton] + exact not_X_sq_dvd (C_ne_zero.mpr (pow_ne_zero 2 G.Z_nonzero)) + (natDegree_C _) + +/-! ## The fibre over `w = 0` -/ + +/-- `g(-B/A) = -(B/A)³`: the curve equation at the abscissa of the two +points over `w = 0`. -/ +theorem eval_g_neg_B_div_A : + (-(G.E.B/G.E.A))^3 + G.E.A * -(G.E.B/G.E.A) + G.E.B + = -(G.E.B/G.E.A)^3 := by + have hA := G.A_nonzero + field_simp + ring + +/-- `g(-B/A) ≠ 0`: the two points over `w = 0` have nonzero ordinate, so +`w` vanishes simply at each — the input that makes the Eisenstein pattern +mean total ramification in the cited argument. -/ +theorem g_neg_B_div_A_ne_zero : + (-(G.E.B/G.E.A))^3 + G.E.A * -(G.E.B/G.E.A) + G.E.B ≠ 0 := by + rw [G.eval_g_neg_B_div_A] + exact neg_ne_zero.mpr (pow_ne_zero 3 + (div_ne_zero G.E.B_nonzero G.A_nonzero)) + +end SSWUParams + +end CompElliptic.Hashing From 0a8e05fd302650389b8a3c20f0092e208be31a4b Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Tue, 18 Aug 2026 18:48:38 +0100 Subject: [PATCH 09/25] meta: weave the supporting-fact references and enforce them MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- .github/workflows/ci.yml | 10 ++++ design/weil-constant-derivation.md | 81 +++++++++++++++++++++-------- scripts/check_weil_support_refs.py | 42 +++++++++++++++ scripts/weil-derivation-checks.sage | 14 +++++ 4 files changed, 126 insertions(+), 21 deletions(-) create mode 100755 scripts/check_weil_support_refs.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6153a11..47756db 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -108,6 +108,16 @@ jobs: - name: Check the precompiled lane's import closure run: scripts/check_native_lane.sh + weil-support-refs: + name: design doc lists the Weil supporting facts exactly + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 + with: + persist-credentials: false + - name: Check the supporting-facts listing against WeilSupport.lean + run: scripts/check_weil_support_refs.py + csimp-census: name: csimp lemmas are axiom-censused runs-on: ubuntu-latest diff --git a/design/weil-constant-derivation.md b/design/weil-constant-derivation.md index 37ba871..1abe54c 100644 --- a/design/weil-constant-derivation.md +++ b/design/weil-constant-derivation.md @@ -19,9 +19,15 @@ and Theorem 3, and the standard point bookkeeping for hyperelliptic models [Galbraith, ch. 10]. The symbolic identities it relies on are checked by `scripts/weil-derivation-checks.sage`; the per-instance facts (the empty w = 0 fibre, the Frobenius statistics, the -square-class witnesses) by `weilbound.sage`. It is not machine-checked; -formalizing the calculation in Lean is what remains of #28 — Weil's -theorem itself stays a cited input. +square-class witnesses) by `weilbound.sage`. The calculation from the +per-cover Weil inputs to the deployed constants is machine-checked +(CompElliptic's `Hashing/BranchCovers.lean`, `Hashing/WeilInstance.lean`, +and `Hashing/PastaSSWU.lean`), and so are the checkable inputs of the two +cited steps (`Hashing/WeilSupport.lean`, whose facts are referenced at +their points of use below; CI checks the correspondence in both +directions). The cited steps themselves +and Weil's theorem stay on paper — the vocabulary they need is tracked +at #30. ## Background @@ -82,9 +88,16 @@ as above. - **Eisenstein criterion at a place.** The classical irreducibility test transplants to function fields with "prime" replaced by "place of the base curve": lower coefficients vanishing at the place, the - constant term exactly once, leading coefficient a unit. Its - conclusion is what we use: the polynomial is irreducible there and - the cover is *totally ramified* over that place. [Stichtenoth, ch. 3] + constant term exactly once, leading coefficient a unit. The + transplant is an instantiation rather than a new theorem — the + criterion is a statement about any discrete valuation, whose + hypotheses force the Newton polygon to a single segment of slope + −1/n, so every root has valuation 1/n. Its conclusion is what we + use: the polynomial is irreducible there and the cover is *totally + ramified* over that place. [Stichtenoth, ch. 3] [Newton polygons: + J. S. Milne, *Algebraic Number Theory*, course notes, ch. 7, + Prop. 7.44 (stated for characteristic zero, but the argument is + characteristic-free) — free at ] Throughout: q ≡ 1 (mod 4) is the base field size; E′ : y² = g(x) with g(x) = x³ + A·x + B, A·B ≠ 0, and #E′(F_q) an odd prime; Z is a @@ -130,12 +143,14 @@ y² = g(x_j(u)). Direct computation (verified symbolically) factors both: g(x₁(u)) = −B·Φ(u) / (A³·ta³), g(x₂(u)) = −B·Φ(u) / (A³·(Z·u²+1)³), -with the **shared degree-12 core** +with the **shared degree-12 core** (`phiPoly`, matching the pointwise +core by `eval_phiPoly`) Φ(u) = B²·(ta + 1)³ + A³·ta². Using ta = Z·u²·(Z·u²+1) and clearing squares, the two curves have -hyperelliptic models +hyperelliptic models (`model1Poly`, `model2Poly`, evaluating to the +pointwise `model1`, `model2` by `eval_model1Poly`, `eval_model2Poly`) C₁ : W² = d₁·(Z·u²+1)·Φ(u), d₁ = −A³·B·Z³ ≡ −A·B·Z (mod squares), C₂ : W² = d₂·(Z·u²+1)·Φ(u), d₂ = −A³·B ≡ −A·B (mod squares). @@ -145,7 +160,9 @@ geometric curve, two F_q-forms; the twist is the branch dichotomy itself. **Genus.** Φ(0) = B² and Φ = B² at t = −1, so Φ is coprime to u and to -Z·u²+1; its degree is exactly 12 (leading coefficient B²·Z⁶ ≠ 0). The +Z·u²+1 (`phiPoly_coeff_zero`, `phiPoly_isCoprime_tPoly_add_one`, with the +quadratic factor separable, `tPoly_add_one_separable`); its degree is +exactly 12 (leading coefficient B²·Z⁶ ≠ 0; `phiPoly_natDegree`). The odd-multiplicity part of the right-hand side is therefore (Z·u²+1)·Φ, of degree 14 — provided Φ is squarefree, which holds unconditionally: @@ -153,18 +170,32 @@ of degree 14 — provided Φ is squarefree, which holds unconditionally: repeated root over the algebraic closure. *Proof.* Φ is a composition: Φ(u) = φ(ta(u)) with the cubic -φ(T) = B²·(T+1)³ + A³·T² = B²·T³ + (A³+3·B²)·T² + 3·B²·T + B². A -repeated root u₀ of Φ has Φ(u₀) = 0 and +φ(T) = B²·(T+1)³ + A³·T² = B²·T³ + (A³+3·B²)·T² + 3·B²·T + B² +(`phiCubic`, `phiPoly`, `phiPoly_eq_comp`; the derivative +`phiCubic_derivative`). A repeated root u₀ of Φ has Φ(u₀) = 0 and Φ′(u₀) = φ′(ta(u₀))·ta′(u₀) = 0. If φ′(ta(u₀)) = 0, then ta(u₀) is a repeated root of φ; but disc(φ) = −A⁶·B²·(4·A³ + 27·B²) ≠ 0, since A·B ≠ 0 and 4·A³ + 27·B² ≠ 0 is exactly the ellipticity of E′. -Otherwise ta′(u₀) = 2·Z·u₀·(2·Z·u₀² + 1) = 0 (char ≠ 2), so either -u₀ = 0, where φ(ta(0)) = φ(0) = B² ≠ 0, or Z·u₀² = −1/2, where -ta(u₀) = −1/4 and 64·φ(−1/4) = 4·A³ + 27·B² ≠ 0 — again ellipticity. -Either way Φ(u₀) ≠ 0, a contradiction. ∎ +(The formal counterpart avoids the discriminant: `phiCubic_separable` +witnesses coprimality of φ and φ′ directly, by a Bézout identity with +constant A³·B²·(4·A³ + 27·B²), through the generic +`isCoprime_of_bezout`.) Otherwise +ta′(u₀) = 2·Z·u₀·(2·Z·u₀² + 1) = 0 (char ≠ 2; `taPoly_derivative`), so +either u₀ = 0, where φ(ta(0)) = φ(0) = B² ≠ 0 (`phiPoly_coeff_zero`, +via `isCoprime_X_of_coeff_zero`), or Z·u₀² = −1/2, where ta(u₀) = −1/4 +and 64·φ(−1/4) = 4·A³ + 27·B² ≠ 0 — again ellipticity (formally: the +re-expansion 64·Φ = Ψ(2·Z·u² + 1), `psiPoly`, `phiPoly_64_eq`, has +constant term the ellipticity, `psiPoly_coeff_zero`, giving +`phiPoly_isCoprime_snd`). Either way Φ(u₀) ≠ 0, a contradiction. ∎ + +The lemma is `phiPoly_squarefree` in `Hashing/WeilSupport.lean` +(separability `phiPoly_separable`, assembled with the generic +`isCoprime_C_of_ne_zero`), and the models inherit it: +`model1Poly_squarefree` and `model2Poly_squarefree`, squarefree of +degree exactly 14 (`model1Poly_natDegree`, `model2Poly_natDegree`). The discriminant factorization and both critical values are checked symbolically in `scripts/weil-derivation-checks.sage`. So each C_j is @@ -183,19 +214,26 @@ rules every intermediate out at a stroke, since ramification indices multiply along a tower. Consider the fibre w = 0 of E′, i.e. the two geometric points -(−B/A, ±y₀) with y₀² = g(−B/A) = −(B/A)³ ≠ 0 (B ≠ 0). Since y₀ ≠ 0, the +(−B/A, ±y₀) with y₀² = g(−B/A) = −(B/A)³ ≠ 0 (B ≠ 0; +`eval_g_neg_B_div_A`, `g_neg_B_div_A_ne_zero`). Since y₀ ≠ 0, the function w vanishes simply at each, so it is a uniformizer there. - P₂ = B·Z²·u⁴ + Z·w·u² + w is **Eisenstein** at each such point: lower coefficients divisible by w, constant term w exactly once, leading - coefficient B·Z² a unit. So C₂ → E′ is totally ramified over w = 0. + coefficient B·Z² a unit (`p2Poly`, with the coefficient pattern + `p2Poly_coeff`, degree `p2Poly_natDegree`, and the criterion + `p2Poly_isEisensteinAt`). So C₂ → E′ is totally ramified over w = 0. - P₁ = Z²·w·u⁴ + Z·w·u² + B is Eisenstein *reversed*: its reciprocal - polynomial B·u⁴ + Z·w·u² + Z²·w is Eisenstein at the same points, so - C₁ → E′ is totally ramified over w = 0 with the four roots merging at - u = ∞. + polynomial B·u⁴ + Z·w·u² + Z²·w is Eisenstein at the same points + (`p1RecipPoly`, `p1RecipPoly_coeff`, `p1RecipPoly_natDegree`, + `p1RecipPoly_isEisensteinAt`, with `not_X_sq_dvd` for the (w)² + condition), so C₁ → E′ is totally ramified over w = 0 with the four + roots merging at u = ∞. Hence neither cover factors through a nontrivial unramified subcover, -with no condition beyond A·B ≠ 0. +with no condition beyond A·B ≠ 0. The coefficient patterns and the +fibre ordinate above are the formalized inputs; the step from them to +total ramification is the cited part. Independently, the biquadratic shape puts the monodromy inside D₄, and the biquadratic Galois classification pins it: the group drops to V₄ @@ -301,3 +339,4 @@ For `WeilBounded` (squared form): C = 21/2 satisfies (10·√q + 1)² ≤ C²·q at the deployed sizes with margin ≈ 2¹²⁷. The downstream regularity distance ε ≈ C²·√(#G)/#F comes to about 2⁻¹²⁰, improving the ≈ 2⁻¹¹⁶ previously quoted from the FFSTV-sized constant. + diff --git a/scripts/check_weil_support_refs.py b/scripts/check_weil_support_refs.py new file mode 100755 index 0000000..3dc12ad --- /dev/null +++ b/scripts/check_weil_support_refs.py @@ -0,0 +1,42 @@ +#!/usr/bin/env python3 +"""Check the design doc's references to the formalized supporting facts: +every declaration of CompElliptic/Hashing/WeilSupport.lean must be +referenced (backticked) somewhere in design/weil-constant-derivation.md, +and every backticked identifier in the doc must resolve to a declaration +somewhere in CompElliptic or be a known non-Lean term. Run from the +repository root; exits non-zero on violation.""" +import pathlib +import re +import sys + +# Backticked identifiers that are not Lean declarations (RFC and spec +# names, Sage identifiers, and similar). +ALLOWED_NON_LEAN = { + 'map_to_curve_simple_swu', 'hash_to_field', +} + +DECL_RE = re.compile( + r'^(?:noncomputable )?(?:def|theorem|abbrev|structure) ' + r'(?:_root_\.(?:[A-Za-z_][A-Za-z0-9_]*\.)*)?([A-Za-z_][A-Za-z0-9_]*)', + re.M) + +root = pathlib.Path(__file__).resolve().parent.parent +support = set(DECL_RE.findall( + (root / 'CompElliptic/Hashing/WeilSupport.lean').read_text())) +everywhere = set() +for f in (root / 'CompElliptic').rglob('*.lean'): + everywhere |= set(DECL_RE.findall(f.read_text())) + +doc = (root / 'design/weil-constant-derivation.md').read_text() +listed = set(re.findall(r'`([A-Za-z_][A-Za-z0-9_]*)`', doc)) + +missing = sorted(support - listed) +unknown = sorted(listed - everywhere - ALLOWED_NON_LEAN) +if missing: + print("declared in WeilSupport.lean but not referenced in the doc:", + *missing, sep='\n ') +if unknown: + print("backticked in the doc but not a CompElliptic declaration" + " (add to ALLOWED_NON_LEAN if intentional):", + *unknown, sep='\n ') +sys.exit(1 if (missing or unknown) else 0) diff --git a/scripts/weil-derivation-checks.sage b/scripts/weil-derivation-checks.sage index d5f7138..9c571d1 100644 --- a/scripts/weil-derivation-checks.sage +++ b/scripts/weil-derivation-checks.sage @@ -60,6 +60,20 @@ assert phi(0) == b^2 assert 64*phi(-1/QQ(4)) == 4*a^3 + 27*b^2 print("φ composition, discriminant, and critical values: OK") +# The certificates transcribed in Hashing/WeilSupport.lean: φ's Bézout +# cofactors, the re-expansion 64·Φ = Ψ(2·z·u² + 1), and the coprimality +# decomposition of Φ against z·u² + 1: +s3 = (6*a^3*b^2 + 36*b^4)*T + (4*a^6 + 36*a^3*b^2 + 63*b^4) +t3 = (-2*a^3*b^2 - 12*b^4)*T^2 + (-2*a^6 - 18*a^3*b^2 - 33*b^4)*T \ + + (-3*a^3*b^2 - 21*b^4) +assert s3*phi + t3*phi.derivative() == a^3*b^2*(4*a^3 + 27*b^2) +Psi = b^2*T^6 + (4*a^3 + 9*b^2)*T^4 + (27*b^2 - 8*a^3)*T^2 \ + + (4*a^3 + 27*b^2) +assert 64*Phi == Psi(2*z*u^2 + 1) +assert Psi(0) == 4*a^3 + 27*b^2 +assert Phi == ta*(b^2*ta^2 + (3*b^2 + a^3)*ta + 3*b^2) + b^2 +print("WeilSupport certificates: OK") + # g(−b/a) = −(b/a)³, so its square class is that of −a·b: assert g(-b/a) == -(b/a)^3 print("Eisenstein-fibre ordinate identity: OK") From 75ba99fbbc08bbc4ab035a43fa3f1a84a95d4d85 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Tue, 18 Aug 2026 23:58:34 +0100 Subject: [PATCH 10/25] meta: weave the already-proven facts through the design doc MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- design/weil-constant-derivation.md | 118 +++++++++++++++++------------ scripts/check_weil_support_refs.py | 32 ++++++-- 2 files changed, 96 insertions(+), 54 deletions(-) diff --git a/design/weil-constant-derivation.md b/design/weil-constant-derivation.md index 1abe54c..4fcc817 100644 --- a/design/weil-constant-derivation.md +++ b/design/weil-constant-derivation.md @@ -11,7 +11,7 @@ where S_f(χ) = Σ_{u ∈ F_q} χ(f(u)) and f is the odd (zero-repaired) form of `map_to_curve_simple_swu` into the iso-curve E′. This discharges the `WeilBounded` hypothesis of `Hashing/WellDistributed.lean` at C = 21/2 with enormous margin: (10√q + 1)² ≤ (21/2)²·q needs 10.25·q ≥ 20√q + 1, -and q > 2²⁵⁴. +and q > 2^{254}. Status: this document is a proof of the bound, modulo results cited as established mathematics: Weil's theorem in the form of FFSTV's Lemma 1 @@ -24,10 +24,9 @@ per-cover Weil inputs to the deployed constants is machine-checked (CompElliptic's `Hashing/BranchCovers.lean`, `Hashing/WeilInstance.lean`, and `Hashing/PastaSSWU.lean`), and so are the checkable inputs of the two cited steps (`Hashing/WeilSupport.lean`, whose facts are referenced at -their points of use below; CI checks the correspondence in both -directions). The cited steps themselves -and Weil's theorem stay on paper — the vocabulary they need is tracked -at #30. +their points of use below; CI checks that this document references all +of that file's declarations). The cited steps themselves and Weil's +theorem stay on paper — the vocabulary they need is tracked at #30. ## Background @@ -40,8 +39,8 @@ Public Key Cryptography*, CUP 2012, free at ), and FFSTV as above. -- **Curves via their function fields.** We work with a curve through its - field of rational functions; points of the curve correspond to +- **Curves via their function fields.** We work with a curve through + its field of rational functions; points of the curve correspond to *places* of the field, and a function *vanishes simply* at a place when it is a local coordinate (a *uniformizer*) there. Everything below is arithmetic in explicit function fields like F_q(E′)(u). @@ -109,20 +108,22 @@ Theorem 6, adapted to these parameters and to sign-freeness. ## 1. The branch covers -For ta ≠ 0 the simplified SWU abscissae are +For ta ≠ 0 the simplified SWU abscissae are (`x1`, `x2`) x₁(u) = B·(ta + 1) / (A·(−ta)), x₂(u) = t·x₁(u), and exactly one of g(x₁(u)), g(x₂(u)) is a square, by the identity -g(x₂) = t³·g(x₁) with t = Z·u² in the square class of Z. The mapping -outputs the point with the square candidate, with its ordinate's sign -set by `sgn0`; the zero-repaired form sets f(0) = 𝒪, which makes f odd: -f(−u) = −f(u) for all u. +g(x₂) = t³·g(x₁) with t = Z·u² in the square class of Z (in cleared +form, `g_x2_eq`). The mapping outputs the point with the square +candidate, with its ordinate's sign set by `sgn0`; the zero-repaired +form sets f(0) = 𝒪, which makes f odd: f(−u) = −f(u) for all u (`map_neg` +away from 0; on each deployed curve, `isOdd_zeroRepaired_mapToCurve`). Since q ≡ 1 (mod 4), −1 is a square, so −1/Z is a nonsquare and t = −1 -has no solutions: **ta vanishes only at u = 0**, and the exceptional -input set is exactly {0}. (This is where the deployed setting is simpler -than FFSTV's q ≡ 3 (mod 4), whose t = −1 fibre is inhabited.) +has no solutions (`Zuu_add_one_ne_zero`): **ta vanishes only at u = 0** +(`ta_ne_zero_of_u_ne_zero`), and the exceptional input set is exactly +{0}. (This is where the deployed setting is simpler than FFSTV's +q ≡ 3 (mod 4), whose t = −1 fibre is inhabited.) Rearranging x = x_j(u) gives the covers of E′ as quartics in u over the function field F_q(E′), writing w = A·x + B: @@ -144,20 +145,21 @@ y² = g(x_j(u)). Direct computation (verified symbolically) factors both: g(x₂(u)) = −B·Φ(u) / (A³·(Z·u²+1)³), with the **shared degree-12 core** (`phiPoly`, matching the pointwise -core by `eval_phiPoly`) +`phiCore` by `eval_phiPoly`) Φ(u) = B²·(ta + 1)³ + A³·ta². Using ta = Z·u²·(Z·u²+1) and clearing squares, the two curves have hyperelliptic models (`model1Poly`, `model2Poly`, evaluating to the -pointwise `model1`, `model2` by `eval_model1Poly`, `eval_model2Poly`) +pointwise `model1`, `model2` by `eval_model1Poly`, `eval_model2Poly`; +their relation to the curve equation at x_j is `model1_eq`, `model2_eq`) C₁ : W² = d₁·(Z·u²+1)·Φ(u), d₁ = −A³·B·Z³ ≡ −A·B·Z (mod squares), C₂ : W² = d₂·(Z·u²+1)·Φ(u), d₂ = −A³·B ≡ −A·B (mod squares). -So C₁ and C₂ are **quadratic twists of one another by Z** — one -geometric curve, two F_q-forms; the twist is the branch dichotomy -itself. +So C₁ and C₂ are **quadratic twists of one another by Z** (`twist1`, +`twist2`, differing by Z³ = Z times a square) — one geometric curve, +two F_q-forms; the twist is the branch dichotomy itself. **Genus.** Φ(0) = B² and Φ = B² at t = −1, so Φ is coprime to u and to Z·u²+1 (`phiPoly_coeff_zero`, `phiPoly_isCoprime_tPoly_add_one`, with the @@ -181,15 +183,14 @@ repeated root of φ; but since A·B ≠ 0 and 4·A³ + 27·B² ≠ 0 is exactly the ellipticity of E′. (The formal counterpart avoids the discriminant: `phiCubic_separable` witnesses coprimality of φ and φ′ directly, by a Bézout identity with -constant A³·B²·(4·A³ + 27·B²), through the generic -`isCoprime_of_bezout`.) Otherwise -ta′(u₀) = 2·Z·u₀·(2·Z·u₀² + 1) = 0 (char ≠ 2; `taPoly_derivative`), so -either u₀ = 0, where φ(ta(0)) = φ(0) = B² ≠ 0 (`phiPoly_coeff_zero`, -via `isCoprime_X_of_coeff_zero`), or Z·u₀² = −1/2, where ta(u₀) = −1/4 -and 64·φ(−1/4) = 4·A³ + 27·B² ≠ 0 — again ellipticity (formally: the -re-expansion 64·Φ = Ψ(2·Z·u² + 1), `psiPoly`, `phiPoly_64_eq`, has -constant term the ellipticity, `psiPoly_coeff_zero`, giving -`phiPoly_isCoprime_snd`). Either way Φ(u₀) ≠ 0, a contradiction. ∎ +constant A³·B²·(4·A³ + 27·B²), through the generic `isCoprime_of_bezout`.) +Otherwise ta′(u₀) = 2·Z·u₀·(2·Z·u₀² + 1) = 0 (char ≠ 2; +`taPoly_derivative`), so either u₀ = 0, where φ(ta(0)) = φ(0) = B² ≠ 0 +(`phiPoly_coeff_zero`, via `isCoprime_X_of_coeff_zero`), or Z·u₀² = −1/2, +where ta(u₀) = −1/4 and 64·φ(−1/4) = 4·A³ + 27·B² ≠ 0 — again ellipticity. +(Formally: the re-expansion 64·Φ = Ψ(2·Z·u² + 1), `psiPoly`, +`phiPoly_64_eq`, has constant term the ellipticity, `psiPoly_coeff_zero`, +giving `phiPoly_isCoprime_snd`.) Either way Φ(u₀) ≠ 0, a contradiction. ∎ The lemma is `phiPoly_squarefree` in `Hashing/WeilSupport.lean` (separability `phiPoly_separable`, assembled with the generic @@ -253,6 +254,10 @@ By Theorem 3(6), for every nontrivial character χ of E′(F_q): |S_{C_j}(χ)| := |Σ_{P ∈ C_j(F_q)} χ(h_j(P))| ≤ (2·6 − 2)·√q = 10·√q. +(This is the cited Weil input. It enters the formal development squared +and over the model point sets, as the two `CharSumBounded` hypotheses +at bound 100·q.) + FFSTV additionally needed the sign of the ordinate as an Artin character (their conductor term deg y = 12), because their sum selects one point per input. Oddness makes that unnecessary: substituting @@ -262,7 +267,8 @@ u → −u shows S_f(χ) is real, so and (χ + χ̄)(f(u)) = χ(P) + χ(−P) depends only on the ±-class of f(u) — which the sign rule never influences. This is the same reduction that -`CharacterSum.lean` formalizes as the ±-class multiplicity form. +`CharacterSum.lean` formalizes as the ±-class multiplicity form +(`charSum_eq`, with the symmetry from `IsOdd.mult_neg`). **The correspondence.** All counting happens on the smooth model W² = H_j(u), with H_j = d_j·(Z·u²+1)·Φ squarefree of degree 14 by the @@ -272,19 +278,25 @@ singular point would need W = 0 at a repeated root of H_j. Over each u₀ there are two rational points when H_j(u₀) is a nonzero square, one when H_j(u₀) = 0, and none when H_j(u₀) is a nonsquare. Since the degree 14 is even, there are two more points at infinity, rational -exactly when the leading coefficient of H_j is a square. +exactly when the leading coefficient of H_j is a square. This reading +is what the point sets `modelPoints1`, `modelPoints2` encode: the +affine solutions of W² = H_j(u), plus the pair at infinity exactly +when the leading square class d_j·Z is a square. The model coordinate is W = y·s_j(u), with s₁ = A³·Z³·u³·(Z·u²+1)² and -s₂ = A³·(Z·u²+1)²; the identities g(x_j(u))·s_j(u)² = H_j(u) are -checked symbolically. Since Z·u²+1 has no rational roots (−1/Z is a -nonsquare), s_j(u₀) ≠ 0 for every input u₀ ∉ {0}. Over such a u₀, then, +s₂ = A³·(Z·u²+1)² (`scale1`, `scale2`); the identities +g(x_j(u))·s_j(u)² = H_j(u) are checked symbolically and proven as +`model1_eq`, `model2_eq`. Since Z·u²+1 has no rational roots (−1/Z is +a nonsquare; `Zuu_add_one_ne_zero`), s_j(u₀) ≠ 0 for every input +u₀ ∉ {0} (`scale1_ne_zero`, `scale2_ne_zero`). Over such a u₀, then, y ↦ W = y·s_j(u₀) is a bijection between the rational points of y² = g(x_j(u)) and those of the model, and H_j(u₀) is a square exactly when g(x_j(u₀)) is. So on the branch j with g(x_j(u₀)) a square, the fibre of C_j over u₀ consists of the two ordinate-conjugate points, which map under h_j to f(u₀) and −f(u₀), contributing exactly -(χ + χ̄)(f(u₀)); the other branch's fibre has no rational points. Three -boundary cases: +(χ + χ̄)(f(u₀)); the other branch's fibre has no rational points. The +last two sentences are `fibre_sum`, with h_j in model coordinates as +`cover1Map`, `cover2Map`. Three boundary cases: - **W = 0** would merge the two points. It happens only at rational roots of (Z·u²+1)·Φ, hence only at rational roots of Φ; and a @@ -292,7 +304,8 @@ boundary cases: rational 2-torsion point of E′. Since #E′(F_q) is an odd prime, E′ has no rational 2-torsion, so Φ has no rational roots and this case is empty. -- **u = 0**: H_j(0) = d_j·B², in the square class of d_j. +- **u = 0**: H_j(0) = d_j·B², in the square class of d_j + (`model1_zero`, `model2_zero`). - **u = ∞**: the leading coefficient of H_j is d_j·B²·Z⁷, in the square class of d_j·Z. @@ -304,7 +317,8 @@ abscissa functions (checked symbolically): x₁ has a pole at u = 0 and tends to −B/A at u = ∞, while x₂(0) = −B/A and x₂ has a pole at u = ∞. A pole of x_j at the place means the point maps to 𝒪. At the deployed parameters −A·B is a nonsquare (the script's empty w = 0 -fibre), so the rational pairs are C₁'s over u = 0 and C₂'s at +fibre; the Euler certificates `neg_AB_not_isSquare`, one per +iso-curve), so the rational pairs are C₁'s over u = 0 and C₂'s at infinity —both pole loci— and all four extra points map to 𝒪. Summing, with f(0) = 𝒪 and χ(𝒪) = 1: @@ -312,6 +326,10 @@ Summing, with f(0) = 𝒪 and χ(𝒪) = 1: S_{C₁}(χ) + S_{C₂}(χ) = Σ_{u ≠ 0} (χ + χ̄)(f(u)) + 4 = 2·S_f(χ) − 2·χ(𝒪) + 4 = 2·S_f(χ) + 2. +The first equality is `modelPoints_sum`, stated for any +commutative-monoid-valued φ with the boundary contributing 4·φ(𝒪); +the character form through to the + 2 is `cover_charSum`. + (If −A·B were a square, the rational pairs would swap to the −B/A loci: all four extra points would map to the two rational points of E′ over w = 0, contributing 2·(χ + χ̄)(P₀) for P₀ one of them — bounded by @@ -325,18 +343,24 @@ case, so this variant is not needed for them.) so |S_f(χ)| ≤ 10·√q + 1 for every nontrivial χ, on both deployed iso-curves. (For a valid parameter set with −A·B square, §4's variant -gives 10·√q + 3.) The comparison with FFSTV's Theorem 6 (52·√q + 151 -for Z = −1, q ≡ 3 (mod 4), residue-status sign rule): sign-freeness -removes their conductor term and the per-branch double-count, and the -deployed covers have genus 6 against their 8. +gives 10·√q + 3.) The square-root-free formal counterpart is +`weilBounded_zeroRepaired`: two `CharSumBounded` inputs at c²·#F yield +`WeilBounded` at c + 1/2, parametrically in the per-cover constant c; +the deployed c = 10 gives the recorded 21/2. The comparison with +FFSTV's Theorem 6 (52·√q + 151 for Z = −1, q ≡ 3 (mod 4), +residue-status sign rule): sign-freeness removes their conductor term +and the per-branch double-count, and the deployed covers have genus 6 +against their 8. The composition through the deployed 3-isogeny costs nothing: the isogeny is bijective on rational points, so χ ∘ iso ranges over the nontrivial characters of the iso-curve as χ does, and the bound -transfers to the full `mapToCurve` verbatim. +transfers to the full `mapToCurve` verbatim (`WeilBounded.comp`; per +curve, `weilBounded_zeroRepaired_mapToCurve`). For `WeilBounded` (squared form): C = 21/2 satisfies -(10·√q + 1)² ≤ C²·q at the deployed sizes with margin ≈ 2¹²⁷. The -downstream regularity distance ε ≈ C²·√(#G)/#F comes to about 2⁻¹²⁰, -improving the ≈ 2⁻¹¹⁶ previously quoted from the FFSTV-sized constant. - +(10·√q + 1)² ≤ C²·q at the deployed sizes with margin ≈ 2^{127}. The +downstream regularity distance ε ≈ C²·√(#G)/#F (the budget shape of +`sum_abs_prob_dev_le`, carried to the deployed mapping by +`sum_abs_prob_dev_transport_le`) comes to about 2^{-120}, improving +the ≈ 2^{-116} previously quoted from the FFSTV-sized constant. diff --git a/scripts/check_weil_support_refs.py b/scripts/check_weil_support_refs.py index 3dc12ad..f5311bd 100755 --- a/scripts/check_weil_support_refs.py +++ b/scripts/check_weil_support_refs.py @@ -2,9 +2,10 @@ """Check the design doc's references to the formalized supporting facts: every declaration of CompElliptic/Hashing/WeilSupport.lean must be referenced (backticked) somewhere in design/weil-constant-derivation.md, -and every backticked identifier in the doc must resolve to a declaration -somewhere in CompElliptic or be a known non-Lean term. Run from the -repository root; exits non-zero on violation.""" +and every backticked identifier in the doc (dot-qualified ones included) +must resolve to a declaration somewhere in CompElliptic or be a known +non-Lean term. Run from the repository root; exits non-zero on +violation.""" import pathlib import re import sys @@ -17,7 +18,7 @@ DECL_RE = re.compile( r'^(?:noncomputable )?(?:def|theorem|abbrev|structure) ' - r'(?:_root_\.(?:[A-Za-z_][A-Za-z0-9_]*\.)*)?([A-Za-z_][A-Za-z0-9_]*)', + r'(?:_root_\.)?([A-Za-z_][A-Za-z0-9_]*(?:\.[A-Za-z_][A-Za-z0-9_]*)*)', re.M) root = pathlib.Path(__file__).resolve().parent.parent @@ -28,10 +29,27 @@ everywhere |= set(DECL_RE.findall(f.read_text())) doc = (root / 'design/weil-constant-derivation.md').read_text() -listed = set(re.findall(r'`([A-Za-z_][A-Za-z0-9_]*)`', doc)) +listed = set(re.findall( + r'`([A-Za-z_][A-Za-z0-9_]*(?:\.[A-Za-z_][A-Za-z0-9_]*)*)`', doc)) +# Backticked filenames (`BranchCovers.lean`, `weilbound.sage`) are file +# references, not declarations. +listed = {name for name in listed + if not re.search(r'\.(lean|sage|py|md|toml|yml|sh)$', name)} -missing = sorted(support - listed) -unknown = sorted(listed - everywhere - ALLOWED_NON_LEAN) + +def last(name: str) -> str: + """The final dot-separated segment of a (possibly qualified) name.""" + return name.rsplit('.', 1)[-1] + + +# Declarations are spelled bare inside namespace blocks or dot-qualified at +# top level; references may use either form. Compare by final segment. +declared_last = {last(name) for name in everywhere} +missing = sorted({last(name) for name in support} + - {last(name) for name in listed}) +unknown = sorted(name for name in listed + if last(name) not in declared_last + and name not in ALLOWED_NON_LEAN) if missing: print("declared in WeilSupport.lean but not referenced in the doc:", *missing, sep='\n ') From 2612a9726ee9a2bfeee4356d52c88a69730cbc51 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Tue, 18 Aug 2026 23:58:47 +0100 Subject: [PATCH 11/25] feat: realness of an odd mapping's character sum MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `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 --- CompElliptic/Hashing/CharacterSum.lean | 50 ++++++++++++++++++++++++-- design/weil-constant-derivation.md | 8 +++-- 2 files changed, 52 insertions(+), 6 deletions(-) diff --git a/CompElliptic/Hashing/CharacterSum.lean b/CompElliptic/Hashing/CharacterSum.lean index ee4747e..4937d98 100644 --- a/CompElliptic/Hashing/CharacterSum.lean +++ b/CompElliptic/Hashing/CharacterSum.lean @@ -24,10 +24,13 @@ the uniform distribution on `G`. The mappings used to hash to elliptic curves (simplified SWU and its relatives) choose the sign of the `y`-coordinate from the sign of the input. That sign rule makes the mapping **odd**: `f (-u) = -f u`. This file proves that oddness alone -forces two facts: +forces these facts: -* the value multiplicity is symmetric under negation (`IsOdd.mult_neg`); and -* `f` sends `0` to `0` when `G` has odd order (`IsOdd.map_zero`). +* the value multiplicity is symmetric under negation (`IsOdd.mult_neg`); +* `f` sends `0` to `0` when `G` has odd order (`IsOdd.map_zero`); +* the character sum is real (`IsOdd.conj_charSum`), and twice the sum is the + sum of the conjugation-symmetric terms `ψ (f u) + conj (ψ (f u))` + (`IsOdd.two_mul_charSum`). The main identity (`charSum_eq`) rewrites `∑ u, ψ (f u)` as the character transform of `fun Q => mult f Q - 1`, the deviation of the value multiplicity from a perfect @@ -117,4 +120,45 @@ theorem charSum_eq {ψ : AddChar G ℂ} (hψ : ψ ≠ 1) : exact Finset.sum_congr rfl fun Q _ => by ring rw [hsplit, hzero, sub_zero] +omit [DecidableEq G] in +/-- Negating the argument of a complex character conjugates its value: on a +finite group every character value is a root of unity, hence of unit norm, +and `ψ (-P) = (ψ P)⁻¹`. -/ +theorem addChar_map_neg_eq_conj (ψ : AddChar G ℂ) (P : G) : + ψ (-P) = (starRingEnd ℂ) (ψ P) := by + have hpow : ψ P ^ Fintype.card G = 1 := by + rw [← AddChar.map_nsmul_eq_pow, card_nsmul_eq_zero, AddChar.map_zero_eq_one] + rw [AddChar.map_neg_eq_inv, + Complex.inv_eq_conj (Complex.norm_eq_one_of_pow_eq_one hpow + Fintype.card_ne_zero)] + +omit [DecidableEq F] [DecidableEq G] in +/-- **Realness** (design doc §4): the character sum of an odd mapping is fixed +by complex conjugation. Conjugating a term negates the output +(`addChar_map_neg_eq_conj`), which oddness trades for negating the input, and +input negation permutes the domain. -/ +theorem IsOdd.conj_charSum (hf : IsOdd f) (ψ : AddChar G ℂ) : + (starRingEnd ℂ) (∑ u, ψ (f u)) = ∑ u, ψ (f u) := by + rw [map_sum] + calc ∑ u, (starRingEnd ℂ) (ψ (f u)) + = ∑ u, ψ (f (-u)) := by + refine Finset.sum_congr rfl fun u _ => ?_ + rw [hf u, addChar_map_neg_eq_conj] + _ = ∑ u, ψ (f u) := + Fintype.sum_equiv (Equiv.neg F) _ _ fun u => rfl + +omit [DecidableEq F] [DecidableEq G] in +/-- **The doubled character sum, sign-free** (design doc §4): twice the +character sum of an odd mapping is the sum of `ψ (f u) + conj (ψ (f u))` over +inputs. Each term equals `ψ P + ψ (-P)` at `P = f u` +(`addChar_map_neg_eq_conj`), so it is unchanged by negating `f u`: the sign +convention has no influence on it. -/ +theorem IsOdd.two_mul_charSum (hf : IsOdd f) (ψ : AddChar G ℂ) : + 2 * ∑ u, ψ (f u) = ∑ u, (ψ (f u) + (starRingEnd ℂ) (ψ (f u))) := by + have h : ∑ u, (starRingEnd ℂ) (ψ (f u)) = ∑ u, ψ (f u) := by + rw [← map_sum (starRingEnd ℂ) (fun u => ψ (f u)) Finset.univ] + exact hf.conj_charSum ψ + rw [Finset.sum_add_distrib, h] + ring + end CompElliptic.Hashing diff --git a/design/weil-constant-derivation.md b/design/weil-constant-derivation.md index 4fcc817..e26346f 100644 --- a/design/weil-constant-derivation.md +++ b/design/weil-constant-derivation.md @@ -261,12 +261,14 @@ at bound 100·q.) FFSTV additionally needed the sign of the ordinate as an Artin character (their conductor term deg y = 12), because their sum selects one point per input. Oddness makes that unnecessary: substituting -u → −u shows S_f(χ) is real, so +u → −u shows S_f(χ) is real (`IsOdd.conj_charSum`), so 2·S_f(χ) = Σ_{u} (χ + χ̄)(f(u)), -and (χ + χ̄)(f(u)) = χ(P) + χ(−P) depends only on the ±-class of f(u) — -which the sign rule never influences. This is the same reduction that +(`IsOdd.two_mul_charSum`), and (χ + χ̄)(f(u)) = χ(P) + χ(−P) depends +only on the ±-class of f(u) — which the sign rule never influences +(the identity χ(−P) = χ̄(P) behind the pairing is +`addChar_map_neg_eq_conj`). This is the same reduction that `CharacterSum.lean` formalizes as the ±-class multiplicity form (`charSum_eq`, with the symmetry from `IsOdd.mult_neg`). From 4b2d51c814df4b9fff9a6b7b95c072a1bb8dddd6 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Wed, 19 Aug 2026 00:02:39 +0100 Subject: [PATCH 12/25] feat: the monodromy square exclusions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- CompElliptic/Hashing/WeilSupport.lean | 299 ++++++++++++++++++++++++++ design/weil-constant-derivation.md | 48 ++++- scripts/weil-derivation-checks.sage | 29 +++ 3 files changed, 365 insertions(+), 11 deletions(-) diff --git a/CompElliptic/Hashing/WeilSupport.lean b/CompElliptic/Hashing/WeilSupport.lean index ff82906..488e752 100644 --- a/CompElliptic/Hashing/WeilSupport.lean +++ b/CompElliptic/Hashing/WeilSupport.lean @@ -5,7 +5,10 @@ as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Daira-Emma Hopwood -/ import CompElliptic.Hashing.BranchCovers +import Mathlib.FieldTheory.RatFunc.Basic import Mathlib.FieldTheory.Separable +import Mathlib.RingTheory.AdjoinRoot +import Mathlib.RingTheory.IntegralClosure.IntegrallyClosed import Mathlib.RingTheory.Polynomial.Eisenstein.Basic /-! @@ -39,6 +42,13 @@ The ramification argument (§3) consumes: * `eval_g_neg_B_div_A` — `g(-B/A) = -(B/A)³ ≠ 0` (this is why `w` is a uniformizer at both points over `w = 0`). +The monodromy cross-check (§3) consumes `v4TestPoly_not_isSquare` and +`c4TestPoly_not_isSquare`: the biquadratic V₄/C₄ square classes +`B·(A·x + B)` and `B·(A·x - 3·B)` are not squares in the function +field. The field is presented via `gPoly` as the quadratic algebra +`K[Y]/(Y² - ĝ)` over `K = F_q(x)`. The section header below describes +the decomposition machinery. + The Eisenstein criterion is that the leading coefficient lies outside the ideal, every lower coefficient lies inside it, and the constant coefficient lies outside its square. The cited total-ramification argument relies on @@ -475,6 +485,295 @@ theorem g_neg_B_div_A_ne_zero : exact neg_ne_zero.mpr (pow_ne_zero 3 (div_ne_zero G.E.B_nonzero G.A_nonzero)) +/-! ## The monodromy square exclusions + +Design doc §3 pins the monodromy group at full `D₄`: the biquadratic +V₄/C₄ square-class tests reduce to `B·(A·x + B)` and `B·(A·x - 3·B)` +being squares in `F_q(E′)`, and both fail. The paper argument is +divisor parity. Its checkable core is elementary, because `F_q(E′)` is +the quadratic algebra `K[Y]/(Y² - ĝ)` over `K = F_q(x)`: + +* a square from the base decomposes there — `a = p²` or `a = ĝ·p²` in + `K` (`sq_or_mul_sq_of_isSquare_adjoinRoot`); +* a rational square root of a polynomial is a polynomial + (`exists_sq_eq_of_ratFunc_sq` — `F[X]` is integrally closed); +* a squarefree polynomial of positive degree is not a polynomial square + (`not_isSquare_ratFunc_of_squarefree`) — the affine shadow of the + divisor parity. + +The Kappe–Warren reduction to the two square classes stays cited; it is +checked symbolically in `scripts/weil-derivation-checks.sage`, along +with the Bézout certificates used below. -/ + +/-- A rational square root of a polynomial is a polynomial: `F[X]` is +integrally closed in `F(X)`, and an element whose square is a polynomial +is integral over `F[X]`. -/ +theorem _root_.CompElliptic.Hashing.exists_sq_eq_of_ratFunc_sq + {F : Type*} [Field F] {n : Polynomial F} {p : RatFunc F} + (h : p^2 = algebraMap (Polynomial F) (RatFunc F) n) : + ∃ f : Polynomial F, f^2 = n := by + have hint : IsIntegral (Polynomial F) p := + ⟨X^2 - C n, monic_X_pow_sub_C n (by norm_num), by + simp only [eval₂_sub, eval₂_pow, eval₂_X, eval₂_C] + rw [h, sub_self]⟩ + obtain ⟨f, hf⟩ := IsIntegrallyClosed.isIntegral_iff.mp hint + refine ⟨f, IsFractionRing.injective (Polynomial F) (RatFunc F) ?_⟩ + rw [map_pow, hf, h] + +/-- A squarefree polynomial of positive degree is not a square in the +rational-function field: a rational square root would be a polynomial +(`exists_sq_eq_of_ratFunc_sq`). Its square divides the squarefree +target, so it is a unit and the target is constant. -/ +theorem _root_.CompElliptic.Hashing.not_isSquare_ratFunc_of_squarefree + {F : Type*} [Field F] {n : Polynomial F} (hsf : Squarefree n) + (hdeg : n.natDegree ≠ 0) : + ¬ IsSquare (algebraMap (Polynomial F) (RatFunc F) n) := by + rintro ⟨p, hp⟩ + obtain ⟨f, hf⟩ := exists_sq_eq_of_ratFunc_sq (p := p) + (by rw [sq]; exact hp.symm) + have hunit : IsUnit f := hsf f ⟨1, by rw [← hf]; ring⟩ + refine hdeg ?_ + rw [← hf, natDegree_pow, natDegree_eq_zero_of_isUnit hunit, mul_zero] + +/-- **Squares from the base of a quadratic extension decompose**. Write +a square root of `a` in `K[Y]/(Y² - g)` as `p₀ + p₁·Y`; its square is +`(p₀² + g·p₁²) + 2·p₀·p₁·Y`. So away from characteristic 2, either +`a = p₀²` or `a = g·p₁²` in `K`. -/ +theorem _root_.CompElliptic.Hashing.sq_or_mul_sq_of_isSquare_adjoinRoot + {K : Type*} [Field K] (h2 : (2 : K) ≠ 0) {g a : K} + (h : IsSquare (AdjoinRoot.of (X^2 - C g) a)) : + (∃ p : K, a = p^2) ∨ ∃ p : K, a = g * p^2 := by + have hmonic : (X^2 - C g).Monic := monic_X_pow_sub_C g (by norm_num) + have hdeg2 : (X^2 - C g).degree = 2 := degree_X_pow_sub_C (by norm_num) g + -- Representations `of x + of y · root` are unique: a difference lifts + -- to a polynomial of degree at most 1 divisible by the monic quadratic. + have huniq : ∀ x y x' y' : K, + AdjoinRoot.of (X^2 - C g) x + + AdjoinRoot.of (X^2 - C g) y * AdjoinRoot.root (X^2 - C g) + = AdjoinRoot.of (X^2 - C g) x' + + AdjoinRoot.of (X^2 - C g) y' * AdjoinRoot.root (X^2 - C g) → + x = x' ∧ y = y' := by + intro x y x' y' hxy + have hmk : AdjoinRoot.mk (X^2 - C g) + (C (x - x') + C (y - y') * X) = 0 := by + rw [map_add, map_mul, AdjoinRoot.mk_C, AdjoinRoot.mk_C, + AdjoinRoot.mk_X, map_sub, map_sub] + linear_combination hxy + have hzero : (C (x - x') + C (y - y') * X : Polynomial K) = 0 := by + refine eq_zero_of_dvd_of_degree_lt (AdjoinRoot.mk_eq_zero.mp hmk) ?_ + rw [hdeg2, add_comm] + exact lt_of_le_of_lt degree_linear_le + (by exact_mod_cast (by norm_num : (1 : ℕ) < 2)) + constructor + · have h0 : x - x' = 0 := by + simpa using congrArg (fun p => Polynomial.coeff p 0) hzero + exact sub_eq_zero.mp h0 + · have h1 : y - y' = 0 := by + simpa using congrArg (fun p => Polynomial.coeff p 1) hzero + exact sub_eq_zero.mp h1 + obtain ⟨z, hz⟩ := h + obtain ⟨r, rfl⟩ := AdjoinRoot.mk_surjective z + -- Reduce the representative modulo the monic quadratic. + have hzr : AdjoinRoot.mk (X^2 - C g) r + = AdjoinRoot.mk (X^2 - C g) (r %ₘ (X^2 - C g)) := by + conv_lhs => rw [← modByMonic_add_div r (X^2 - C g)] + rw [map_add, map_mul, AdjoinRoot.mk_self, zero_mul, add_zero] + set p0 := (r %ₘ (X^2 - C g)).coeff 0 with hp0 + set p1 := (r %ₘ (X^2 - C g)).coeff 1 with hp1 + have hrep : r %ₘ (X^2 - C g) = C p1 * X + C p0 := by + rcases eq_or_ne (r %ₘ (X^2 - C g)) 0 with h0 | h0 + · rw [hp0, hp1, h0] + simp + · refine eq_X_add_C_of_degree_le_one ?_ + have hlt := degree_modByMonic_lt r hmonic + rw [hdeg2, degree_eq_natDegree h0] at hlt + rw [degree_eq_natDegree h0] + exact_mod_cast Nat.lt_succ_iff.mp (by exact_mod_cast hlt) + have hroot : (AdjoinRoot.root (X^2 - C g))^2 + = AdjoinRoot.of (X^2 - C g) g := by + have h0 := AdjoinRoot.mk_self (f := X^2 - C g) + rw [map_sub, map_pow, AdjoinRoot.mk_X, AdjoinRoot.mk_C, + sub_eq_zero] at h0 + exact h0 + -- Expand `of a = (of p1 · root + of p0)²` over the basis `{1, root}`. + have hexpand : AdjoinRoot.of (X^2 - C g) a + = AdjoinRoot.of (X^2 - C g) (p0^2 + g * p1^2) + + AdjoinRoot.of (X^2 - C g) (2 * p0 * p1) + * AdjoinRoot.root (X^2 - C g) := by + rw [hz, hzr, hrep] + simp only [map_add, map_mul, map_pow, map_ofNat, AdjoinRoot.mk_C, + AdjoinRoot.mk_X] + linear_combination (AdjoinRoot.of (X^2 - C g) p1)^2 * hroot + obtain ⟨ha, hb⟩ := huniq a 0 (p0^2 + g * p1^2) (2 * p0 * p1) (by + rw [map_zero, zero_mul, add_zero] + exact hexpand) + have hzero : p0 = 0 ∨ p1 = 0 := by + rcases mul_eq_zero.mp hb.symm with h' | h' + · rcases mul_eq_zero.mp h' with h'' | h'' + · exact absurd h'' h2 + · exact Or.inl h'' + · exact Or.inr h' + rcases hzero with h' | h' + · exact Or.inr ⟨p1, by rw [ha, h']; ring⟩ + · exact Or.inl ⟨p0, by rw [ha, h']; ring⟩ + +/-- The curve cubic `g = X³ + A·X + B` as a polynomial over `F`. +Adjoining a square root of its image `ĝ` in `K = F_q(x)` presents the +function field `F_q(E′)`. -/ +noncomputable def gPoly : Polynomial F := X^3 + C G.E.A * X + C G.E.B + +/-- `g` is separable, by the Bézout certificate +`(27·B - 18·A·X)·g + (6·A·X² - 9·B·X + 4·A²)·g′ = 4·A³ + 27·B²` +(checked in `scripts/weil-derivation-checks.sage`): the constant is +nonzero exactly by ellipticity. -/ +theorem gPoly_separable (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : + G.gPoly.Separable := by + have hd : G.gPoly.derivative = 3 * X^2 + C G.E.A := by + simp only [gPoly, derivative_add, derivative_mul, derivative_pow, + derivative_C, derivative_X, Nat.cast_ofNat, map_ofNat] + ring + rw [Polynomial.separable_def, hd] + refine isCoprime_of_bezout + (u := 27 * C G.E.B - 18 * C G.E.A * X) + (v := 6 * C G.E.A * X^2 - 9 * C G.E.B * X + 4 * (C G.E.A)^2) + (c := 4*G.E.A^3 + 27*G.E.B^2) hdisc ?_ + have hC : (C (4*G.E.A^3 + 27*G.E.B^2) : Polynomial F) + = 4*(C G.E.A)^3 + 27*(C G.E.B)^2 := by + simp only [map_add, map_mul, map_pow, map_ofNat] + rw [gPoly, hC] + ring + +/-- `ĝ` is not a square in `F_q(x)`: `g` is squarefree of odd degree. So +`Y² - ĝ` is irreducible and the quadratic algebra below is the function +field `F_q(E′)` itself. (The exclusions need only the ring structure, so +that last step stays informal.) -/ +theorem gPoly_not_isSquare_ratFunc + (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : + ¬ IsSquare (algebraMap (Polynomial F) (RatFunc F) G.gPoly) := by + refine not_isSquare_ratFunc_of_squarefree + (G.gPoly_separable hdisc).squarefree ?_ + have h3 : G.gPoly.natDegree = 3 := by unfold gPoly; compute_degree! + omega + +/-- **The common core of the two exclusions**: for any linear `l` +coprime to `g`, the class `B·l` is not a square in the quadratic +algebra `K[Y]/(Y² - ĝ)`. A square would decompose as `p²` or `ĝ·p²` +over `K` (`sq_or_mul_sq_of_isSquare_adjoinRoot`), and each case +descends to a polynomial square (`exists_sq_eq_of_ratFunc_sq`). That +contradicts the squarefreeness of `B·l` (degree 1) and of `B·l·g` +(degree 4) respectively, by `not_isSquare_ratFunc_of_squarefree`. -/ +theorem not_isSquare_adjoinRoot_of_linear + (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) {l : Polynomial F} + (hdeg : l.natDegree = 1) (hcop : IsCoprime l G.gPoly) : + ¬ IsSquare (AdjoinRoot.of + (X^2 - C (algebraMap (Polynomial F) (RatFunc F) G.gPoly)) + (algebraMap (Polynomial F) (RatFunc F) (C G.E.B * l))) := by + intro hsq + -- Characteristic ≠ 2 (`Z` is a nonsquare) transfers to `F_q(x)`. + have h2F : (2 : F) ≠ 0 := Ring.two_ne_zero G.ringChar_ne_two + have h2P : (2 : Polynomial F) ≠ 0 := fun h => h2F (by + simpa using congrArg (fun p => Polynomial.coeff p 0) h) + have h2 : (2 : RatFunc F) ≠ 0 := fun h => h2P + (IsFractionRing.injective (Polynomial F) (RatFunc F) + (by rw [map_ofNat, map_zero]; exact h)) + -- The linear factor and both products are squarefree, with known + -- degrees. + have hl0 : l ≠ 0 := fun h => by simp [h] at hdeg + have hl1 : l.coeff 1 ≠ 0 := by + have hlc := leadingCoeff_ne_zero.mpr hl0 + rwa [Polynomial.leadingCoeff, hdeg] at hlc + have hlsep : l.Separable := by + have hd : l.derivative = C (l.coeff 1) := by + conv_lhs => rw [eq_X_add_C_of_natDegree_le_one hdeg.le] + simp only [derivative_add, derivative_mul, derivative_C, + derivative_X, zero_mul, mul_one, zero_add, add_zero] + rw [Polynomial.separable_def, hd] + exact isCoprime_C_of_ne_zero hl1 + have hτsep : (C G.E.B * l).Separable := + Polynomial.Separable.mul ((separable_C _).mpr G.E.B_nonzero.isUnit) + hlsep ((isCoprime_C_of_ne_zero G.E.B_nonzero).symm) + have hτdeg : (C G.E.B * l).natDegree = 1 := by + rw [natDegree_mul (C_ne_zero.mpr G.E.B_nonzero) hl0, natDegree_C, + zero_add, hdeg] + have hgm : G.gPoly.Monic := by + unfold gPoly + rw [add_assoc] + exact monic_X_pow_add (lt_of_le_of_lt degree_linear_le + (by exact_mod_cast (by norm_num : (1 : ℕ) < 3))) + have hg3 : G.gPoly.natDegree = 3 := by unfold gPoly; compute_degree! + have hτgsf : Squarefree (C G.E.B * l * G.gPoly) := + (Polynomial.Separable.mul hτsep (G.gPoly_separable hdisc) + (IsCoprime.mul_left ((isCoprime_C_of_ne_zero G.E.B_nonzero).symm) + hcop)).squarefree + -- Decompose the square over the base field and refute both cases. + rcases sq_or_mul_sq_of_isSquare_adjoinRoot h2 hsq with ⟨p, hp⟩ | ⟨p, hp⟩ + · exact not_isSquare_ratFunc_of_squarefree hτsep.squarefree + (by rw [hτdeg]; norm_num) ⟨p, by rw [hp, sq]⟩ + · refine not_isSquare_ratFunc_of_squarefree hτgsf + (by rw [natDegree_mul (mul_ne_zero (C_ne_zero.mpr G.E.B_nonzero) hl0) + hgm.ne_zero, hτdeg, hg3]; norm_num) + ⟨algebraMap (Polynomial F) (RatFunc F) G.gPoly * p, ?_⟩ + rw [map_mul, hp] + ring + +/-- The V₄-test square class of the branch quartics: `B·w = B·(A·x + B)`. -/ +noncomputable def v4TestPoly : Polynomial F := + C G.E.B * (C G.E.A * X + C G.E.B) + +/-- The C₄-test square class of the branch quartics: `B·(A·x - 3·B)`. -/ +noncomputable def c4TestPoly : Polynomial F := + C G.E.B * (C G.E.A * X - 3 * C G.E.B) + +/-- **The V₄ exclusion** (design doc §3): `B·(A·x + B)` is not a square +in the function field. The coprimality certificate is +`(A²·X² - A·B·X + (B² + A³))·(A·X + B) - A³·g = B³` (checked in +`scripts/weil-derivation-checks.sage`). -/ +theorem v4TestPoly_not_isSquare (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : + ¬ IsSquare (AdjoinRoot.of + (X^2 - C (algebraMap (Polynomial F) (RatFunc F) G.gPoly)) + (algebraMap (Polynomial F) (RatFunc F) G.v4TestPoly)) := by + have hdeg : (C G.E.A * X + C G.E.B).natDegree = 1 := by + compute_degree! + all_goals exact G.A_nonzero + have hcop : IsCoprime (C G.E.A * X + C G.E.B) G.gPoly := by + refine isCoprime_of_bezout + (u := (C G.E.A)^2 * X^2 - C G.E.A * C G.E.B * X + + ((C G.E.B)^2 + (C G.E.A)^3)) + (v := -(C G.E.A)^3) + (c := G.E.B^3) (pow_ne_zero 3 G.E.B_nonzero) ?_ + have hC : (C (G.E.B^3) : Polynomial F) = (C G.E.B)^3 := map_pow _ _ _ + rw [gPoly, hC] + ring + unfold v4TestPoly + exact G.not_isSquare_adjoinRoot_of_linear hdisc hdeg hcop + +/-- **The C₄ exclusion** (design doc §3): `B·(A·x - 3·B)` is not a square +in the function field. The coprimality certificate is +`A³·g - (A²·X² + 3·A·B·X + (9·B² + A³))·(A·X - 3·B) = B·(4·A³ + 27·B²)` +(checked in `scripts/weil-derivation-checks.sage`); its constant is again +a product of the standing nonzero quantities. -/ +theorem c4TestPoly_not_isSquare (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : + ¬ IsSquare (AdjoinRoot.of + (X^2 - C (algebraMap (Polynomial F) (RatFunc F) G.gPoly)) + (algebraMap (Polynomial F) (RatFunc F) G.c4TestPoly)) := by + have hdeg : (C G.E.A * X - 3 * C G.E.B).natDegree = 1 := by + compute_degree! + all_goals exact G.A_nonzero + have hcop : IsCoprime (C G.E.A * X - 3 * C G.E.B) G.gPoly := by + refine isCoprime_of_bezout + (u := -((C G.E.A)^2 * X^2 + 3 * C G.E.A * C G.E.B * X + + (9*(C G.E.B)^2 + (C G.E.A)^3))) + (v := (C G.E.A)^3) + (c := G.E.B * (4*G.E.A^3 + 27*G.E.B^2)) + (mul_ne_zero G.E.B_nonzero hdisc) ?_ + have hC : (C (G.E.B * (4*G.E.A^3 + 27*G.E.B^2)) : Polynomial F) + = C G.E.B * (4*(C G.E.A)^3 + 27*(C G.E.B)^2) := by + simp only [map_mul, map_add, map_pow, map_ofNat] + rw [gPoly, hC] + ring + unfold c4TestPoly + exact G.not_isSquare_adjoinRoot_of_linear hdisc hdeg hcop + end SSWUParams end CompElliptic.Hashing diff --git a/design/weil-constant-derivation.md b/design/weil-constant-derivation.md index e26346f..2952bd2 100644 --- a/design/weil-constant-derivation.md +++ b/design/weil-constant-derivation.md @@ -236,17 +236,43 @@ with no condition beyond A·B ≠ 0. The coefficient patterns and the fibre ordinate above are the formalized inputs; the step from them to total ramification is the cited part. -Independently, the biquadratic shape puts the monodromy inside D₄, and -the biquadratic Galois classification pins it: the group drops to V₄ -(three intermediate quadratics) only if the normalized constant term is -a square in F_q(E′), and to C₄ only if q·(p² − 4q) is. These reduce to -B·(A·x + B) and B·(A·x − 3·B) being squares in F_q(E′), which fail by -divisor parity (each has two simple zeros and a double pole, so its -divisor is not twice a divisor). So the monodromy is full D₄ and the -v = u² subcover is the unique intermediate — consistent with the -script's Frobenius statistics (5000 samples per branch match the D₄ -cycle-type proportions ⅛, ¼, ⅜, ¼ to within ±0.006) and its nonsquare -specialization witnesses. +Independently, the biquadratic shape puts the monodromy inside D₄, +and the biquadratic Galois classification pins it. The group drops to +V₄ (three intermediate quadratics) only if the normalized constant +term is a square in F_q(E′), and to C₄ only if q·(p² − 4q) is. For +both quartics, these reduce to the same two classes: B·(A·x + B) and +B·(A·x − 3·B) being squares in F_q(E′). (The reductions are checked +symbolically in `scripts/weil-derivation-checks.sage`.) Both fail by +divisor parity: each class has two simple zeros and a double pole, so +its divisor is not twice a divisor. So the monodromy is full D₄, and +the v = u² subcover is the unique intermediate. This is consistent +with the script's Frobenius statistics (5000 samples per branch match +the D₄ cycle-type proportions ⅛, ¼, ⅜, ¼ to within ±0.006) and with +its nonsquare specialization witnesses. + +The two failures are formalized as `v4TestPoly_not_isSquare` and +`c4TestPoly_not_isSquare` (the classes are `v4TestPoly`, `c4TestPoly`), +with no vocabulary beyond polynomials. F_q(E′) is the quadratic algebra +K[Y]/(Y² − ĝ) over K = F_q(x), for ĝ the image of the curve cubic +`gPoly`. The algebra is the field itself, because ĝ is not a square in +K (`gPoly_not_isSquare_ratFunc`, via `gPoly_separable`). The parity +argument's affine form rests on three facts: + +- a square from the base decomposes as p² or ĝ·p² + (`sq_or_mul_sq_of_isSquare_adjoinRoot`, in characteristic ≠ 2); +- a rational square root of a polynomial is a polynomial + (`exists_sq_eq_of_ratFunc_sq` — F_q[x] is integrally closed); +- a squarefree polynomial of positive degree is not a polynomial + square (`not_isSquare_ratFunc_of_squarefree`). + +The shared core `not_isSquare_adjoinRoot_of_linear` applies these to +B·l of degree 1 and to B·l·g of degree 4. The coprimality of each +linear factor l with g comes from a Bézout certificate. The two +constants are B³ and B·(4·A³ + 27·B²) — ellipticity yet again. (The +certificates are normalized with positive constants. That matches the +file's other certificates, and it keeps a negation out of the +constant-lifting step of the Lean proofs; it is why they differ by +sign from the naïve division remainders.) ## 4. The sign-free assembly diff --git a/scripts/weil-derivation-checks.sage b/scripts/weil-derivation-checks.sage index 9c571d1..efd6721 100644 --- a/scripts/weil-derivation-checks.sage +++ b/scripts/weil-derivation-checks.sage @@ -98,3 +98,32 @@ assert n1.leading_coefficient() / e1.leading_coefficient() == -b/a assert n2(0) / e2(0) == -b/a assert n2.degree() > e2.degree() print("boundary images of x_j: OK") + +# Monodromy square-exclusion certificates (design doc §3, WeilSupport): +# g's separability, the coprimality of the V₄/C₄ linear factors with g, +# and the Kappe–Warren reductions to the square classes b·w and +# b·(w − 4·b) = b·(a·x − 3·b). +Rx = PolynomialRing(K, 'x') +X = Rx.gen() +gx = X^3 + a*X + b +gd = gx.derivative() +assert (27*b - 18*a*X)*gx + (6*a*X^2 - 9*b*X + 4*a^2)*gd \ + == 4*a^3 + 27*b^2 +assert (a^2*X^2 - a*b*X + (b^2 + a^3))*(a*X + b) - a^3*gx == b^3 +assert a^3*gx - (a^2*X^2 + 3*a*b*X + (9*b^2 + a^3))*(a*X - 3*b) \ + == b*(4*a^3 + 27*b^2) +assert gx(3*b/a) == b*(4*a^3 + 27*b^2)/a^3 +print("monodromy Bézout certificates: OK") + +# The Kappe–Warren square-class reductions. Writing each quartic monically +# as u⁴ + p·u² + q over F_q(E′): V₄ needs q a square, C₄ needs q·(p² − 4·q) +# a square. Both quartics reduce both tests to the same two square classes: +FW = PolynomialRing(K, 'w').fraction_field() +w = FW.gen() +p1q, q1q = 1/FW(z), b/(z^2*w) +p2q, q2q = w/(b*z), w/(b*z^2) +assert q1q * (b*w) == (b/z)^2 +assert q2q * (b*w) == (w/z)^2 +assert q1q*(p1q^2 - 4*q1q) * (b*(w - 4*b)) == (b*(w - 4*b)/(z^2*w))^2 +assert q2q*(p2q^2 - 4*q2q) * (b*(w - 4*b)) == (w*(w - 4*b)/(b*z^2))^2 +print("Kappe–Warren square-class reductions: OK") From 515ad63a9794c8a48a9db03a91e172cb2c745b75 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Wed, 19 Aug 2026 00:08:32 +0100 Subject: [PATCH 13/25] refactor: reorder WeilSupport.lean into the doc's reading order MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- CompElliptic/Hashing/WeilSupport.lean | 175 +++++++++++++------------- 1 file changed, 88 insertions(+), 87 deletions(-) diff --git a/CompElliptic/Hashing/WeilSupport.lean b/CompElliptic/Hashing/WeilSupport.lean index 488e752..009b6ee 100644 --- a/CompElliptic/Hashing/WeilSupport.lean +++ b/CompElliptic/Hashing/WeilSupport.lean @@ -90,23 +90,13 @@ namespace SSWUParams variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] variable (G : SSWUParams F) -/-! ## The core `Φ` as a polynomial, and its cubic factor through `ta` -/ - -/-- The cubic `φ(T) = B²·(T + 1)³ + A³·T²` through which the core factors: -`Φ = φ ∘ ta` (design doc §2, the squarefreeness lemma). -/ -noncomputable def phiCubic : Polynomial F := - (C G.E.B)^2 * (X + 1)^3 + (C G.E.A)^3 * X^2 +/-! ## The core `Φ` as a polynomial -/ /-- The core `Φ(u) = B²·(ta + 1)³ + A³·ta²` as a polynomial in `u` (`phiCore` is its evaluation). -/ noncomputable def phiPoly : Polynomial F := (C G.E.B)^2 * (G.taPoly + 1)^3 + (C G.E.A)^3 * G.taPoly^2 -/-- `Φ` factors through `ta`: `Φ = φ ∘ ta`. -/ -theorem phiPoly_eq_comp : G.phiPoly = G.phiCubic.comp G.taPoly := by - simp only [phiPoly, phiCubic, add_comp, mul_comp, pow_comp, C_comp, X_comp, - one_comp] - /-- `phiPoly` evaluates to the pointwise core `phiCore`. -/ theorem eval_phiPoly (u : F) : G.phiPoly.eval u = G.phiCore u := by simp only [phiPoly, phiCore, taPoly, tPoly, eval_add, eval_mul, eval_pow, @@ -118,12 +108,78 @@ theorem phiPoly_natDegree : G.phiPoly.natDegree = 12 := by compute_degree! exact ⟨G.E.B_nonzero, G.Z_nonzero⟩ +/-! ## The models `H_j = d_j·(Z·u²+1)·Φ` as polynomials -/ + +/-- The first model `H₁ = d₁·(Z·u²+1)·Φ` as a polynomial in `u`. -/ +noncomputable def model1Poly : Polynomial F := + C G.twist1 * ((G.tPoly + 1) * G.phiPoly) + +/-- The second model `H₂ = d₂·(Z·u²+1)·Φ` as a polynomial in `u`. -/ +noncomputable def model2Poly : Polynomial F := + C G.twist2 * ((G.tPoly + 1) * G.phiPoly) + +/-- `model1Poly` evaluates to the pointwise model `model1`. -/ +theorem eval_model1Poly (u : F) : G.model1Poly.eval u = G.model1 u := by + simp only [model1Poly, model1, tPoly, eval_mul, eval_add, eval_C, eval_X, + eval_pow, eval_one, G.eval_phiPoly] + ring + +/-- `model2Poly` evaluates to the pointwise model `model2`. -/ +theorem eval_model2Poly (u : F) : G.model2Poly.eval u = G.model2 u := by + simp only [model2Poly, model2, tPoly, eval_mul, eval_add, eval_C, eval_X, + eval_pow, eval_one, G.eval_phiPoly] + ring + +/-! ## The genus inputs: `Φ` at `u = 0`, and coprime to `Z·X² + 1` -/ + +/-- `Φ` has constant coefficient `B²`: it is coprime to `X`. This is the +design doc's `φ(ta(0)) = B² ≠ 0` case of the squarefreeness lemma. -/ +theorem phiPoly_coeff_zero : G.phiPoly.coeff 0 = G.E.B^2 := by + rw [coeff_zero_eq_eval_zero, G.eval_phiPoly, G.phiCore_zero] + +/-- `Φ` is coprime to `Z·X² + 1`: modulo that factor, `ta = 0` and +`Φ = B²`. This is the design doc's coprimality of `Φ` with the models' +quadratic factor. -/ +theorem phiPoly_isCoprime_tPoly_add_one : + IsCoprime G.phiPoly (G.tPoly + 1) := by + refine isCoprime_of_bezout (u := 1) + (v := -(G.tPoly * ((C G.E.B)^2 * G.taPoly^2 + + (3*(C G.E.B)^2 + (C G.E.A)^3) * G.taPoly + 3*(C G.E.B)^2))) + (c := G.E.B^2) (pow_ne_zero 2 G.E.B_nonzero) ?_ + have hC : (C (G.E.B^2) : Polynomial F) = (C G.E.B)^2 := map_pow _ _ _ + rw [hC, phiPoly, taPoly, tPoly] + ring + +/-- `Z·X² + 1` is separable: its Bézout certificate against its derivative +`2·Z·X` has the constant `2`. -/ +theorem tPoly_add_one_separable : (G.tPoly + 1).Separable := by + have h2 : (2 : F) ≠ 0 := Ring.two_ne_zero G.ringChar_ne_two + have hd : (G.tPoly + 1).derivative = 2 * C G.Z * X := by + simp only [tPoly, derivative_add, derivative_mul, derivative_pow, + derivative_C, derivative_X, derivative_one, Nat.cast_ofNat, map_ofNat] + ring + rw [Polynomial.separable_def, hd] + refine isCoprime_of_bezout (u := 2) (v := -X) (c := 2) h2 ?_ + have hC2 : (C (2 : F) : Polynomial F) = 2 := map_ofNat _ 2 + rw [tPoly, hC2] + ring + /-! ## Separability of the cubic, by Bézout certificate The cofactors were computed by `xgcd` in `scripts/weil-derivation-checks.sage`; the identity's constant is `A³·B²·(4·A³ + 27·B²)`, nonzero exactly from the standing assumptions plus ellipticity. -/ +/-- The cubic `φ(T) = B²·(T + 1)³ + A³·T²` through which the core factors: +`Φ = φ ∘ ta` (design doc §2, the squarefreeness lemma). -/ +noncomputable def phiCubic : Polynomial F := + (C G.E.B)^2 * (X + 1)^3 + (C G.E.A)^3 * X^2 + +/-- `Φ` factors through `ta`: `Φ = φ ∘ ta`. -/ +theorem phiPoly_eq_comp : G.phiPoly = G.phiCubic.comp G.taPoly := by + simp only [phiPoly, phiCubic, add_comp, mul_comp, pow_comp, C_comp, X_comp, + one_comp] + /-- The derivative of the cubic `φ`. -/ theorem phiCubic_derivative : G.phiCubic.derivative = 3*(C G.E.B)^2 * (X + 1)^2 + 2*(C G.E.A)^3 * X := by @@ -175,11 +231,6 @@ theorem _root_.CompElliptic.Hashing.isCoprime_C_of_ne_zero IsCoprime p (C c) := ⟨0, C c⁻¹, by simp [← C_mul, inv_mul_cancel₀ hc]⟩ -/-- `Φ` has constant coefficient `B²`: it is coprime to `X`. This is the -design doc's `φ(ta(0)) = B² ≠ 0` case of the squarefreeness lemma. -/ -theorem phiPoly_coeff_zero : G.phiPoly.coeff 0 = G.E.B^2 := by - rw [coeff_zero_eq_eval_zero, G.eval_phiPoly, G.phiCore_zero] - /-- The even-powers polynomial `Ψ` with `64·Φ = Ψ(2·Z·X² + 1)`: the core, re-expanded around the second critical locus of `ta`. Its constant term is the ellipticity `4·A³ + 27·B²` — the design doc's `64·φ(-1/4)`. -/ @@ -258,57 +309,7 @@ theorem phiPoly_squarefree (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : Squarefree G.phiPoly := (G.phiPoly_separable hdisc).squarefree -/-! ## The models: squarefree of degree 14 - -`H_j = d_j·(Z·u²+1)·Φ` — the objects the cited hyperelliptic genus formula -is applied to. -/ - -/-- The first model `H₁ = d₁·(Z·u²+1)·Φ` as a polynomial in `u`. -/ -noncomputable def model1Poly : Polynomial F := - C G.twist1 * ((G.tPoly + 1) * G.phiPoly) - -/-- The second model `H₂ = d₂·(Z·u²+1)·Φ` as a polynomial in `u`. -/ -noncomputable def model2Poly : Polynomial F := - C G.twist2 * ((G.tPoly + 1) * G.phiPoly) - -/-- `model1Poly` evaluates to the pointwise model `model1`. -/ -theorem eval_model1Poly (u : F) : G.model1Poly.eval u = G.model1 u := by - simp only [model1Poly, model1, tPoly, eval_mul, eval_add, eval_C, eval_X, - eval_pow, eval_one, G.eval_phiPoly] - ring - -/-- `model2Poly` evaluates to the pointwise model `model2`. -/ -theorem eval_model2Poly (u : F) : G.model2Poly.eval u = G.model2 u := by - simp only [model2Poly, model2, tPoly, eval_mul, eval_add, eval_C, eval_X, - eval_pow, eval_one, G.eval_phiPoly] - ring - -/-- `Z·X² + 1` is separable: its Bézout certificate against its derivative -`2·Z·X` has the constant `2`. -/ -theorem tPoly_add_one_separable : (G.tPoly + 1).Separable := by - have h2 : (2 : F) ≠ 0 := Ring.two_ne_zero G.ringChar_ne_two - have hd : (G.tPoly + 1).derivative = 2 * C G.Z * X := by - simp only [tPoly, derivative_add, derivative_mul, derivative_pow, - derivative_C, derivative_X, derivative_one, Nat.cast_ofNat, map_ofNat] - ring - rw [Polynomial.separable_def, hd] - refine isCoprime_of_bezout (u := 2) (v := -X) (c := 2) h2 ?_ - have hC2 : (C (2 : F) : Polynomial F) = 2 := map_ofNat _ 2 - rw [tPoly, hC2] - ring - -/-- `Φ` is coprime to `Z·X² + 1`: modulo that factor, `ta = 0` and -`Φ = B²`. This is the design doc's coprimality of `Φ` with the models' -quadratic factor. -/ -theorem phiPoly_isCoprime_tPoly_add_one : - IsCoprime G.phiPoly (G.tPoly + 1) := by - refine isCoprime_of_bezout (u := 1) - (v := -(G.tPoly * ((C G.E.B)^2 * G.taPoly^2 - + (3*(C G.E.B)^2 + (C G.E.A)^3) * G.taPoly + 3*(C G.E.B)^2))) - (c := G.E.B^2) (pow_ne_zero 2 G.E.B_nonzero) ?_ - have hC : (C (G.E.B^2) : Polynomial F) = (C G.E.B)^2 := map_pow _ _ _ - rw [hC, phiPoly, taPoly, tPoly] - ring +/-! ## The models are squarefree of degree 14 -/ /-- **The first model is squarefree**: a unit times the product of the two coprime separable factors `Z·X² + 1` and `Φ`. -/ @@ -356,6 +357,26 @@ theorem model2Poly_natDegree : G.model2Poly.natDegree = 14 := by | exact G.Z_nonzero | exact G.twist2_ne_zero +/-! ## The fibre over `w = 0` -/ + +/-- `g(-B/A) = -(B/A)³`: the curve equation at the abscissa of the two +points over `w = 0`. -/ +theorem eval_g_neg_B_div_A : + (-(G.E.B/G.E.A))^3 + G.E.A * -(G.E.B/G.E.A) + G.E.B + = -(G.E.B/G.E.A)^3 := by + have hA := G.A_nonzero + field_simp + ring + +/-- `g(-B/A) ≠ 0`: the two points over `w = 0` have nonzero ordinate, so +`w` vanishes simply at each — the input that makes the Eisenstein pattern +mean total ramification in the cited argument. -/ +theorem g_neg_B_div_A_ne_zero : + (-(G.E.B/G.E.A))^3 + G.E.A * -(G.E.B/G.E.A) + G.E.B ≠ 0 := by + rw [G.eval_g_neg_B_div_A] + exact neg_ne_zero.mpr (pow_ne_zero 3 + (div_ne_zero G.E.B_nonzero G.A_nonzero)) + /-! ## The branch quartics are Eisenstein at `w = 0` The design doc's §3 works over the function field of the curve, where `w` @@ -465,26 +486,6 @@ theorem p1RecipPoly_isEisensteinAt : exact not_X_sq_dvd (C_ne_zero.mpr (pow_ne_zero 2 G.Z_nonzero)) (natDegree_C _) -/-! ## The fibre over `w = 0` -/ - -/-- `g(-B/A) = -(B/A)³`: the curve equation at the abscissa of the two -points over `w = 0`. -/ -theorem eval_g_neg_B_div_A : - (-(G.E.B/G.E.A))^3 + G.E.A * -(G.E.B/G.E.A) + G.E.B - = -(G.E.B/G.E.A)^3 := by - have hA := G.A_nonzero - field_simp - ring - -/-- `g(-B/A) ≠ 0`: the two points over `w = 0` have nonzero ordinate, so -`w` vanishes simply at each — the input that makes the Eisenstein pattern -mean total ramification in the cited argument. -/ -theorem g_neg_B_div_A_ne_zero : - (-(G.E.B/G.E.A))^3 + G.E.A * -(G.E.B/G.E.A) + G.E.B ≠ 0 := by - rw [G.eval_g_neg_B_div_A] - exact neg_ne_zero.mpr (pow_ne_zero 3 - (div_ne_zero G.E.B_nonzero G.A_nonzero)) - /-! ## The monodromy square exclusions Design doc §3 pins the monodromy group at full `D₄`: the biquadratic From 572fd66ba0e416ba03a6ee55224fc7b79ea63af7 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Wed, 19 Aug 2026 00:51:21 +0100 Subject: [PATCH 14/25] meta: retire the stale #28 tracking pointers MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- CompElliptic/Hashing/BranchCovers.lean | 3 +-- CompElliptic/Hashing/WeilInstance.lean | 7 ++----- CompElliptic/Hashing/WellDistributed.lean | 9 +++++---- 3 files changed, 8 insertions(+), 11 deletions(-) diff --git a/CompElliptic/Hashing/BranchCovers.lean b/CompElliptic/Hashing/BranchCovers.lean index 66cce4e..287eed8 100644 --- a/CompElliptic/Hashing/BranchCovers.lean +++ b/CompElliptic/Hashing/BranchCovers.lean @@ -27,8 +27,7 @@ form: `g (x₂ u) = (Z·u²)³ · g (x₁ u)`. The notation follows `design/weil-constant-derivation.md` §2, which derives the Weil character-sum bound for the deployed mappings from these models; -formal consumption of that bound is tracked at -. +`WeilInstance.lean` assembles the formal consumption. On a field where `-1` is a square (both Pasta base fields), `Z·u² + 1` never vanishes (`Zuu_add_one_ne_zero`), so the scalings vanish only at `u = 0` and diff --git a/CompElliptic/Hashing/WeilInstance.lean b/CompElliptic/Hashing/WeilInstance.lean index 83c23f1..83c076f 100644 --- a/CompElliptic/Hashing/WeilInstance.lean +++ b/CompElliptic/Hashing/WeilInstance.lean @@ -22,11 +22,8 @@ not factor through a nontrivial unramified subcover. The branch covers have genus 6, and their total ramification over `A·x + B = 0` rules every unramified subcover out; both derivations are cited from `design/weil-constant-derivation.md` §2–3. Mathlib does not yet have the -vocabulary to state them (genus, places, covers of curves), and that -vocabulary is out of scope for -, which covers -formalizing the computation and the paper proof's supporting facts; the -vocabulary itself, on the Riemann's-inequality route, is +vocabulary to state them (genus, places, covers of curves); the +vocabulary, on the Riemann's-inequality route, is tracked at . The derivation is parametric in the per-cover constant `c`: inputs at diff --git a/CompElliptic/Hashing/WellDistributed.lean b/CompElliptic/Hashing/WellDistributed.lean index ddca2a9..41c8bb1 100644 --- a/CompElliptic/Hashing/WellDistributed.lean +++ b/CompElliptic/Hashing/WellDistributed.lean @@ -109,10 +109,11 @@ is the elementary, orthogonality-only content of `CharacterSum.lean`. the deployed sizes with margin `≈ 2^{127}`. The bound is proven in `design/weil-constant-derivation.md`, modulo results cited there as established mathematics (Weil's theorem in the form of FFSTV's Lemma 1 - and Theorem 3, and standard hyperelliptic point bookkeeping); - formalizing the calculation in Lean is what remains of - . Separately, - `WeilBounded` itself is an external input to the formalization. + and Theorem 3, and standard hyperelliptic point bookkeeping). The + calculation and the paper proof's supporting facts are formalized + (`Hashing/BranchCovers.lean`, `Hashing/WeilInstance.lean`, + `Hashing/WeilSupport.lean`). Separately, `WeilBounded` itself is an + external input to the formalization. -/ namespace CompElliptic.Hashing From 309d4e4c3c24faf5c581f2e64e446b2a50922703 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Wed, 19 Aug 2026 01:07:21 +0100 Subject: [PATCH 15/25] docs: docstrings for the remaining undocumented declarations `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 --- CompElliptic/Fields/Jubjub.lean | 4 +++- CompElliptic/Fields/Pasta.lean | 8 ++++++-- CompElliptic/Hashing/FibreBound.lean | 2 ++ scripts/gen_jubjub.py | 4 +++- scripts/gen_pasta.py | 8 ++++++-- scripts/pratt.py | 7 +++++-- 6 files changed, 25 insertions(+), 8 deletions(-) diff --git a/CompElliptic/Fields/Jubjub.lean b/CompElliptic/Fields/Jubjub.lean index 6f9dcd8..bc8d06d 100644 --- a/CompElliptic/Fields/Jubjub.lean +++ b/CompElliptic/Fields/Jubjub.lean @@ -19,11 +19,13 @@ base field (the BLS12-381 scalar field) are not defined here. namespace CompElliptic.Fields.Jubjub --- Jubjub scalar field ℓ (the prime-order subgroup order). +/-- The order `ℓ` of the Jubjub scalar field (the prime-order subgroup order). -/ @[reducible] def JUBJUB_SCALAR_CARD : Nat := 0xe7db4ea6533afa906673b0101343b00a6682093ccc81082d0970e5ed6f72cb7 +/-- The Jubjub scalar field `F_ℓ`. -/ abbrev JubjubScalarField := ZMod JUBJUB_SCALAR_CARD +/-- `ℓ` is prime, by a Pratt certificate. -/ theorem JUBJUB_SCALAR_is_prime : Nat.Prime JUBJUB_SCALAR_CARD := by unfold JUBJUB_SCALAR_CARD refine PrattCertificate'.out (p := 6554484396890773809930967563523245729705921265872317281365359162392183254199) ⟨6, (by reduce_mod_char), ?_⟩ diff --git a/CompElliptic/Fields/Pasta.lean b/CompElliptic/Fields/Pasta.lean index 4bcdc89..489a4f8 100644 --- a/CompElliptic/Fields/Pasta.lean +++ b/CompElliptic/Fields/Pasta.lean @@ -19,11 +19,13 @@ factorizations of `p-1` and `q-1` (PARI/GP); see also https://github.com/zcash/p namespace CompElliptic.Fields.Pasta --- Pallas base field p (= Vesta scalar field). +/-- The order `p` of the Pallas base field (= the Vesta scalar field). -/ @[reducible] def PALLAS_BASE_CARD : Nat := 0x40000000000000000000000000000000224698fc094cf91b992d30ed00000001 +/-- The Pallas base field `F_p` (= the Vesta scalar field). -/ abbrev PallasBaseField := ZMod PALLAS_BASE_CARD +/-- `p` is prime, by a Pratt certificate. -/ theorem PALLAS_BASE_is_prime : Nat.Prime PALLAS_BASE_CARD := by unfold PALLAS_BASE_CARD refine PrattCertificate'.out (p := 28948022309329048855892746252171976963363056481941560715954676764349967630337) ⟨5, (by reduce_mod_char), ?_⟩ @@ -90,11 +92,13 @@ theorem PALLAS_BASE_is_prime : Nat.Prime PALLAS_BASE_CARD := by instance : Fact (Nat.Prime PALLAS_BASE_CARD) := ⟨PALLAS_BASE_is_prime⟩ instance : Field PallasBaseField := ZMod.instField PALLAS_BASE_CARD --- Pallas scalar field q (= Vesta base field). +/-- The order `q` of the Pallas scalar field (= the Vesta base field). -/ @[reducible] def PALLAS_SCALAR_CARD : Nat := 0x40000000000000000000000000000000224698fc0994a8dd8c46eb2100000001 +/-- The Pallas scalar field `F_q` (= the Vesta base field). -/ abbrev PallasScalarField := ZMod PALLAS_SCALAR_CARD +/-- `q` is prime, by a Pratt certificate. -/ theorem PALLAS_SCALAR_is_prime : Nat.Prime PALLAS_SCALAR_CARD := by unfold PALLAS_SCALAR_CARD refine PrattCertificate'.out (p := 28948022309329048855892746252171976963363056481941647379679742748393362948097) ⟨5, (by reduce_mod_char), ?_⟩ diff --git a/CompElliptic/Hashing/FibreBound.lean b/CompElliptic/Hashing/FibreBound.lean index 919a523..1e9459e 100644 --- a/CompElliptic/Hashing/FibreBound.lean +++ b/CompElliptic/Hashing/FibreBound.lean @@ -111,6 +111,8 @@ theorem fibrePoly_fst_ne_zero (G : SSWUParams F) (x : F) : theorem fibrePoly_ne_zero (G : SSWUParams F) (x : F) : G.fibrePoly x ≠ 0 := mul_ne_zero (G.fibrePoly_fst_ne_zero x) (G.fibrePoly_snd_ne_zero x) +/-- `Φ_x` has degree at most 10: its first factor has degree at most 4, +and its second exactly 6 (`fibrePoly_snd_natDegree`). -/ theorem fibrePoly_natDegree_le (G : SSWUParams F) (x : F) : (G.fibrePoly x).natDegree ≤ 10 := by refine natDegree_mul_le.trans ?_ diff --git a/scripts/gen_jubjub.py b/scripts/gen_jubjub.py index be21966..912a9ba 100644 --- a/scripts/gen_jubjub.py +++ b/scripts/gen_jubjub.py @@ -56,6 +56,8 @@ if __name__ == "__main__": out = HEADER out += field_block("JUBJUB_SCALAR", L, "JubjubScalarField", - "Jubjub scalar field ℓ (the prime-order subgroup order).") + "The order `ℓ` of the Jubjub scalar field (the prime-order subgroup order).", + "The Jubjub scalar field `F_ℓ`.", + "`ℓ` is prime, by a Pratt certificate.") out += FOOTER print(out, end="") diff --git a/scripts/gen_pasta.py b/scripts/gen_pasta.py index e5ccd02..d76a1ab 100644 --- a/scripts/gen_pasta.py +++ b/scripts/gen_pasta.py @@ -88,8 +88,12 @@ def vestaBase : TonelliShanks VestaBaseField where if __name__ == "__main__": out = HEADER out += field_block("PALLAS_BASE", P, "PallasBaseField", - "Pallas base field p (= Vesta scalar field).") + "The order `p` of the Pallas base field (= the Vesta scalar field).", + "The Pallas base field `F_p` (= the Vesta scalar field).", + "`p` is prime, by a Pratt certificate.") out += field_block("PALLAS_SCALAR", Q, "PallasScalarField", - "Pallas scalar field q (= Vesta base field).") + "The order `q` of the Pallas scalar field (= the Vesta base field).", + "The Pallas scalar field `F_q` (= the Vesta base field).", + "`q` is prime, by a Pratt certificate.") out += FOOTER print(out, end="") diff --git a/scripts/pratt.py b/scripts/pratt.py index a3cba3a..2026b2e 100644 --- a/scripts/pratt.py +++ b/scripts/pratt.py @@ -69,11 +69,14 @@ def theorem(name: str, card: int) -> str: return f"theorem {name}_is_prime : Nat.Prime {name}_CARD := by\n unfold {name}_CARD\n{body}" -def field_block(name: str, card: int, fieldabbrev: str, doc: str) -> str: +def field_block(name: str, card: int, fieldabbrev: str, carddoc: str, + fielddoc: str, primedoc: str) -> str: return ( - f"\n-- {doc}\n" + f"\n/-- {carddoc} -/\n" f"@[reducible] def {name}_CARD : Nat := 0x{card:x}\n\n" + f"/-- {fielddoc} -/\n" f"abbrev {fieldabbrev} := ZMod {name}_CARD\n\n" + f"/-- {primedoc} -/\n" f"{theorem(name, card)}\n\n" f"instance : Fact (Nat.Prime {name}_CARD) := ⟨{name}_is_prime⟩\n" f"instance : Field {fieldabbrev} := ZMod.instField {name}_CARD\n" From b89d595d58a89f67ee5e8c85a9e123b34d148f49 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Wed, 19 Aug 2026 01:38:55 +0100 Subject: [PATCH 16/25] meta: the deployed constant exists; update TwoTermUniformity's estimates MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- CompElliptic/Hashing/TwoTermUniformity.lean | 22 ++++++++------------- 1 file changed, 8 insertions(+), 14 deletions(-) diff --git a/CompElliptic/Hashing/TwoTermUniformity.lean b/CompElliptic/Hashing/TwoTermUniformity.lean index 84e2220..ccab9bc 100644 --- a/CompElliptic/Hashing/TwoTermUniformity.lean +++ b/CompElliptic/Hashing/TwoTermUniformity.lean @@ -68,14 +68,9 @@ multiplication in the frequency domain: nontrivial frequencies contributes at most `(C²·#F)²`. * `sq_sum_abs_dev_le` and `sq_sum_abs_prob_dev_le`: Cauchy–Schwarz converts the squared-deviation bound into (the square of) the L¹ deviation — twice the - statistical distance. At the deployed sizes (`#G ≈ #F ≈ 2^{254}`), a constant - of the order FFSTV obtain for a sibling encoding (`C = 52`) would put the - statistical distance near `2^{-116}`. No constant has been derived for the - deployed mappings themselves: FFSTV's Theorem 6 treats simplified SWU with - `Z = -1` over fields of size `≡ 3 (mod 4)` under a quadratic-residue sign - rule, and the deployed variant differs in all three respects, so the genus - computation behind the constant remains to be redone for its branch curves - (see `WellDistributed.lean`). + statistical distance. At the deployed sizes (`#G ≈ #F ≈ 2^{254}`), the + derived constant `C = 21/2` puts the statistical distance near `2^{-120}` + (`design/weil-constant-derivation.md`; see `WellDistributed.lean`). Everything here is stated for an arbitrary function `f : F → G` from a finite type into a finite abelian group; oddness of the mapping and the elliptic curve @@ -341,12 +336,11 @@ theorem sq_sum_abs_dev_le (f : F → G) {C : ℝ} (h : WeilBounded f C) : form, `pairCount f Q / (#F)²` is the chance the two-term hash outputs `Q`, and `1/#G` is the uniform chance, so the total variation distance is half of `∑ Q, |probability - uniform|`. This theorem bounds that sum's square by -`(#G - 1)·C⁴/(#F)²`. At the deployed sizes (`#G ≈ #F ≈ 2^{254}`), a constant -of the order FFSTV obtain for a sibling encoding (`C = 52`) would make the -statistical distance about `2^{-116}`; no constant has been derived for the -deployed mappings (see `WellDistributed.lean`). The two-term hash output is -therefore indistinguishable from a uniformly random group element up to that -error, which is the quantitative content of "the construction repairs the +`(#G - 1)·C⁴/(#F)²`. At the deployed sizes (`#G ≈ #F ≈ 2^{254}`), the derived +constant `C = 21/2` makes the statistical distance about `2^{-120}` (see +`WellDistributed.lean`). The two-term hash output is therefore +indistinguishable from a uniformly random group element up to that error, +which is the quantitative content of "the construction repairs the non-uniformity of a single evaluation of `f`". -/ theorem sq_sum_abs_prob_dev_le [Nonempty F] (f : F → G) {C : ℝ} (h : WeilBounded f C) : From 4e8514025077294bf5a8e65f479b59cdea2e54f2 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Wed, 19 Aug 2026 02:12:01 +0100 Subject: [PATCH 17/25] ci: run the Weil-derivation sage checks in the sage job MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- .github/workflows/ci.yml | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 47756db..4d3bc6f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -73,17 +73,19 @@ jobs: - name: Fail if the regenerated files differ from the committed ones run: git diff --exit-code CompElliptic/Fields/Pasta.lean CompElliptic/Fields/Jubjub.lean - velu-certificates: - name: Vélu certificates reproduce + sage-checks: + name: sage checks - Vélu certificates and Weil-derivation identities runs-on: ubuntu-latest steps: - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 with: persist-credentials: false - # Sage pinned to the version that generated the committed certificates: - # Singular's `lift` output (the emitted cofactors) can differ between - # versions, so byte-reproducibility needs the same engine as the local - # regeneration. + # One environment for both sage steps. Sage is pinned to the version that + # generated the committed certificates: Singular's `lift` output (the + # emitted cofactors) can differ between versions, so byte-reproducibility + # needs the same engine as the local regeneration. (The Weil-derivation + # checks are exact symbolic assertions over ℚ(a, b, z), so any engine + # verifies those.) - uses: mamba-org/setup-micromamba@f457c30a868e4760d3a6fcea5f25dc655b8edf39 # v3.2.1 with: environment-name: sage @@ -97,6 +99,9 @@ jobs: run: sage scripts/gen_velu_certificates.sage - name: Fail if the regenerated section differs from the committed one run: git diff --exit-code CompElliptic/Isogenies/VeluCertificates.lean + - name: Check the design doc's symbolic identities and certificates + shell: bash -el {0} + run: sage scripts/weil-derivation-checks.sage native-lane: name: FastFieldNative lane is core-only From 4a7540ae8bed6f09f127f52a796a3df1bbc5cc1c Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Wed, 19 Aug 2026 13:07:31 +0100 Subject: [PATCH 18/25] scripts: the small-curve branch statistics, exactly MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- .github/workflows/ci.yml | 3 + scripts/check_sswu_small_curves.sage | 87 ++++++++++++++++++++++++++++ 2 files changed, 90 insertions(+) create mode 100644 scripts/check_sswu_small_curves.sage diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4d3bc6f..03e792c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -102,6 +102,9 @@ jobs: - name: Check the design doc's symbolic identities and certificates shell: bash -el {0} run: sage scripts/weil-derivation-checks.sage + - name: Confirm the branch statistics on small curves + shell: bash -el {0} + run: sage scripts/check_sswu_small_curves.sage native-lane: name: FastFieldNative lane is core-only diff --git a/scripts/check_sswu_small_curves.sage b/scripts/check_sswu_small_curves.sage new file mode 100644 index 0000000..9faae97 --- /dev/null +++ b/scripts/check_sswu_small_curves.sage @@ -0,0 +1,87 @@ +# Exact simplified-SWU branch statistics on small curves. +# +# The ironwood book's group-hash page makes three heuristic claims about +# the deployed-shape mapping, confirmed here by exhaustive computation on +# small instances (q ≡ 1 (mod 4), A·B ≠ 0, odd prime order, -A·B a +# nonsquare, Z the first nonsquare ∉ {0, -1}): +# +# * the images of the two branches f₁ and f₂ coincide, apart from a +# negligible proportion of exceptional points (the single-branch +# count is reported, not asserted — we have not proven a bound on +# the exceptional cases; it is zero at every instance here); +# * about 3/8 of the group is reached, with about 1/8 of the points +# having 4 preimages and about 1/4 having 2 (asserted to within +# 3/√q, the Lang–Weil-shaped error; the constants are not +# optimized); +# * every reached point other than 𝒪 has exactly 2 or 4 preimages +# (asserted exactly: a target's quadratic has 1 or 2 realizable +# roots, each contributing one preimage per branch). +# +# The w = 0 fibre is empty when -A·B is a nonsquare, so the only +# exceptional output is 𝒪 (from the repaired input u = 0). + +def sgn0(x): + return Integer(x) % 2 + +def find_instance(q): + F = GF(q) + for a in range(1, 50): + for b in range(1, 50): + A, B = F(a), F(b) + if 4*A^3 + 27*B^2 == 0: + continue + E = EllipticCurve(F, [A, B]) + N = E.order() + if not (N.is_prime() and N % 2 == 1): + continue + if (-A*B).is_square(): + continue + Z = next(F(z) for z in range(2, q) + if not F(z).is_square() and F(z) != F(-1)) + return (F, E, A, B, Z, N) + return None + +def sswu(F, E, A, B, Z, u): + """The deployed-shape mapping, and which branch produced the point.""" + if u == 0: + return (E(0), None) # the zero-repaired exceptional input + t = Z*u^2 + ta = t^2 + t + assert ta != 0 # t = -1 has no solutions for q ≡ 1 (mod 4) + x1 = B*(ta + 1) / (A*(-ta)) + for branch, x in ((1, x1), (2, t*x1)): + g = x^3 + A*x + B + assert g != 0 # a root would be rational 2-torsion + if g.is_square(): + y = g.sqrt() + if sgn0(y) != sgn0(u): + y = -y + return (E((x, y)), branch) + raise AssertionError("neither branch value is a square") + +for q in [101, 149, 197, 401, 601, 1009, 10009]: + assert q % 4 == 1 + inst = find_instance(q) + assert inst is not None, f"no instance found for q = {q}" + F, E, A, B, Z, N = inst + hist = {} + branches = {} + for u in F: + P, branch = sswu(F, E, A, B, Z, u) + if branch is None: + continue + hist[P] = hist.get(P, 0) + 1 + branches.setdefault(P, set()).add(branch) + assert set(hist.values()) <= {2, 4}, sorted(set(hist.values())) + reached = len(hist) + single = sum(1 for s in branches.values() if len(s) == 1) + four = sum(1 for c in hist.values() if c == 4) + two = reached - four + tol = 3/sqrt(q) + for count, target in [(reached, 3/8), (four, 1/8), (two, 1/4)]: + assert abs(count/N - target) <= tol, (q, count, N, target) + print(f"q={q} A={A} B={B} Z={Z} N={N}: reached {reached}/{N} " + f"(3/8·N ≈ {float(3*N/8):.0f}), 4-preimage {four} (N/8 ≈ {float(N/8):.0f}), " + f"2-preimage {two} (N/4 ≈ {float(N/4):.0f}), single-branch points {single}") + +print("small-curve branch statistics: OK") From 17f75ab5fb5ad8ceaa6b508d1ed5e288186c8236 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Wed, 19 Aug 2026 13:17:01 +0100 Subject: [PATCH 19/25] scripts: rename the Weil-derivation checks to the check_* convention 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 --- .github/workflows/ci.yml | 2 +- CompElliptic/Hashing/WeilSupport.lean | 14 +++++++------- design/weil-constant-derivation.md | 6 +++--- ...ion-checks.sage => check_weil_derivations.sage} | 0 4 files changed, 11 insertions(+), 11 deletions(-) rename scripts/{weil-derivation-checks.sage => check_weil_derivations.sage} (100%) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 03e792c..dbc1863 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -101,7 +101,7 @@ jobs: run: git diff --exit-code CompElliptic/Isogenies/VeluCertificates.lean - name: Check the design doc's symbolic identities and certificates shell: bash -el {0} - run: sage scripts/weil-derivation-checks.sage + run: sage scripts/check_weil_derivations.sage - name: Confirm the branch statistics on small curves shell: bash -el {0} run: sage scripts/check_sswu_small_curves.sage diff --git a/CompElliptic/Hashing/WeilSupport.lean b/CompElliptic/Hashing/WeilSupport.lean index 009b6ee..90ee58e 100644 --- a/CompElliptic/Hashing/WeilSupport.lean +++ b/CompElliptic/Hashing/WeilSupport.lean @@ -166,7 +166,7 @@ theorem tPoly_add_one_separable : (G.tPoly + 1).Separable := by /-! ## Separability of the cubic, by Bézout certificate -The cofactors were computed by `xgcd` in `scripts/weil-derivation-checks.sage`; +The cofactors were computed by `xgcd` in `scripts/check_weil_derivations.sage`; the identity's constant is `A³·B²·(4·A³ + 27·B²)`, nonzero exactly from the standing assumptions plus ellipticity. -/ @@ -189,7 +189,7 @@ theorem phiCubic_derivative : /-- **The cubic `φ` is separable**, by the Bézout certificate `s·φ + t·φ′ = A³·B²·(4·A³ + 27·B²)` computed in -`scripts/weil-derivation-checks.sage`: the identity's constant is a product +`scripts/check_weil_derivations.sage`: the identity's constant is a product of exactly the standing nonzero quantities. -/ theorem phiCubic_separable (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : G.phiCubic.Separable := by @@ -246,7 +246,7 @@ theorem psiPoly_coeff_zero : simp [psiPoly] /-- The re-expansion `64·Φ = Ψ(2·Z·X² + 1)`, checked symbolically in -`scripts/weil-derivation-checks.sage`. -/ +`scripts/check_weil_derivations.sage`. -/ theorem phiPoly_64_eq : 64 * G.phiPoly = G.psiPoly.comp (2 * C G.Z * X^2 + 1) := by simp only [psiPoly, phiPoly, taPoly, tPoly, add_comp, mul_comp, pow_comp, @@ -503,7 +503,7 @@ the quadratic algebra `K[Y]/(Y² - ĝ)` over `K = F_q(x)`: divisor parity. The Kappe–Warren reduction to the two square classes stays cited; it is -checked symbolically in `scripts/weil-derivation-checks.sage`, along +checked symbolically in `scripts/check_weil_derivations.sage`, along with the Bézout certificates used below. -/ /-- A rational square root of a polynomial is a polynomial: `F[X]` is @@ -625,7 +625,7 @@ noncomputable def gPoly : Polynomial F := X^3 + C G.E.A * X + C G.E.B /-- `g` is separable, by the Bézout certificate `(27·B - 18·A·X)·g + (6·A·X² - 9·B·X + 4·A²)·g′ = 4·A³ + 27·B²` -(checked in `scripts/weil-derivation-checks.sage`): the constant is +(checked in `scripts/check_weil_derivations.sage`): the constant is nonzero exactly by ellipticity. -/ theorem gPoly_separable (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : G.gPoly.Separable := by @@ -728,7 +728,7 @@ noncomputable def c4TestPoly : Polynomial F := /-- **The V₄ exclusion** (design doc §3): `B·(A·x + B)` is not a square in the function field. The coprimality certificate is `(A²·X² - A·B·X + (B² + A³))·(A·X + B) - A³·g = B³` (checked in -`scripts/weil-derivation-checks.sage`). -/ +`scripts/check_weil_derivations.sage`). -/ theorem v4TestPoly_not_isSquare (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : ¬ IsSquare (AdjoinRoot.of (X^2 - C (algebraMap (Polynomial F) (RatFunc F) G.gPoly)) @@ -751,7 +751,7 @@ theorem v4TestPoly_not_isSquare (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : /-- **The C₄ exclusion** (design doc §3): `B·(A·x - 3·B)` is not a square in the function field. The coprimality certificate is `A³·g - (A²·X² + 3·A·B·X + (9·B² + A³))·(A·X - 3·B) = B·(4·A³ + 27·B²)` -(checked in `scripts/weil-derivation-checks.sage`); its constant is again +(checked in `scripts/check_weil_derivations.sage`); its constant is again a product of the standing nonzero quantities. -/ theorem c4TestPoly_not_isSquare (hdisc : 4*G.E.A^3 + 27*G.E.B^2 ≠ 0) : ¬ IsSquare (AdjoinRoot.of diff --git a/design/weil-constant-derivation.md b/design/weil-constant-derivation.md index 2952bd2..562d279 100644 --- a/design/weil-constant-derivation.md +++ b/design/weil-constant-derivation.md @@ -17,7 +17,7 @@ Status: this document is a proof of the bound, modulo results cited as established mathematics: Weil's theorem in the form of FFSTV's Lemma 1 and Theorem 3, and the standard point bookkeeping for hyperelliptic models [Galbraith, ch. 10]. The symbolic identities it relies on are -checked by `scripts/weil-derivation-checks.sage`; the per-instance +checked by `scripts/check_weil_derivations.sage`; the per-instance facts (the empty w = 0 fibre, the Frobenius statistics, the square-class witnesses) by `weilbound.sage`. The calculation from the per-cover Weil inputs to the deployed constants is machine-checked @@ -199,7 +199,7 @@ The lemma is `phiPoly_squarefree` in `Hashing/WeilSupport.lean` degree exactly 14 (`model1Poly_natDegree`, `model2Poly_natDegree`). The discriminant factorization and both critical values are checked -symbolically in `scripts/weil-derivation-checks.sage`. So each C_j is +symbolically in `scripts/check_weil_derivations.sage`. So each C_j is hyperelliptic of genus ⌊(14 − 1)/2⌋ = 6, for **every** valid parameter set — the pleasant surprise being that the two quantities the argument needs to be nonzero are the curve discriminant and A·B, both already @@ -242,7 +242,7 @@ V₄ (three intermediate quadratics) only if the normalized constant term is a square in F_q(E′), and to C₄ only if q·(p² − 4q) is. For both quartics, these reduce to the same two classes: B·(A·x + B) and B·(A·x − 3·B) being squares in F_q(E′). (The reductions are checked -symbolically in `scripts/weil-derivation-checks.sage`.) Both fail by +symbolically in `scripts/check_weil_derivations.sage`.) Both fail by divisor parity: each class has two simple zeros and a double pole, so its divisor is not twice a divisor. So the monodromy is full D₄, and the v = u² subcover is the unique intermediate. This is consistent diff --git a/scripts/weil-derivation-checks.sage b/scripts/check_weil_derivations.sage similarity index 100% rename from scripts/weil-derivation-checks.sage rename to scripts/check_weil_derivations.sage From 058fd1baa91f14e17bc2f725150c5b9619eba56f Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Wed, 19 Aug 2026 14:42:40 +0100 Subject: [PATCH 20/25] meta: the absorption margin is 2^{126}, not 2^{127} MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit (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 --- CompElliptic/Hashing/WellDistributed.lean | 2 +- design/weil-constant-derivation.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CompElliptic/Hashing/WellDistributed.lean b/CompElliptic/Hashing/WellDistributed.lean index 41c8bb1..293ff2d 100644 --- a/CompElliptic/Hashing/WellDistributed.lean +++ b/CompElliptic/Hashing/WellDistributed.lean @@ -106,7 +106,7 @@ is the elementary, orthogonality-only content of `CharacterSum.lean`. `-1/Z` is a nonsquare whenever `Z` is, so the `t = -1` fibre is empty). The result, for both iso-curves, is `|S_f(χ)| ≤ 10·√q + 1` (the script's coarser audit gives `+ 3`), and `C = 21/2` absorbs the additive term at - the deployed sizes with margin `≈ 2^{127}`. The bound is proven in + the deployed sizes with margin `≈ 2^{126}`. The bound is proven in `design/weil-constant-derivation.md`, modulo results cited there as established mathematics (Weil's theorem in the form of FFSTV's Lemma 1 and Theorem 3, and standard hyperelliptic point bookkeeping). The diff --git a/design/weil-constant-derivation.md b/design/weil-constant-derivation.md index 562d279..a1a126f 100644 --- a/design/weil-constant-derivation.md +++ b/design/weil-constant-derivation.md @@ -387,7 +387,7 @@ transfers to the full `mapToCurve` verbatim (`WeilBounded.comp`; per curve, `weilBounded_zeroRepaired_mapToCurve`). For `WeilBounded` (squared form): C = 21/2 satisfies -(10·√q + 1)² ≤ C²·q at the deployed sizes with margin ≈ 2^{127}. The +(10·√q + 1)² ≤ C²·q at the deployed sizes with margin ≈ 2^{126}. The downstream regularity distance ε ≈ C²·√(#G)/#F (the budget shape of `sum_abs_prob_dev_le`, carried to the deployed mapping by `sum_abs_prob_dev_transport_le`) comes to about 2^{-120}, improving From 964bccfbde2f09e3f12983e43d4a61aca73bc84c Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Thu, 20 Aug 2026 02:08:06 +0100 Subject: [PATCH 21/25] doc: cite FFSTV in full at its first use MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- design/weil-constant-derivation.md | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/design/weil-constant-derivation.md b/design/weil-constant-derivation.md index a1a126f..c759cbc 100644 --- a/design/weil-constant-derivation.md +++ b/design/weil-constant-derivation.md @@ -14,15 +14,17 @@ with enormous margin: (10√q + 1)² ≤ (21/2)²·q needs 10.25·q ≥ 20√q + and q > 2^{254}. Status: this document is a proof of the bound, modulo results cited as -established mathematics: Weil's theorem in the form of FFSTV's Lemma 1 -and Theorem 3, and the standard point bookkeeping for hyperelliptic -models [Galbraith, ch. 10]. The symbolic identities it relies on are -checked by `scripts/check_weil_derivations.sage`; the per-instance -facts (the empty w = 0 fibre, the Frobenius statistics, the -square-class witnesses) by `weilbound.sage`. The calculation from the -per-cover Weil inputs to the deployed constants is machine-checked -(CompElliptic's `Hashing/BranchCovers.lean`, `Hashing/WeilInstance.lean`, -and `Hashing/PastaSSWU.lean`), and so are the checkable inputs of the two +established mathematics: Weil's theorem in the form of Lemma 1 and +Theorem 3 of Farashahi–Fouque–Shparlinski–Tibouchi–Voloch +([eprint 2010/539](https://eprint.iacr.org/2010/539), "FFSTV"), and the +standard point bookkeeping for hyperelliptic models [Galbraith, ch. 10]. +The symbolic identities it relies on are checked by +`scripts/check_weil_derivations.sage`; the per-instance facts (the empty +w = 0 fibre, the Frobenius statistics, the square-class witnesses) by +`weilbound.sage`. The calculation from the per-cover Weil inputs to the +deployed constants is machine-checked (CompElliptic's +`Hashing/BranchCovers.lean`, `Hashing/WeilInstance.lean`, and +`Hashing/PastaSSWU.lean`), and so are the checkable inputs of the two cited steps (`Hashing/WeilSupport.lean`, whose facts are referenced at their points of use below; CI checks that this document references all of that file's declarations). The cited steps themselves and Weil's @@ -102,9 +104,8 @@ Throughout: q ≡ 1 (mod 4) is the base field size; E′ : y² = g(x) with g(x) = x³ + A·x + B, A·B ≠ 0, and #E′(F_q) an odd prime; Z is a nonsquare with Z ∉ {0, −1}; t = Z·u² and ta = t² + t. The deployed instances are iso-Pallas and iso-Vesta with Z = −13 and B = 1265. We -follow Farashahi–Fouque–Shparlinski–Tibouchi–Voloch -([eprint 2010/539](https://eprint.iacr.org/2010/539), "FFSTV"), -Theorem 6, adapted to these parameters and to sign-freeness. +follow FFSTV's Theorem 6, adapted to these parameters and to +sign-freeness. ## 1. The branch covers From 76b509dfa3e8cc30cdc43be50ef1b6b45cf86ca0 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Thu, 20 Aug 2026 02:40:21 +0100 Subject: [PATCH 22/25] meta: pin the design doc's cited declarations in the census MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- .github/workflows/ci.yml | 2 +- CompElliptic/TrustBoundary.lean | 132 +++++++++++++++++++++++++++++ design/weil-constant-derivation.md | 8 +- scripts/check_weil_support_refs.py | 38 +++++++-- 4 files changed, 169 insertions(+), 11 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index dbc1863..58343ef 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -123,7 +123,7 @@ jobs: - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 with: persist-credentials: false - - name: Check the supporting-facts listing against WeilSupport.lean + - name: Check the doc's references against WeilSupport.lean and the census run: scripts/check_weil_support_refs.py csimp-census: diff --git a/CompElliptic/TrustBoundary.lean b/CompElliptic/TrustBoundary.lean index fc6cb6d..9810f6b 100644 --- a/CompElliptic/TrustBoundary.lean +++ b/CompElliptic/TrustBoundary.lean @@ -6,6 +6,8 @@ Authors: Daira-Emma Hopwood -/ import CompElliptic.Curves.PastaOrder import CompElliptic.Hashing.PastaSSWU +import CompElliptic.Hashing.TwoTermUniformity +import CompElliptic.Hashing.WeilSupport import CompElliptic.Curves.Pasta.Fast.Projective import CompElliptic.Curves.Pasta.Fast.Msm import CompElliptic.Curves.Pasta.Fast.ProjectiveMontEquiv @@ -140,3 +142,133 @@ assert_axioms CompElliptic.Curves.Pasta.Fast.Msm.pippengerFastPar_eq_msm assert_axioms CompElliptic.Curves.Pasta.Fast.Msm.commitLagrangeFastWith_eq assert_axioms CompElliptic.Curves.Pasta.Fast.ProjectiveMont.pnsmulM_spec assert_axioms CompElliptic.Curves.Pasta.Fast.ProjectiveMont.msmM_spec + +/-! ## The Weil-derivation design doc's citations + +`design/weil-constant-derivation.md` is a pencil-and-paper proof whose reader relies on +every Lean declaration it cites. To avoid a resulting axiom-checking gap, every such +declaration must be pinned here (checked in CI by `scripts/check_weil_support_refs.py`). +Definitions of polynomials in these modules use Mathlib's noncomputable ones, so they +take `assert_axioms` like the theorems and `Prop`-shaped definitions. -/ + +/-! ### The abscissae, branch covers, and models (`Hashing/BranchCovers.lean`, +`Hashing/FibreBound.lean`, `Hashing/SimplifiedSWU.lean`, `Hashing/SignedLift.lean`) -/ + +assert_computable CompElliptic.Hashing.SSWUParams.x1 +assert_computable CompElliptic.Hashing.SSWUParams.x2 +assert_computable CompElliptic.Hashing.SSWUParams.phiCore +assert_computable CompElliptic.Hashing.SSWUParams.twist1 +assert_computable CompElliptic.Hashing.SSWUParams.twist2 +assert_computable CompElliptic.Hashing.SSWUParams.model1 +assert_computable CompElliptic.Hashing.SSWUParams.model2 +assert_computable CompElliptic.Hashing.SSWUParams.scale1 +assert_computable CompElliptic.Hashing.SSWUParams.scale2 +assert_computable CompElliptic.Hashing.sgn0 +assert_axioms CompElliptic.Hashing.SSWUParams.map_neg +assert_axioms CompElliptic.Hashing.SSWUParams.Zuu_add_one_ne_zero +assert_axioms CompElliptic.Hashing.SSWUParams.ta_ne_zero_of_u_ne_zero +assert_axioms CompElliptic.Hashing.SSWUParams.g_x2_eq +assert_axioms CompElliptic.Hashing.SSWUParams.model1_eq +assert_axioms CompElliptic.Hashing.SSWUParams.model2_eq +assert_axioms CompElliptic.Hashing.SSWUParams.model1_zero +assert_axioms CompElliptic.Hashing.SSWUParams.model2_zero +assert_axioms CompElliptic.Hashing.SSWUParams.scale1_ne_zero +assert_axioms CompElliptic.Hashing.SSWUParams.scale2_ne_zero + +/-! ### The model point sets and covering maps (`Hashing/BranchCovers.lean`) -/ + +assert_computable CompElliptic.Hashing.SSWUParams.modelPoints1 +choice +assert_computable CompElliptic.Hashing.SSWUParams.modelPoints2 +choice +assert_computable CompElliptic.Hashing.SSWUParams.cover1Map +choice +assert_computable CompElliptic.Hashing.SSWUParams.cover2Map +choice +assert_axioms CompElliptic.Hashing.SSWUParams.fibre_sum +assert_axioms CompElliptic.Hashing.SSWUParams.modelPoints_sum + +/-! ### The supporting facts of the cited steps (`Hashing/WeilSupport.lean`) -/ + +assert_axioms CompElliptic.Hashing.isCoprime_of_bezout +assert_axioms CompElliptic.Hashing.isCoprime_X_of_coeff_zero +assert_axioms CompElliptic.Hashing.isCoprime_C_of_ne_zero +assert_axioms CompElliptic.Hashing.not_X_sq_dvd +assert_axioms CompElliptic.Hashing.SSWUParams.gPoly +assert_axioms CompElliptic.Hashing.SSWUParams.gPoly_separable +assert_axioms CompElliptic.Hashing.SSWUParams.eval_g_neg_B_div_A +assert_axioms CompElliptic.Hashing.SSWUParams.g_neg_B_div_A_ne_zero +assert_axioms CompElliptic.Hashing.SSWUParams.phiCubic +assert_axioms CompElliptic.Hashing.SSWUParams.phiCubic_derivative +assert_axioms CompElliptic.Hashing.SSWUParams.phiCubic_separable +assert_axioms CompElliptic.Hashing.SSWUParams.taPoly_derivative +assert_axioms CompElliptic.Hashing.SSWUParams.tPoly_add_one_separable +assert_axioms CompElliptic.Hashing.SSWUParams.phiPoly +assert_axioms CompElliptic.Hashing.SSWUParams.eval_phiPoly +assert_axioms CompElliptic.Hashing.SSWUParams.phiPoly_eq_comp +assert_axioms CompElliptic.Hashing.SSWUParams.phiPoly_natDegree +assert_axioms CompElliptic.Hashing.SSWUParams.phiPoly_coeff_zero +assert_axioms CompElliptic.Hashing.SSWUParams.psiPoly +assert_axioms CompElliptic.Hashing.SSWUParams.psiPoly_coeff_zero +assert_axioms CompElliptic.Hashing.SSWUParams.phiPoly_64_eq +assert_axioms CompElliptic.Hashing.SSWUParams.phiPoly_isCoprime_snd +assert_axioms CompElliptic.Hashing.SSWUParams.phiPoly_isCoprime_tPoly_add_one +assert_axioms CompElliptic.Hashing.SSWUParams.phiPoly_separable +assert_axioms CompElliptic.Hashing.SSWUParams.phiPoly_squarefree +assert_axioms CompElliptic.Hashing.SSWUParams.model1Poly +assert_axioms CompElliptic.Hashing.SSWUParams.model2Poly +assert_axioms CompElliptic.Hashing.SSWUParams.eval_model1Poly +assert_axioms CompElliptic.Hashing.SSWUParams.eval_model2Poly +assert_axioms CompElliptic.Hashing.SSWUParams.model1Poly_natDegree +assert_axioms CompElliptic.Hashing.SSWUParams.model2Poly_natDegree +assert_axioms CompElliptic.Hashing.SSWUParams.model1Poly_squarefree +assert_axioms CompElliptic.Hashing.SSWUParams.model2Poly_squarefree +assert_axioms CompElliptic.Hashing.SSWUParams.p2Poly +assert_axioms CompElliptic.Hashing.SSWUParams.p2Poly_coeff +assert_axioms CompElliptic.Hashing.SSWUParams.p2Poly_natDegree +assert_axioms CompElliptic.Hashing.SSWUParams.p2Poly_isEisensteinAt +assert_axioms CompElliptic.Hashing.SSWUParams.p1RecipPoly +assert_axioms CompElliptic.Hashing.SSWUParams.p1RecipPoly_coeff +assert_axioms CompElliptic.Hashing.SSWUParams.p1RecipPoly_natDegree +assert_axioms CompElliptic.Hashing.SSWUParams.p1RecipPoly_isEisensteinAt +assert_axioms CompElliptic.Hashing.not_isSquare_ratFunc_of_squarefree +assert_axioms CompElliptic.Hashing.exists_sq_eq_of_ratFunc_sq +assert_axioms CompElliptic.Hashing.sq_or_mul_sq_of_isSquare_adjoinRoot +assert_axioms CompElliptic.Hashing.SSWUParams.not_isSquare_adjoinRoot_of_linear +assert_axioms CompElliptic.Hashing.SSWUParams.gPoly_not_isSquare_ratFunc +assert_axioms CompElliptic.Hashing.SSWUParams.v4TestPoly +assert_axioms CompElliptic.Hashing.SSWUParams.v4TestPoly_not_isSquare +assert_axioms CompElliptic.Hashing.SSWUParams.c4TestPoly +assert_axioms CompElliptic.Hashing.SSWUParams.c4TestPoly_not_isSquare + +/-! ### Characters and realness (`Hashing/CharacterSum.lean`) -/ + +assert_axioms CompElliptic.Hashing.charSum_eq +assert_axioms CompElliptic.Hashing.addChar_map_neg_eq_conj +assert_axioms CompElliptic.Hashing.IsOdd.mult_neg +assert_axioms CompElliptic.Hashing.IsOdd.conj_charSum +assert_axioms CompElliptic.Hashing.IsOdd.two_mul_charSum + +/-! ### The Weil-input shape and the assembly (`Hashing/WeilInstance.lean`, +`Hashing/WellDistributed.lean`, `Hashing/TwoTermUniformity.lean`) -/ + +assert_axioms CompElliptic.Hashing.CharSumBounded +assert_axioms CompElliptic.Hashing.SSWUParams.cover_charSum +assert_axioms CompElliptic.Hashing.SSWUParams.weilBounded_zeroRepaired +assert_axioms CompElliptic.Hashing.WeilBounded +assert_axioms CompElliptic.Hashing.WeilBounded.comp +assert_axioms CompElliptic.Hashing.sum_abs_prob_dev_le +assert_axioms CompElliptic.Hashing.sum_abs_prob_dev_transport_le + +/-! ### The deployed instances (`Hashing/PastaSSWU.lean`) -/ + +assert_computable CompElliptic.Curves.Pasta.Pallas.mapToCurve +choice +native( + CompElliptic.Fields.Pasta.pallasBase) +assert_computable CompElliptic.Curves.Pasta.Vesta.mapToCurve +choice +native( + CompElliptic.Fields.Pasta.vestaBase) +assert_axioms CompElliptic.Curves.Pasta.Pallas.neg_AB_not_isSquare +assert_axioms CompElliptic.Curves.Pasta.Vesta.neg_AB_not_isSquare +assert_axioms CompElliptic.Curves.Pasta.Pallas.weilBounded_zeroRepaired_mapToCurve +native( + CompElliptic.Fields.Pasta.pallasBase, + CompElliptic.Curves.Pasta.Pallas.q_nsmul_Gpt, + CompElliptic.Curves.Pasta.Pallas.q_nsmul_isoGpt) +assert_axioms CompElliptic.Curves.Pasta.Vesta.weilBounded_zeroRepaired_mapToCurve +native( + CompElliptic.Fields.Pasta.vestaBase, + CompElliptic.Curves.Pasta.Vesta.p_nsmul_Gpt, + CompElliptic.Curves.Pasta.Vesta.p_nsmul_isoGpt) diff --git a/design/weil-constant-derivation.md b/design/weil-constant-derivation.md index c759cbc..4204a7f 100644 --- a/design/weil-constant-derivation.md +++ b/design/weil-constant-derivation.md @@ -27,8 +27,12 @@ deployed constants is machine-checked (CompElliptic's `Hashing/PastaSSWU.lean`), and so are the checkable inputs of the two cited steps (`Hashing/WeilSupport.lean`, whose facts are referenced at their points of use below; CI checks that this document references all -of that file's declarations). The cited steps themselves and Weil's -theorem stay on paper — the vocabulary they need is tracked at #30. +of that file's declarations). Every declaration cited here is also +pinned in the axiom census (`CompElliptic/TrustBoundary.lean`), and CI +checks that too: a reader of this proof relies on everything it cites, +so an unpinned citation would be a gap in axiom-checking. The cited +steps themselves and Weil's theorem stay on paper — the vocabulary they +need is tracked at #30. ## Background diff --git a/scripts/check_weil_support_refs.py b/scripts/check_weil_support_refs.py index f5311bd..c8cbc7e 100755 --- a/scripts/check_weil_support_refs.py +++ b/scripts/check_weil_support_refs.py @@ -1,11 +1,15 @@ #!/usr/bin/env python3 -"""Check the design doc's references to the formalized supporting facts: -every declaration of CompElliptic/Hashing/WeilSupport.lean must be -referenced (backticked) somewhere in design/weil-constant-derivation.md, -and every backticked identifier in the doc (dot-qualified ones included) -must resolve to a declaration somewhere in CompElliptic or be a known -non-Lean term. Run from the repository root; exits non-zero on -violation.""" +"""Check the design doc's references to the formalized facts, in three +directions: every declaration of CompElliptic/Hashing/WeilSupport.lean +must be referenced (backticked) somewhere in +design/weil-constant-derivation.md; every backticked identifier in the +doc (dot-qualified ones included) must resolve to a declaration +somewhere in CompElliptic or be a known non-Lean term; and every +referenced declaration must be named directly in an `assert_axioms` or +`assert_computable` entry of CompElliptic/TrustBoundary.lean. The doc is +a pencil-and-paper proof whose reader relies on everything it cites, so +an unpinned citation would be a gap in axiom-checking. Run from the +repository root; exits non-zero on violation.""" import pathlib import re import sys @@ -50,6 +54,20 @@ def last(name: str) -> str: unknown = sorted(name for name in listed if last(name) not in declared_last and name not in ALLOWED_NON_LEAN) + +# Census entries are written fully qualified, so a reference is pinned when +# some entry's name ends with it at a segment boundary. An ambiguous short +# reference (`mapToCurve`) is satisfied by any of its instantiations; the +# census pins all of them. +pins = set(re.findall( + r'^assert_(?:axioms|computable) +(?:_root_\.)?' + r'([A-Za-z_][A-Za-z0-9_]*(?:\.[A-Za-z_][A-Za-z0-9_]*)*)', + (root / 'CompElliptic/TrustBoundary.lean').read_text(), re.M)) +unpinned = sorted(name for name in listed + if name not in ALLOWED_NON_LEAN + and last(name) in declared_last + and not any(p == name or p.endswith('.' + name) + for p in pins)) if missing: print("declared in WeilSupport.lean but not referenced in the doc:", *missing, sep='\n ') @@ -57,4 +75,8 @@ def last(name: str) -> str: print("backticked in the doc but not a CompElliptic declaration" " (add to ALLOWED_NON_LEAN if intentional):", *unknown, sep='\n ') -sys.exit(1 if (missing or unknown) else 0) +if unpinned: + print("referenced in the doc but not pinned in the axiom census" + " (CompElliptic/TrustBoundary.lean):", + *unpinned, sep='\n ') +sys.exit(1 if (missing or unknown or unpinned) else 0) From fdb2580c2163c7af2121f784b071b147d8168e44 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Thu, 20 Aug 2026 03:07:08 +0100 Subject: [PATCH 23/25] scripts: resolve doc citations by path-suffix, not final segment MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- scripts/check_weil_support_refs.py | 89 ++++++++++++++++++++---------- 1 file changed, 59 insertions(+), 30 deletions(-) diff --git a/scripts/check_weil_support_refs.py b/scripts/check_weil_support_refs.py index c8cbc7e..1e8a5c0 100755 --- a/scripts/check_weil_support_refs.py +++ b/scripts/check_weil_support_refs.py @@ -3,13 +3,14 @@ directions: every declaration of CompElliptic/Hashing/WeilSupport.lean must be referenced (backticked) somewhere in design/weil-constant-derivation.md; every backticked identifier in the -doc (dot-qualified ones included) must resolve to a declaration -somewhere in CompElliptic or be a known non-Lean term; and every -referenced declaration must be named directly in an `assert_axioms` or -`assert_computable` entry of CompElliptic/TrustBoundary.lean. The doc is -a pencil-and-paper proof whose reader relies on everything it cites, so -an unpinned citation would be a gap in axiom-checking. Run from the -repository root; exits non-zero on violation.""" +doc (dot-qualified ones included) must be a dot-path suffix of the +fully qualified name of a declaration somewhere in CompElliptic, or be +a known non-Lean term; and every referenced declaration must be named +directly in an `assert_axioms` or `assert_computable` entry of +CompElliptic/TrustBoundary.lean. The doc is a pencil-and-paper proof +whose reader relies on everything it cites, so an unpinned citation +would be a gap in axiom-checking. Run from the repository root; exits +non-zero on violation.""" import pathlib import re import sys @@ -21,16 +22,52 @@ } DECL_RE = re.compile( - r'^(?:noncomputable )?(?:def|theorem|abbrev|structure) ' - r'(?:_root_\.)?([A-Za-z_][A-Za-z0-9_]*(?:\.[A-Za-z_][A-Za-z0-9_]*)*)', - re.M) + r'^(private +|protected +)?(?:noncomputable +|partial +|unsafe +)?' + r'(?:theorem|lemma|def|abbrev|instance|axiom|opaque|inductive' + r'|structure|class) ' + r"(_root_\.)?([A-Za-z_][A-Za-z0-9_']*(?:\.[A-Za-z_][A-Za-z0-9_']*)*)") +NS_RE = re.compile(r"^namespace +([A-Za-z_][A-Za-z0-9_.']*)") +END_RE = re.compile(r"^end +([A-Za-z_][A-Za-z0-9_.']*)") + + +def declared_names(path: pathlib.Path) -> set: + """The fully qualified names declared in a Lean file. The enclosing + namespace is reconstructed from the `namespace`/`end` pairs above each + declaration — `end ` pops only a matching innermost `namespace`, so + a named `section ... end` cannot corrupt the stack — the same + reconstruction as ironwood's `scripts/check_endpoint_census.sh`. A + `_root_.` prefix ignores the enclosing namespace; a `private` + declaration is not citable, so it is not collected.""" + names = set() + stack = [] + for line in path.read_text().splitlines(): + m = NS_RE.match(line) + if m: + stack.append(m.group(1)) + continue + m = END_RE.match(line) + if m: + if stack and stack[-1] == m.group(1): + stack.pop() + continue + m = DECL_RE.match(line) + if m and not (m.group(1) or '').startswith('private'): + names.add(m.group(3) if m.group(2) or not stack + else '.'.join(stack) + '.' + m.group(3)) + return names + + +def is_path_suffix(name: str, full: str) -> bool: + """Whether `name` is a dot-path suffix of `full`, on segment + boundaries.""" + return full == name or full.endswith('.' + name) + root = pathlib.Path(__file__).resolve().parent.parent -support = set(DECL_RE.findall( - (root / 'CompElliptic/Hashing/WeilSupport.lean').read_text())) +support = declared_names(root / 'CompElliptic/Hashing/WeilSupport.lean') everywhere = set() for f in (root / 'CompElliptic').rglob('*.lean'): - everywhere |= set(DECL_RE.findall(f.read_text())) + everywhere |= declared_names(f) doc = (root / 'design/weil-constant-derivation.md').read_text() listed = set(re.findall( @@ -40,20 +77,14 @@ listed = {name for name in listed if not re.search(r'\.(lean|sage|py|md|toml|yml|sh)$', name)} - -def last(name: str) -> str: - """The final dot-separated segment of a (possibly qualified) name.""" - return name.rsplit('.', 1)[-1] - - -# Declarations are spelled bare inside namespace blocks or dot-qualified at -# top level; references may use either form. Compare by final segment. -declared_last = {last(name) for name in everywhere} -missing = sorted({last(name) for name in support} - - {last(name) for name in listed}) +# A citation resolves when it is a dot-path suffix of some declaration's +# fully qualified name. Final-segment matching alone would let a bogus +# `junk.last` resolve against any declaration ending in `last`. +missing = sorted(full for full in support + if not any(is_path_suffix(name, full) for name in listed)) unknown = sorted(name for name in listed - if last(name) not in declared_last - and name not in ALLOWED_NON_LEAN) + if name not in ALLOWED_NON_LEAN + and not any(is_path_suffix(name, full) for full in everywhere)) # Census entries are written fully qualified, so a reference is pinned when # some entry's name ends with it at a segment boundary. An ambiguous short @@ -64,10 +95,8 @@ def last(name: str) -> str: r'([A-Za-z_][A-Za-z0-9_]*(?:\.[A-Za-z_][A-Za-z0-9_]*)*)', (root / 'CompElliptic/TrustBoundary.lean').read_text(), re.M)) unpinned = sorted(name for name in listed - if name not in ALLOWED_NON_LEAN - and last(name) in declared_last - and not any(p == name or p.endswith('.' + name) - for p in pins)) + if name not in ALLOWED_NON_LEAN and name not in unknown + and not any(is_path_suffix(name, p) for p in pins)) if missing: print("declared in WeilSupport.lean but not referenced in the doc:", *missing, sep='\n ') From 642a7f7b243115664930bec67a76d118d932010c Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Thu, 20 Aug 2026 05:31:39 +0100 Subject: [PATCH 24/25] scripts: restrict citation resolution to the relevant modules MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- design/weil-constant-derivation.md | 5 +- scripts/check_weil_support_refs.py | 103 ++++++++++++++++++++--------- 2 files changed, 73 insertions(+), 35 deletions(-) diff --git a/design/weil-constant-derivation.md b/design/weil-constant-derivation.md index 4204a7f..343fbaa 100644 --- a/design/weil-constant-derivation.md +++ b/design/weil-constant-derivation.md @@ -121,8 +121,9 @@ and exactly one of g(x₁(u)), g(x₂(u)) is a square, by the identity g(x₂) = t³·g(x₁) with t = Z·u² in the square class of Z (in cleared form, `g_x2_eq`). The mapping outputs the point with the square candidate, with its ordinate's sign set by `sgn0`; the zero-repaired -form sets f(0) = 𝒪, which makes f odd: f(−u) = −f(u) for all u (`map_neg` -away from 0; on each deployed curve, `isOdd_zeroRepaired_mapToCurve`). +form sets f(0) = 𝒪, which makes f odd: f(−u) = −f(u) for all u away +from 0 (`SSWUParams.map_neg`); on each deployed curve this is +`isOdd_zeroRepaired_mapToCurve`. Since q ≡ 1 (mod 4), −1 is a square, so −1/Z is a nonsquare and t = −1 has no solutions (`Zuu_add_one_ne_zero`): **ta vanishes only at u = 0** diff --git a/scripts/check_weil_support_refs.py b/scripts/check_weil_support_refs.py index 1e8a5c0..cb629df 100755 --- a/scripts/check_weil_support_refs.py +++ b/scripts/check_weil_support_refs.py @@ -1,16 +1,20 @@ #!/usr/bin/env python3 -"""Check the design doc's references to the formalized facts, in three -directions: every declaration of CompElliptic/Hashing/WeilSupport.lean -must be referenced (backticked) somewhere in -design/weil-constant-derivation.md; every backticked identifier in the -doc (dot-qualified ones included) must be a dot-path suffix of the -fully qualified name of a declaration somewhere in CompElliptic, or be -a known non-Lean term; and every referenced declaration must be named -directly in an `assert_axioms` or `assert_computable` entry of -CompElliptic/TrustBoundary.lean. The doc is a pencil-and-paper proof -whose reader relies on everything it cites, so an unpinned citation -would be a gap in axiom-checking. Run from the repository root; exits -non-zero on violation.""" +"""Check the design doc's references to the formalized facts: every +declaration of CompElliptic/Hashing/WeilSupport.lean must be referenced +(backticked) somewhere in design/weil-constant-derivation.md, and every +backticked identifier in the doc (dot-qualified ones included) must +resolve to a declaration — its exact fully qualified name anywhere in +CompElliptic, or a dot-path suffix of one under the relevant modules +(CompElliptic.{Hashing,Curves}). A citation that also matches a name +outside the relevant modules must qualify itself. Every declaration a +citation can refer to must be named directly in an `assert_axioms` or +`assert_computable` entry of CompElliptic/TrustBoundary.lean: the doc +is a pencil-and-paper proof whose reader relies on everything it cites, +so an unpinned citation would be a gap in axiom-checking. Declared Lean +names that could be mistaken for a filename or an allowlisted non-Lean +term are rejected outright, so the citation filters cannot silently +mask a real declaration. Run from the repository root; exits non-zero +on violation.""" import pathlib import re import sys @@ -28,6 +32,7 @@ r"(_root_\.)?([A-Za-z_][A-Za-z0-9_']*(?:\.[A-Za-z_][A-Za-z0-9_']*)*)") NS_RE = re.compile(r"^namespace +([A-Za-z_][A-Za-z0-9_.']*)") END_RE = re.compile(r"^end +([A-Za-z_][A-Za-z0-9_.']*)") +FILENAME_RE = re.compile(r"\.(lean|sage|py|md|toml|yml|sh)$") def declared_names(path: pathlib.Path) -> set: @@ -68,6 +73,12 @@ def is_path_suffix(name: str, full: str) -> bool: everywhere = set() for f in (root / 'CompElliptic').rglob('*.lean'): everywhere |= declared_names(f) +relevant = {full for full in everywhere + if full.startswith('CompElliptic.Hashing.') + or full.startswith('CompElliptic.Curves.')} +confusable = {full for full in everywhere + if any(is_path_suffix(name, full) for name in ALLOWED_NON_LEAN) + or FILENAME_RE.search(full)} doc = (root / 'design/weil-constant-derivation.md').read_text() listed = set(re.findall( @@ -75,37 +86,63 @@ def is_path_suffix(name: str, full: str) -> bool: # Backticked filenames (`BranchCovers.lean`, `weilbound.sage`) are file # references, not declarations. listed = {name for name in listed - if not re.search(r'\.(lean|sage|py|md|toml|yml|sh)$', name)} + if name not in ALLOWED_NON_LEAN + and not FILENAME_RE.search(name)} -# A citation resolves when it is a dot-path suffix of some declaration's -# fully qualified name. Final-segment matching alone would let a bogus -# `junk.last` resolve against any declaration ending in `last`. -missing = sorted(full for full in support - if not any(is_path_suffix(name, full) for name in listed)) -unknown = sorted(name for name in listed - if name not in ALLOWED_NON_LEAN - and not any(is_path_suffix(name, full) for full in everywhere)) +# A citation resolves when it either matches the fully qualified name +# exactly, or it is a dot-path suffix of the fully qualified name of +# some declaration under a "relevant" module (see above). Final-segment +# matching alone would let a bogus `junk.last` resolve against any +# declaration ending in `last`. Allowing matches in any module would +# incur a greater risk of typos accidentally matching unrelated names. +missing = {full for full in support + if not any(is_path_suffix(name, full) for name in listed)} +unknown = {name for name in listed + if name not in everywhere # exact match + and not any(is_path_suffix(name, full) for full in relevant)} + +# There should not be any non-fully-qualified references that match names +# outside the relevant modules. An unknown citation selects no referents: +# its remedy is fixing the citation, so it must not also demand +# qualification or pins here and below. +irrelevant = {full for full in everywhere + if full not in relevant + and any(name not in unknown + and name != full and is_path_suffix(name, full) + for name in listed)} # Census entries are written fully qualified, so a reference is pinned when -# some entry's name ends with it at a segment boundary. An ambiguous short -# reference (`mapToCurve`) is satisfied by any of its instantiations; the -# census pins all of them. +# *every* declaration of which it is a dot-path suffix is included in the +# census. So an ambiguous short reference (e.g. `mapToCurve`) requires all +# of its potential referents to be pinned. Cases already reported as +# "irrelevant" matches are excluded. pins = set(re.findall( r'^assert_(?:axioms|computable) +(?:_root_\.)?' r'([A-Za-z_][A-Za-z0-9_]*(?:\.[A-Za-z_][A-Za-z0-9_]*)*)', (root / 'CompElliptic/TrustBoundary.lean').read_text(), re.M)) -unpinned = sorted(name for name in listed - if name not in ALLOWED_NON_LEAN and name not in unknown - and not any(is_path_suffix(name, p) for p in pins)) +unpinned = {full for full in everywhere + if full not in pins and full not in irrelevant + and any(name not in unknown and is_path_suffix(name, full) + for name in listed)} + if missing: print("declared in WeilSupport.lean but not referenced in the doc:", - *missing, sep='\n ') + *sorted(missing), sep='\n ') if unknown: - print("backticked in the doc but not a CompElliptic declaration" - " (add to ALLOWED_NON_LEAN if intentional):", - *unknown, sep='\n ') + print("backticked in the doc but not found as a relevant or fully qualified" + " declaration (add to ALLOWED_NON_LEAN if intentional):", + *sorted(unknown), sep='\n ') +if irrelevant: + print("referenced in the doc but matches a name outside the relevant modules" + " (qualify to avoid ambiguity):", + *sorted(irrelevant), sep='\n ') if unpinned: print("referenced in the doc but not pinned in the axiom census" " (CompElliptic/TrustBoundary.lean):", - *unpinned, sep='\n ') -sys.exit(1 if (missing or unknown or unpinned) else 0) + *sorted(unpinned), sep='\n ') +if confusable: + print("declared Lean name that looks like a filename or a name in" + " the ALLOWED_NON_LEAN list:", + *sorted(confusable), sep='\n ') + +sys.exit(1 if (missing or unknown or irrelevant or unpinned or confusable) else 0) From 45607a04d2088d3e04cab8bc0d50555d1206e55e Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Thu, 20 Aug 2026 06:37:50 +0100 Subject: [PATCH 25/25] =?UTF-8?q?ci:=20one=20sage=20environment=20for=20al?= =?UTF-8?q?l=20steps=20=E2=80=94=20the=20job=20has=20three=20now?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Claude Fable 5 --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 58343ef..b2f5756 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -80,7 +80,7 @@ jobs: - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 with: persist-credentials: false - # One environment for both sage steps. Sage is pinned to the version that + # One environment for all sage steps. Sage is pinned to the version that # generated the committed certificates: Singular's `lift` output (the # emitted cofactors) can differ between versions, so byte-reproducibility # needs the same engine as the local regeneration. (The Weil-derivation