diff --git a/CompElliptic/Curves/Pasta.lean b/CompElliptic/Curves/Pasta.lean index 802ea5f..0bc3185 100644 --- a/CompElliptic/Curves/Pasta.lean +++ b/CompElliptic/Curves/Pasta.lean @@ -52,9 +52,9 @@ theorem not_onCurve_zero : ¬ OnCurve a b (0, 0) := /-- `5` is a quadratic non-residue in the Pallas base field, so `y² = x³ + 5` has no point with `x = 0` (Zcash protocol spec §5.4.9.7). -Euler's criterion (`ZMod.euler_criterion`) reduces this to `5 ^ (p / 2) ≠ 1`. The LHS (`-1`) is +Euler's criterion (`ZMod.euler_criterion`) reduces this to `5^(p / 2) ≠ 1`. The LHS (`-1`) is evaluated by `reduce_mod_char` (fast modular exponentiation via `NormNum.PowMod`), the same -machinery the `PrattPartList.prime` legs use for their `a ^ k ≠ 1` conditions. -/ +machinery the `PrattPartList.prime` legs use for their `a^k ≠ 1` conditions. -/ theorem five_not_isSquare : ¬ IsSquare (5 : PallasBaseField) := by rw [ZMod.euler_criterion PALLAS_BASE_CARD (by decide : (5 : PallasBaseField) ≠ 0)] reduce_mod_char @@ -64,7 +64,7 @@ theorem five_not_isSquare : ¬ IsSquare (5 : PallasBaseField) := by unambiguously. -/ theorem no_onCurve_x_zero (y : PallasBaseField) : ¬ OnCurve a b (0, y) := by intro h - have h' : y ^ 2 = 5 := by simpa [OnCurve, a, b] using h + have h' : y^2 = 5 := by simpa [OnCurve, a, b] using h exact five_not_isSquare ⟨y, by rw [← h', pow_two]⟩ /-- `-5` is not a cube in the Pallas base field — the cubic analogue of `five_not_isSquare`, and @@ -73,7 +73,7 @@ what rules out 2-torsion on the Pallas curve. `3 ∣ p - 1`, so `not_exists_pow_eq_of_pow_ne_one` reduces this to the single power `(-5)^((p-1)/3)`, which is not `1`. As for `five_not_isSquare`, `reduce_mod_char` (fast modular exponentiation) evaluates it and the kernel re-checks the result. -/ -theorem neg_five_not_isCube : ¬ ∃ x : PallasBaseField, x ^ 3 = -(5 : PallasBaseField) := by +theorem neg_five_not_isCube : ¬ ∃ x : PallasBaseField, x^3 = -(5 : PallasBaseField) := by have hcard : Fintype.card PallasBaseField = PALLAS_BASE_CARD := ZMod.card _ refine Fields.not_exists_pow_eq_of_pow_ne_one (n := 3) (by rw [hcard]; decide) (by decide) ?_ rw [hcard] @@ -87,7 +87,7 @@ theorem neg_five_not_isCube : ¬ ∃ x : PallasBaseField, x ^ 3 = -(5 : PallasBa not a cube (`neg_five_not_isCube`). Equivalently, the Pallas group has no 2-torsion. -/ theorem no_onCurve_y_zero (x : PallasBaseField) : ¬ OnCurve a b (x, 0) := by intro h - have hsum : x ^ 3 + 5 = 0 := by simpa [OnCurve, a, b] using h.symm + have hsum : x^3 + 5 = 0 := by simpa [OnCurve, a, b] using h.symm exact neg_five_not_isCube ⟨x, by linear_combination hsum⟩ -- `(-1, 2)` is on the curve: `2² = 4 = (-1)³ + 5`. @@ -144,7 +144,7 @@ theorem not_onCurve_zero : ¬ OnCurve a b (0, 0) := /-- `5` is a quadratic non-residue in the Vesta base field, so `y² = x³ + 5` has no point with `x = 0` (Zcash protocol spec §5.4.9.7). -As for Pallas: Euler's criterion (`ZMod.euler_criterion`) reduces this to `5 ^ (q / 2) ≠ 1`, and +As for Pallas: Euler's criterion (`ZMod.euler_criterion`) reduces this to `5^(q / 2) ≠ 1`, and `reduce_mod_char` (fast modular exponentiation) evaluates the power to `-1`. -/ theorem five_not_isSquare : ¬ IsSquare (5 : VestaBaseField) := by rw [ZMod.euler_criterion PALLAS_SCALAR_CARD (by decide : (5 : VestaBaseField) ≠ 0)] @@ -155,7 +155,7 @@ theorem five_not_isSquare : ¬ IsSquare (5 : VestaBaseField) := by unambiguously. -/ theorem no_onCurve_x_zero (y : VestaBaseField) : ¬ OnCurve a b (0, y) := by intro h - have h' : y ^ 2 = 5 := by simpa [OnCurve, a, b] using h + have h' : y^2 = 5 := by simpa [OnCurve, a, b] using h exact five_not_isSquare ⟨y, by rw [← h', pow_two]⟩ /-- `-5` is not a cube in the Vesta base field — the cubic analogue of `five_not_isSquare`, and @@ -164,7 +164,7 @@ what rules out 2-torsion on the Vesta curve. `3 ∣ q - 1`, so `not_exists_pow_eq_of_pow_ne_one` reduces this to the single power `(-5)^((q-1)/3)`, which is not `1`. As for `five_not_isSquare`, `reduce_mod_char` (fast modular exponentiation) evaluates it and the kernel re-checks the result. -/ -theorem neg_five_not_isCube : ¬ ∃ x : VestaBaseField, x ^ 3 = -(5 : VestaBaseField) := by +theorem neg_five_not_isCube : ¬ ∃ x : VestaBaseField, x^3 = -(5 : VestaBaseField) := by have hcard : Fintype.card VestaBaseField = PALLAS_SCALAR_CARD := ZMod.card _ refine Fields.not_exists_pow_eq_of_pow_ne_one (n := 3) (by rw [hcard]; decide) (by decide) ?_ rw [hcard] @@ -179,7 +179,7 @@ theorem neg_five_not_isCube : ¬ ∃ x : VestaBaseField, x ^ 3 = -(5 : VestaBase a cube (`neg_five_not_isCube`). Equivalently, the Vesta group has no 2-torsion. -/ theorem no_onCurve_y_zero (x : VestaBaseField) : ¬ OnCurve a b (x, 0) := by intro h - have hsum : x ^ 3 + 5 = 0 := by simpa [OnCurve, a, b] using h.symm + have hsum : x^3 + 5 = 0 := by simpa [OnCurve, a, b] using h.symm exact neg_five_not_isCube ⟨x, by linear_combination hsum⟩ -- `(-1, 2)` is on the curve: `2² = 4 = (-1)³ + 5`. diff --git a/CompElliptic/Fields/Residue.lean b/CompElliptic/Fields/Residue.lean index e1aaad1..2f902c9 100644 --- a/CompElliptic/Fields/Residue.lean +++ b/CompElliptic/Fields/Residue.lean @@ -30,14 +30,14 @@ parameters. namespace CompElliptic.Fields -/-- If `n ∣ #F - 1` and `a ^ ((#F - 1) / n) ≠ 1`, then `a` is not an `n`-th power in `F`. +/-- If `n ∣ #F - 1` and `a^((#F - 1) / n) ≠ 1`, then `a` is not an `n`-th power in `F`. An `n`-th root `x` of `a` is nonzero along with `a`, so Fermat's little theorem forces -`a ^ ((#F - 1) / n) = x ^ (n * ((#F - 1) / n)) = x ^ (#F - 1) = 1`. Contrapositively, evaluating +`a^((#F - 1) / n) = x^(n * ((#F - 1) / n)) = x^(#F - 1) = 1`. Contrapositively, evaluating that one power and finding it is not `1` rules out every root at once. -/ theorem not_exists_pow_eq_of_pow_ne_one {F : Type*} [Field F] [Fintype F] {n : ℕ} {a : F} (hn : n ∣ Fintype.card F - 1) (ha : a ≠ 0) - (h : a ^ ((Fintype.card F - 1) / n) ≠ 1) : ¬ ∃ x : F, x^n = a := by + (h : a^((Fintype.card F - 1) / n) ≠ 1) : ¬ ∃ x : F, x^n = a := by -- `n = 0` is already impossible: the exponent `(#F - 1) / 0` is `0`, so `h` reads `1 ≠ 1`. have hn0 : n ≠ 0 := by rintro rfl; simp at h rintro ⟨x, rfl⟩ @@ -55,8 +55,8 @@ This is Cardano's formula run backwards. A root would split as `x = u + v` with `3·u·v = -A`, making `u³` and `v³` the two roots of the resolvent quadratic `t² + q·t - A³/27`; `w` is one of those roots, so it would be a cube. The proof stays inside `F`, with no splitting field: for a root `x` with `3·x² + A ≠ 0`, setting `r := 3·s/(3·x² + A)` gives -`((x+r)³ - 8·w)·((x-r)³ - 8·w) = 0` as a polynomial consequence of the hypotheses, so `w` is -the cube of `(x+r)/2` or of `(x-r)/2`. A root with `3·x² + A = 0` forces `s = 0` and +`((x + r)³ - 8·w)·((x - r)³ - 8·w) = 0` as a polynomial consequence of the hypotheses, so `w` is +the cube of `(x + r)/2` or of `(x - r)/2`. A root with `3·x² + A = 0` forces `s = 0` and `w = (-x)³` directly. Over a finite field a cubic with no roots is irreducible. So this lemma, with @@ -64,42 +64,42 @@ Over a finite field a cubic with no roots is irreducible. So this lemma, with checkable by `decide` from two precomputed field elements. -/ theorem cubic_no_root_of_resolvent_noncube {F : Type*} [Field F] (h2 : (2 : F) ≠ 0) (h3 : (3 : F) ≠ 0) {A q s w : F} - (hs : 27 * s ^ 2 = 27 * q ^ 2 + 4 * A ^ 3) - (hw : 2 * w = -q + s) - (hnc : ¬ ∃ u : F, u ^ 3 = w) : - ∀ x : F, x ^ 3 + A * x + q ≠ 0 := by + (hs : 27 * s^2 = 27 * q^2 + 4 * A^3) + (hw : 2*w = -q + s) + (hnc : ¬ ∃ u : F, u^3 = w) : + ∀ x : F, x^3 + A*x + q ≠ 0 := by intro x hx have h27 : (27 : F) ≠ 0 := by have h := pow_ne_zero 3 h3 norm_num at h exact h - by_cases hd : 3 * x ^ 2 + A = 0 + by_cases hd : 3 * x^2 + A = 0 · -- A root that is also a critical point: then `s = 0` and `w = (-x)³`, a cube. - have hq : q = 2 * x ^ 3 := by linear_combination hx - x * hd + have hq : q = 2 * x^3 := by linear_combination hx - x*hd have hs0 : s = 0 := by - have h0 : 27 * s ^ 2 = 0 := by - linear_combination hs + 27 * (q + 2 * x ^ 3) * hq - + 4 * (A ^ 2 - 3 * A * x ^ 2 + 9 * x ^ 4) * hd + have h0 : 27 * s^2 = 0 := by + linear_combination hs + 27 * (q + 2 * x^3) * hq + + 4 * (A^2 - 3 * A * x^2 + 9 * x^4) * hd exact sq_eq_zero_iff.mp ((mul_eq_zero.mp h0).resolve_left h27) refine hnc ⟨-x, mul_left_cancel₀ h2 ?_⟩ linear_combination -hw + hq - hs0 - · -- Cardano's split inside `F`: `(x+r)/2` and `(x-r)/2` play the roles of `u` and `v`. - obtain ⟨r, hr⟩ : ∃ r : F, r = 3 * s / (3 * x ^ 2 + A) := ⟨_, rfl⟩ - have hkey : 27 * s ^ 2 = (3 * x ^ 2 + A) ^ 2 * (3 * x ^ 2 + 4 * A) := by - linear_combination hs + 27 * (q - x ^ 3 - A * x) * hx - have hr3 : 3 * r ^ 2 = 3 * x ^ 2 + 4 * A := by + · -- Cardano's split inside `F`: `(x + r)/2` and `(x - r)/2` play the roles of `u` and `v`. + obtain ⟨r, hr⟩ : ∃ r : F, r = 3*s / (3 * x^2 + A) := ⟨_, rfl⟩ + have hkey : 27 * s^2 = (3 * x^2 + A)^2 * (3 * x^2 + 4*A) := by + linear_combination hs + 27 * (q - x^3 - A*x) * hx + have hr3 : 3 * r^2 = 3 * x^2 + 4*A := by rw [hr] field_simp linear_combination hkey - have hpr : 3 * ((x + r) * (x - r)) = -(4 * A) := by linear_combination -hr3 - have hsum : (x + r) ^ 3 + (x - r) ^ 3 = -(8 * q) := by - linear_combination 2 * x * hr3 + 8 * hx - have hwq : 108 * (w ^ 2 + q * w) = 4 * A ^ 3 := by - linear_combination hs + 27 * (2 * w + q + s) * hw - have h0 : 27 * (((x + r) ^ 3 - 8 * w) * ((x - r) ^ 3 - 8 * w)) = 0 := by + have hpr : 3 * ((x + r) * (x - r)) = -(4*A) := by linear_combination -hr3 + have hsum : (x + r)^3 + (x - r)^3 = -(8*q) := by + linear_combination 2*x*hr3 + 8*hx + have hwq : 108 * (w^2 + q*w) = 4 * A^3 := by + linear_combination hs + 27 * (2*w + q + s) * hw + have h0 : 27 * (((x + r)^3 - 8*w) * ((x - r)^3 - 8*w)) = 0 := by linear_combination - (9 * ((x + r) * (x - r)) ^ 2 - 12 * ((x + r) * (x - r)) * A + 16 * A ^ 2) * hpr - - 216 * w * hsum + 16 * hwq + (9 * ((x + r) * (x - r))^2 - 12 * ((x + r) * (x - r)) * A + 16 * A^2) * hpr + - 216*w*hsum + 16*hwq rcases mul_eq_zero.mp ((mul_eq_zero.mp h0).resolve_left h27) with h | h · refine hnc ⟨(x + r) / 2, ?_⟩ field_simp diff --git a/CompElliptic/Fields/Sqrt.lean b/CompElliptic/Fields/Sqrt.lean index b849cdf..b63911d 100644 --- a/CompElliptic/Fields/Sqrt.lean +++ b/CompElliptic/Fields/Sqrt.lean @@ -88,9 +88,9 @@ where /-- Spec of the `go` accumulator: when some `2^j`-th power of `b2k` (with `j ≤ fuel`) is `1`, `go k b2k fuel = k + j₀` where `j₀` is the *least* such exponent. -/ theorem leastPow2Order.go_spec {F : Type*} [Monoid F] [DecidableEq F] : - ∀ (fuel k : ℕ) (b2k : F), (∃ j ≤ fuel, b2k ^ 2^j = 1) → - ∃ j ≤ fuel, leastPow2Order.go k b2k fuel = k + j ∧ b2k ^ 2^j = 1 ∧ - ∀ i < j, b2k ^ 2^i ≠ 1 := by + ∀ (fuel k : ℕ) (b2k : F), (∃ j ≤ fuel, b2k^(2^j) = 1) → + ∃ j ≤ fuel, leastPow2Order.go k b2k fuel = k + j ∧ b2k^(2^j) = 1 ∧ + ∀ i < j, b2k^(2^i) ≠ 1 := by intro fuel induction fuel with | zero => @@ -101,12 +101,12 @@ theorem leastPow2Order.go_spec {F : Type*} [Monoid F] [DecidableEq F] : | succ fuel ih => intro k b2k hex obtain ⟨j, hj, hbj⟩ := hex - have hconv : ∀ m : ℕ, (b2k * b2k) ^ 2^m = b2k ^ 2^(m+1) := fun m => by + have hconv : ∀ m : ℕ, (b2k * b2k)^(2^m) = b2k^(2^(m+1)) := fun m => by rw [← pow_two, ← pow_mul, ← pow_succ'] by_cases hb1 : b2k = 1 · exact ⟨0, Nat.zero_le _, by simp [leastPow2Order.go, hb1], by simpa using hb1, fun i hi => absurd hi (Nat.not_lt_zero i)⟩ - · have hex' : ∃ j' ≤ fuel, (b2k * b2k) ^ 2^j' = 1 := by + · have hex' : ∃ j' ≤ fuel, (b2k * b2k)^(2^j') = 1 := by obtain _ | j := j · exact absurd (by simpa using hbj) hb1 · exact ⟨j, by omega, by rw [hconv]; exact hbj⟩ @@ -131,18 +131,18 @@ theorem leastPow2Order_spec {F : Type*} [Monoid F] [DecidableEq F] (b : F) (y : · exact h have hconv : ∀ m : ℕ, (b*b)^(2^m) = b^(2^(m+1)) := fun m => by rw [← pow_two, ← pow_mul, ← pow_succ'] - have hwit : (b*b)^(2^(y-2)) = 1 := by rw [hconv, show y-2+1 = y-1 from by omega]; exact hy - obtain ⟨j, hj, hgo, hbj, hmin⟩ := leastPow2Order.go_spec y 1 (b*b) ⟨y-2, by omega, hwit⟩ + have hwit : (b*b)^(2^(y - 2)) = 1 := by rw [hconv, show y - 2 + 1 = y-1 from by omega]; exact hy + obtain ⟨j, hj, hgo, hbj, hmin⟩ := leastPow2Order.go_spec y 1 (b*b) ⟨y - 2, by omega, hwit⟩ have hk : leastPow2Order b y = 1 + j := hgo - have hjle : j ≤ y-2 := by - by_contra h; exact hmin (y-2) (Nat.lt_of_not_le h) hwit + have hjle : j ≤ y - 2 := by + by_contra h; exact hmin (y - 2) (Nat.lt_of_not_le h) hwit have hbk1 : b^(2^j) ≠ 1 := by obtain _ | j := j · simpa using hb · rw [← hconv]; exact hmin j (by omega) refine ⟨by omega, by omega, ?_, ?_⟩ · rw [hk, show (1:ℕ)+j = j+1 from by omega, ← hconv]; exact hbj - · rw [hk, show 1+j-1 = j from by omega]; exact hbk1 + · rw [hk, show 1 + j - 1 = j from by omega]; exact hbk1 /-- Validity of Tonelli–Shanks data for `F`, as a predicate on the *bare components* (mirroring `IsCanonical` for encodings): the 2-adic factorization `card - 1 = 2^twoAdicity * oddPart` holds @@ -219,8 +219,8 @@ theorem loop_sound {F : Type*} [Field F] [DecidableEq F] (a : F) : have hy2 : 2 ≤ y := by omega set k := leastPow2Order b y with hkdef set w := iterSq c (y - k - 1) with hwdef - have hw2 : w*w = c^(2^(y-k)) := by - rw [hwdef, iterSq_spec, ← pow_add, ← two_mul, ← pow_succ', show y-k-1+1 = y-k from by omega] + have hw2 : w*w = c^(2^(y - k)) := by + rw [hwdef, iterSq_spec, ← pow_add, ← two_mul, ← pow_succ', show y - k - 1 + 1 = y - k from by omega] have hcm1 : c^(2^(y-1)) = -1 := by have hne : c^(2^(y-1)) ≠ 1 := by intro h @@ -245,12 +245,12 @@ theorem loop_sound {F : Type*} [Field F] [DecidableEq F] (a : F) : have hnewx : (x*w) * (x*w) = a * (b * (w*w)) := by rw [show (x*w) * (x*w) = (x*x) * (w*w) from by ring, hx]; ring have hnewb : (b * (w*w))^(2^(k-1)) = 1 := by - rw [hw2, mul_pow, hbm1, ← pow_mul, ← pow_add, show (y-k) + (k-1) = y-1 from by omega, hcm1] + rw [hw2, mul_pow, hbm1, ← pow_mul, ← pow_add, show (y - k) + (k-1) = y-1 from by omega, hcm1] ring have hnewc : orderOf (w*w) = 2^k := by - rw [hw2, orderOf_pow' c (pow_ne_zero (y-k) (by norm_num)), hc, - Nat.gcd_eq_right (pow_dvd_pow 2 (by omega : y-k ≤ y)), - Nat.pow_div (by omega : y-k ≤ y) (by norm_num), show y - (y-k) = k from by omega] + rw [hw2, orderOf_pow' c (pow_ne_zero (y - k) (by norm_num)), hc, + Nat.gcd_eq_right (pow_dvd_pow 2 (by omega : y - k ≤ y)), + Nat.pow_div (by omega : y - k ≤ y) (by norm_num), show y - (y - k) = k from by omega] have hkf : k ≤ fuel := by omega simp only [loop, if_neg hb1] exact ih (x*w) (b * (w*w)) (w*w) k hkf hnewx hnewb hnewc @@ -311,7 +311,7 @@ theorem sqrt?_isSome_of_isSquare {F : Type*} [Field F] [Fintype F] [DecidableEq exact absurd (by rw [fpow_spec, ← hexp]; exact (FiniteField.isSquare_iff hchar h0).mp ha) h1 /-- A valid `rootOfUnity` is a quadratic non-residue. It has full 2-power order, so its -Euler power `rootOfUnity ^ ((card-1)/2) = (rootOfUnity ^ (2^(twoAdicity-1)))^oddPart` +Euler power `rootOfUnity^((card-1)/2) = (rootOfUnity^(2^(twoAdicity-1)))^oddPart` evaluates to `(-1)^oddPart = -1`, whereas Euler's criterion gives `1` for a nonzero square. This lets a deployment reuse `rootOfUnity` as an auxiliary nonsquare with no per-field computation. -/ @@ -329,15 +329,15 @@ theorem rootOfUnity_not_isSquare {F : Type*} [Field F] [Fintype F] have hexp : Fintype.card F / 2 = 2^(d.twoAdicity - 1) * d.oddPart := by rw [d.valid.card_eq, hpow, mul_assoc]; omega -- `rootOfUnity ≠ 0`, since it has a power equal to `1`. - have hone : d.rootOfUnity ^ 2^d.twoAdicity = 1 := by + have hone : d.rootOfUnity^(2^d.twoAdicity) = 1 := by rw [← d.valid.rootOfUnity_order]; exact pow_orderOf_eq_one _ have hne : d.rootOfUnity ≠ 0 := fun h0 => by rw [h0, zero_pow (by positivity : (2:ℕ)^d.twoAdicity ≠ 0)] at hone exact zero_ne_one hone -- The half power squares to `1` but is not `1` (the order is too big), so it is `-1`. - have hhalf : d.rootOfUnity ^ 2^(d.twoAdicity - 1) = -1 := by - have hsq1 : d.rootOfUnity ^ 2^(d.twoAdicity - 1) - * d.rootOfUnity ^ 2^(d.twoAdicity - 1) = 1 := by + have hhalf : d.rootOfUnity^(2^(d.twoAdicity - 1)) = -1 := by + have hsq1 : d.rootOfUnity^(2^(d.twoAdicity - 1)) + * d.rootOfUnity^(2^(d.twoAdicity - 1)) = 1 := by rw [← pow_add, ← two_mul, ← hpow]; exact hone refine (mul_self_eq_one_iff.mp hsq1).resolve_left fun h1 => ?_ have hdvd : orderOf d.rootOfUnity ∣ 2^(d.twoAdicity - 1) := @@ -347,7 +347,7 @@ theorem rootOfUnity_not_isSquare {F : Type*} [Field F] [Fintype F] have := d.valid.twoAdicity_pos omega -- Euler's power of the square is `1`, but it evaluates to `(-1)^oddPart = -1`. - have heuler : d.rootOfUnity ^ (Fintype.card F / 2) = 1 := + have heuler : d.rootOfUnity^(Fintype.card F / 2) = 1 := (FiniteField.isSquare_iff hchar hne).mp hsq rw [hexp, pow_mul, hhalf, d.valid.oddPart_odd.neg_one_pow] at heuler exact Ring.neg_one_ne_one_of_char_ne_two hchar heuler diff --git a/CompElliptic/Hashing/PastaSSWU.lean b/CompElliptic/Hashing/PastaSSWU.lean index 0983e34..b90a1a1 100644 --- a/CompElliptic/Hashing/PastaSSWU.lean +++ b/CompElliptic/Hashing/PastaSSWU.lean @@ -64,18 +64,18 @@ namespace CompElliptic.Curves.Pasta namespace Pallas -/-- `-13` is a quadratic non-residue in the Pallas base field: Euler's criterion, -with the power evaluated by fast modular exponentiation. -/ +/-- `-13` is a quadratic non-residue in the Pallas base field, by Euler's +criterion with the power evaluated by fast modular exponentiation. -/ theorem neg_thirteen_not_isSquare : ¬ IsSquare (-13 : PallasBaseField) := by rw [ZMod.euler_criterion PALLAS_BASE_CARD (by decide : (-13 : PallasBaseField) ≠ 0)] reduce_mod_char decide -/-- The precomputed resolvent root for RFC 9380's criterion 3 on iso-Pallas is not a -cube: `not_exists_pow_eq_of_pow_ne_one`, with the power evaluated by fast modular -exponentiation as for `neg_five_not_isCube`. -/ +/-- The precomputed resolvent root for RFC 9380's criterion 3 on iso-Pallas is not +a cube, by `not_exists_pow_eq_of_pow_ne_one` with the power evaluated by fast +modular exponentiation, as for `neg_five_not_isCube`. -/ theorem crit3_w_not_isCube : ¬ ∃ u : PallasBaseField, - u ^ 3 = (0x27234601c28978a85e0960ed291d6536dbecfb7c12f0173667d69bce9a3d69bc + u^3 = (0x27234601c28978a85e0960ed291d6536dbecfb7c12f0173667d69bce9a3d69bc : PallasBaseField) := by have hcard : Fintype.card PallasBaseField = PALLAS_BASE_CARD := ZMod.card _ refine Fields.not_exists_pow_eq_of_pow_ne_one (n := 3) (by rw [hcard]; decide) @@ -241,18 +241,18 @@ end Pallas namespace Vesta -/-- `-13` is a quadratic non-residue in the Vesta base field: Euler's criterion, -with the power evaluated by fast modular exponentiation. -/ +/-- `-13` is a quadratic non-residue in the Vesta base field, by Euler's +criterion with the power evaluated by fast modular exponentiation. -/ theorem neg_thirteen_not_isSquare : ¬ IsSquare (-13 : VestaBaseField) := by rw [ZMod.euler_criterion PALLAS_SCALAR_CARD (by decide : (-13 : VestaBaseField) ≠ 0)] reduce_mod_char decide -/-- The precomputed resolvent root for RFC 9380's criterion 3 on iso-Vesta is not a -cube: `not_exists_pow_eq_of_pow_ne_one`, with the power evaluated by fast modular -exponentiation as for `neg_five_not_isCube`. -/ +/-- The precomputed resolvent root for RFC 9380's criterion 3 on iso-Vesta is not +a cube, by `not_exists_pow_eq_of_pow_ne_one` with the power evaluated by fast +modular exponentiation, as for `neg_five_not_isCube`. -/ theorem crit3_w_not_isCube : ¬ ∃ u : VestaBaseField, - u ^ 3 = (0x2236a351e7028c01c80f079ca37fd81fd024e547a51813136e8516e4eaf7d998 + u^3 = (0x2236a351e7028c01c80f079ca37fd81fd024e547a51813136e8516e4eaf7d998 : VestaBaseField) := by have hcard : Fintype.card VestaBaseField = PALLAS_SCALAR_CARD := ZMod.card _ refine Fields.not_exists_pow_eq_of_pow_ne_one (n := 3) (by rw [hcard]; decide) @@ -402,10 +402,10 @@ yet, because Orchard's group hash targets Pallas — the gap is -- The script's printed Jacobian output, converted to the affine point pinned below. example : ((0x12763505036e0e1a6684b7a7d8d5afb7378cc2b191a95e34f44824a06fcbd08e - / 0x1b58d4aa4d68c3f4d9916b77c79ff9911597a27f2ee46244e98eb9615172d2ad ^ 2 : + / 0x1b58d4aa4d68c3f4d9916b77c79ff9911597a27f2ee46244e98eb9615172d2ad^2 : VestaBaseField), (0x0256eafc0188b79bfa7c4b2b393893ddc298e90da500fa4a9aee17c2ea4240e6 - / 0x1b58d4aa4d68c3f4d9916b77c79ff9911597a27f2ee46244e98eb9615172d2ad ^ 3 : + / 0x1b58d4aa4d68c3f4d9916b77c79ff9911597a27f2ee46244e98eb9615172d2ad^3 : VestaBaseField)) = (0x2e983e009cf3b86bc95f91b3411bd6cbd0a87f8c3c3dae80f3f2637084849204, 0x310fb8f3316d069a1fb9374bdbc0fb1391c864a5208b2a812341db7f50b2e106) := by diff --git a/CompElliptic/Hashing/SimplifiedSWU.lean b/CompElliptic/Hashing/SimplifiedSWU.lean index 95d8a87..3b4dec5 100644 --- a/CompElliptic/Hashing/SimplifiedSWU.lean +++ b/CompElliptic/Hashing/SimplifiedSWU.lean @@ -87,9 +87,9 @@ open CompElliptic.Fields variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] -/-- In a finite field, a nonsquare times a nonsquare is a square: the quadratic -character is multiplicative and takes the value `-1` on exactly the nonsquares, -so the product's character is `(-1)·(-1) = 1`. (In characteristic 2 the +/-- In a finite field, a nonsquare times a nonsquare is a square, because the +quadratic character is multiplicative and takes the value `-1` on exactly the +nonsquares, so the product's character is `(-1)·(-1) = 1`. (In characteristic 2 the hypothesis `¬ IsSquare a` is vacuous —every element is a square— so no characteristic assumption is needed.) -/ theorem isSquare_mul_of_not_isSquare {a b : F} @@ -179,7 +179,7 @@ structure SSWUParams (F : Type*) [Field F] [Fintype F] [DecidableEq F] where θ_spec : θ * θ * lam = Z sgn : F → Bool crit2 : Z ≠ -1 - crit3 : ∀ x : F, x ^ 3 + E.A * x + E.B ≠ Z + crit3 : ∀ x : F, x^3 + E.A * x + E.B ≠ Z crit4 : IsSquare ((E.B / (Z * E.A))^3 + E.A * (E.B / (Z * E.A)) + E.B) namespace SSWUParams @@ -201,7 +201,7 @@ a signed lift (`map_eq_signedLift`). -/ def mapXYUpToSign (G : SSWUParams F) (u : F) : F × F := let Zuu := G.Z * u^2 let ta := Zuu^2 + Zuu - let x1num := G.E.B * (ta + 1) + let x1num := G.E.B * (ta+1) let xdiv := G.E.A * (if ta = 0 then G.Z else -ta) let U := (x1num^2 + G.E.A * xdiv^2) * x1num + G.E.B * xdiv^3 let x2num := Zuu * x1num @@ -226,7 +226,7 @@ theorem onCurve_mapXY (G : SSWUParams F) (u : F) : simp only [mapXY, mapXYUpToSign] set Zuu := G.Z * u^2 with hZuu set ta := Zuu^2 + Zuu with hta - set x1num := G.E.B * (ta + 1) with hx1num + set x1num := G.E.B * (ta+1) with hx1num set xdiv := G.E.A * (if ta = 0 then G.Z else -ta) with hxdiv set U := (x1num^2 + G.E.A * xdiv^2) * x1num + G.E.B * xdiv^3 with hU set x2num := Zuu * x1num with hx2num diff --git a/CompElliptic/Hashing/TwoTermUniformity.lean b/CompElliptic/Hashing/TwoTermUniformity.lean index 808ade6..a3c08a8 100644 --- a/CompElliptic/Hashing/TwoTermUniformity.lean +++ b/CompElliptic/Hashing/TwoTermUniformity.lean @@ -25,7 +25,7 @@ distance of uniform on the whole group. The DFT analyzes a signal on `ℤ/N` against the reference waves `a ↦ exp (2πi·k·a/N)`, one per frequency `k`. What makes those waves work is not anything analytic about the exponential — it is the identity -`exp(2πi·k·(a+b)/N) = exp(2πi·k·a/N) · exp(2πi·k·b/N)`, which turns addition of +`exp(2πi·k·(a + b)/N) = exp(2πi·k·a/N) · exp(2πi·k·b/N)`, which turns addition of signal positions into multiplication of wave values. A **character** of a finite abelian group `G` keeps exactly that property and discards the rest: it is a map `ψ : G → ℂ` with `ψ (a + b) = ψ a * ψ b` (so `ψ 0 = 1`, and every value is a root diff --git a/CompElliptic/Isogenies/Homomorphism.lean b/CompElliptic/Isogenies/Homomorphism.lean index da80d8d..ff68d15 100644 --- a/CompElliptic/Isogenies/Homomorphism.lean +++ b/CompElliptic/Isogenies/Homomorphism.lean @@ -55,19 +55,19 @@ theorem chord_x_compat (h2 : (2 : F) ≠ 0) (h₃ : OnCurve I.domain.A I.domain.B (x₃, y₃)) (hne : x₁ ≠ x₂) (hlam : lam = (y₂ - y₁) / (x₂ - x₁)) - (hx₃ : x₃ = lam ^ 2 - x₁ - x₂) + (hx₃ : x₃ = lam^2 - x₁ - x₂) (hy₃ : y₃ = lam * (x₁ - x₃) - y₁) : (I.mapXY x₃ y₃).1 = (((I.mapXY x₂ y₂).2 - (I.mapXY x₁ y₁).2) - / ((I.mapXY x₂ y₂).1 - (I.mapXY x₁ y₁).1)) ^ 2 + / ((I.mapXY x₂ y₂).1 - (I.mapXY x₁ y₁).1))^2 - (I.mapXY x₁ y₁).1 - (I.mapXY x₂ y₂).1 := by have hdd : x₁ - x₂ ≠ 0 := sub_ne_zero.mpr hne have hxx : x₂ - x₁ ≠ 0 := sub_ne_zero.mpr (Ne.symm hne) have hd₁ : x₁ - I.x₀ ≠ 0 := sub_ne_zero.mpr (I.ne_x₀ h₁) have hd₂ : x₂ - I.x₀ ≠ 0 := sub_ne_zero.mpr (I.ne_x₀ h₂) have hd₃ : x₃ - I.x₀ ≠ 0 := sub_ne_zero.mpr (I.ne_x₀ h₃) - have hc₁ : y₁ ^ 2 = x₁ ^ 3 + I.domain.A * x₁ + I.domain.B := h₁ - have hc₂ : y₂ ^ 2 = x₂ ^ 3 + I.domain.A * x₂ + I.domain.B := h₂ + have hc₁ : y₁^2 = x₁^3 + I.domain.A * x₁ + I.domain.B := h₁ + have hc₂ : y₂^2 = x₂^3 + I.domain.A * x₂ + I.domain.B := h₂ have hslope : y₂ - y₁ = lam * (x₂ - x₁) := by rw [hlam, div_mul_cancel₀ _ hxx] set m' : F := y₁ - lam * (x₁ - I.x₀) with hm' @@ -75,8 +75,8 @@ theorem chord_x_compat (h2 : (2 : F) ≠ 0) have hL2 : y₂ = lam * (x₂ - I.x₀) + m' := by linear_combination hslope - hm' have hbridge := chord_psi3_bridge ((x₁ - I.x₀) + (x₂ - I.x₀)) (x₁ - x₂) lam m' I.x₀ I.domain.A I.domain.B - (by linear_combination 8 * hc₁ - 8 * (y₁ + lam * (x₁ - I.x₀) + m') * hL1) - (by linear_combination 8 * hc₂ - 8 * (y₂ + lam * (x₂ - I.x₀) + m') * hL2) + (by linear_combination 8*hc₁ - 8 * (y₁ + lam * (x₁ - I.x₀) + m') * hL1) + (by linear_combination 8*hc₂ - 8 * (y₂ + lam * (x₂ - I.x₀) + m') * hL2) I.psi3 have hp_inst := (mul_eq_zero.mp hbridge).resolve_left (mul_ne_zero hdd (pow_ne_zero 1 h2)) @@ -84,23 +84,23 @@ theorem chord_x_compat (h2 : (2 : F) ≠ 0) have h2p6 : ((2 : F)^6) ≠ 0 := pow_ne_zero _ h2 have hsem_ns := chord_ns_semantics ((x₁ - I.x₀) + (x₂ - I.x₀)) (x₁ - x₂) lam m' I.x₀ I.domain.A I.domain.B - (by linear_combination 8 * hc₁ - 8 * (y₁ + lam * (x₁ - I.x₀) + m') * hL1) - (by linear_combination 8 * hc₂ - 8 * (y₂ + lam * (x₂ - I.x₀) + m') * hL2) + (by linear_combination 8*hc₁ - 8 * (y₁ + lam * (x₁ - I.x₀) + m') * hL1) + (by linear_combination 8*hc₂ - 8 * (y₂ + lam * (x₂ - I.x₀) + m') * hL2) have hsem_ws := chord_ws_semantics ((x₁ - I.x₀) + (x₂ - I.x₀)) (x₁ - x₂) lam m' I.x₀ I.domain.A I.domain.B - (by linear_combination 8 * hc₁ - 8 * (y₁ + lam * (x₁ - I.x₀) + m') * hL1) - (by linear_combination 8 * hc₂ - 8 * (y₂ + lam * (x₂ - I.x₀) + m') * hL2) + (by linear_combination 8*hc₁ - 8 * (y₁ + lam * (x₁ - I.x₀) + m') * hL1) + (by linear_combination 8*hc₂ - 8 * (y₂ + lam * (x₂ - I.x₀) + m') * hL2) obtain ⟨nsv, hnsv⟩ : ∃ n : F, - n = (I.xnum x₂ * (x₁ - I.x₀) ^ 2 - I.xnum x₁ * (x₂ - I.x₀) ^ 2) / (x₁ - x₂) := ⟨_, rfl⟩ + n = (I.xnum x₂ * (x₁ - I.x₀)^2 - I.xnum x₁ * (x₂ - I.x₀)^2) / (x₁ - x₂) := ⟨_, rfl⟩ obtain ⟨wsv, hwsv⟩ : ∃ w : F, - w = ((lam * (x₂ - I.x₀) + m') * I.ynum x₂ * (x₁ - I.x₀) ^ 3 - - (lam * (x₁ - I.x₀) + m') * I.ynum x₁ * (x₂ - I.x₀) ^ 3) / (x₁ - x₂) := ⟨_, rfl⟩ + w = ((lam * (x₂ - I.x₀) + m') * I.ynum x₂ * (x₁ - I.x₀)^3 + - (lam * (x₁ - I.x₀) + m') * I.ynum x₁ * (x₂ - I.x₀)^3) / (x₁ - x₂) := ⟨_, rfl⟩ have hNNv : (x₁ - x₂) * nsv - = I.xnum x₂ * (x₁ - I.x₀) ^ 2 - I.xnum x₁ * (x₂ - I.x₀) ^ 2 := by + = I.xnum x₂ * (x₁ - I.x₀)^2 - I.xnum x₁ * (x₂ - I.x₀)^2 := by rw [hnsv]; field_simp have hWv : (x₁ - x₂) * wsv - = (lam * (x₂ - I.x₀) + m') * I.ynum x₂ * (x₁ - I.x₀) ^ 3 - - (lam * (x₁ - I.x₀) + m') * I.ynum x₁ * (x₂ - I.x₀) ^ 3 := by + = (lam * (x₂ - I.x₀) + m') * I.ynum x₂ * (x₁ - I.x₀)^3 + - (lam * (x₁ - I.x₀) + m') * I.ynum x₁ * (x₂ - I.x₀)^3 := by rw [hwsv]; field_simp have hcert := chord_x_certificate ((x₁ - I.x₀) + (x₂ - I.x₀)) (x₁ - x₂) lam m' I.x₀ nsv wsv hp_inst @@ -114,76 +114,76 @@ theorem chord_x_compat (h2 : (2 : F) ≠ 0) linear_combination ((2 : F)^12) * hW + hsem_ws)) have hcorr := chord_final_correction ((x₁ - I.x₀) + (x₂ - I.x₀)) (x₁ - x₂) lam m' I.x₀ I.domain.A I.domain.B - (by linear_combination 8 * hc₁ - 8 * (y₁ + lam * (x₁ - I.x₀) + m') * hL1) - (by linear_combination 8 * hc₂ - 8 * (y₂ + lam * (x₂ - I.x₀) + m') * hL2) + (by linear_combination 8*hc₁ - 8 * (y₁ + lam * (x₁ - I.x₀) + m') * hL1) + (by linear_combination 8*hc₂ - 8 * (y₂ + lam * (x₂ - I.x₀) + m') * hL2) I.psi3 -- defining equations of the image values, cleared of their denominators - have hX₁ : (I.mapXY x₁ y₁).1 * (x₁ - I.x₀) ^ 2 = I.s ^ 2 * I.xnum x₁ := by + have hX₁ : (I.mapXY x₁ y₁).1 * (x₁ - I.x₀)^2 = I.s^2 * I.xnum x₁ := by simp only [mapXY] exact div_mul_cancel₀ _ (pow_ne_zero 2 hd₁) - have hX₂ : (I.mapXY x₂ y₂).1 * (x₂ - I.x₀) ^ 2 = I.s ^ 2 * I.xnum x₂ := by + have hX₂ : (I.mapXY x₂ y₂).1 * (x₂ - I.x₀)^2 = I.s^2 * I.xnum x₂ := by simp only [mapXY] exact div_mul_cancel₀ _ (pow_ne_zero 2 hd₂) - have hX₃ : (I.mapXY x₃ y₃).1 * (x₃ - I.x₀) ^ 2 = I.s ^ 2 * I.xnum x₃ := by + have hX₃ : (I.mapXY x₃ y₃).1 * (x₃ - I.x₀)^2 = I.s^2 * I.xnum x₃ := by simp only [mapXY] exact div_mul_cancel₀ _ (pow_ne_zero 2 hd₃) - have hY₁ : (I.mapXY x₁ y₁).2 * (x₁ - I.x₀) ^ 3 - = I.s ^ 3 * ((lam * (x₁ - I.x₀) + m') * I.ynum x₁) := by + have hY₁ : (I.mapXY x₁ y₁).2 * (x₁ - I.x₀)^3 + = I.s^3 * ((lam * (x₁ - I.x₀) + m') * I.ynum x₁) := by simp only [mapXY] rw [← hL1] exact div_mul_cancel₀ _ (pow_ne_zero 3 hd₁) - have hY₂ : (I.mapXY x₂ y₂).2 * (x₂ - I.x₀) ^ 3 - = I.s ^ 3 * ((lam * (x₂ - I.x₀) + m') * I.ynum x₂) := by + have hY₂ : (I.mapXY x₂ y₂).2 * (x₂ - I.x₀)^3 + = I.s^3 * ((lam * (x₂ - I.x₀) + m') * I.ynum x₂) := by simp only [mapXY] rw [← hL2] exact div_mul_cancel₀ _ (pow_ne_zero 3 hd₂) -- the difference and sum equations, in terms of the atoms - have hΔX : ((I.mapXY x₂ y₂).1 - (I.mapXY x₁ y₁).1) * ((x₁ - I.x₀) ^ 2 * (x₂ - I.x₀) ^ 2) - = I.s ^ 2 * ((x₁ - x₂) * nsv) := by - linear_combination (x₁ - I.x₀) ^ 2 * hX₂ - (x₂ - I.x₀) ^ 2 * hX₁ - I.s ^ 2 * hNNv - have hΔY : ((I.mapXY x₂ y₂).2 - (I.mapXY x₁ y₁).2) * ((x₁ - I.x₀) ^ 3 * (x₂ - I.x₀) ^ 3) - = I.s ^ 3 * ((x₁ - x₂) * wsv) := by - linear_combination (x₁ - I.x₀) ^ 3 * hY₂ - (x₂ - I.x₀) ^ 3 * hY₁ - I.s ^ 3 * hWv + have hΔX : ((I.mapXY x₂ y₂).1 - (I.mapXY x₁ y₁).1) * ((x₁ - I.x₀)^2 * (x₂ - I.x₀)^2) + = I.s^2 * ((x₁ - x₂) * nsv) := by + linear_combination (x₁ - I.x₀)^2 * hX₂ - (x₂ - I.x₀)^2 * hX₁ - I.s^2 * hNNv + have hΔY : ((I.mapXY x₂ y₂).2 - (I.mapXY x₁ y₁).2) * ((x₁ - I.x₀)^3 * (x₂ - I.x₀)^3) + = I.s^3 * ((x₁ - x₂) * wsv) := by + linear_combination (x₁ - I.x₀)^3 * hY₂ - (x₂ - I.x₀)^3 * hY₁ - I.s^3 * hWv have hsumX : ((I.mapXY x₃ y₃).1 + (I.mapXY x₁ y₁).1 + (I.mapXY x₂ y₂).1) - * ((x₁ - I.x₀) ^ 2 * (x₂ - I.x₀) ^ 2 * (x₃ - I.x₀) ^ 2) - = I.s ^ 2 * (I.xnum x₃ * (x₁ - I.x₀) ^ 2 * (x₂ - I.x₀) ^ 2 - + I.xnum x₁ * (x₂ - I.x₀) ^ 2 * (x₃ - I.x₀) ^ 2 - + I.xnum x₂ * (x₁ - I.x₀) ^ 2 * (x₃ - I.x₀) ^ 2) := by - linear_combination (x₁ - I.x₀) ^ 2 * (x₂ - I.x₀) ^ 2 * hX₃ - + (x₂ - I.x₀) ^ 2 * (x₃ - I.x₀) ^ 2 * hX₁ + (x₁ - I.x₀) ^ 2 * (x₃ - I.x₀) ^ 2 * hX₂ + * ((x₁ - I.x₀)^2 * (x₂ - I.x₀)^2 * (x₃ - I.x₀)^2) + = I.s^2 * (I.xnum x₃ * (x₁ - I.x₀)^2 * (x₂ - I.x₀)^2 + + I.xnum x₁ * (x₂ - I.x₀)^2 * (x₃ - I.x₀)^2 + + I.xnum x₂ * (x₁ - I.x₀)^2 * (x₃ - I.x₀)^2) := by + linear_combination (x₁ - I.x₀)^2 * (x₂ - I.x₀)^2 * hX₃ + + (x₂ - I.x₀)^2 * (x₃ - I.x₀)^2 * hX₁ + (x₁ - I.x₀)^2 * (x₃ - I.x₀)^2 * hX₂ -- the image abscissas are distinct have hXne : (I.mapXY x₂ y₂).1 - (I.mapXY x₁ y₁).1 ≠ 0 := by intro h0 exact hne (I.abscissa_inj h2 hd h₁ h₂ (sub_eq_zero.mp h0).symm) subst hx₃ -- the cleared, slope-free key equation, closed by the certificate and correction - have hkeyc : (2 : F) ^ 10 - * ((((I.mapXY (lam ^ 2 - x₁ - x₂) y₃).1 + (I.mapXY x₁ y₁).1 + (I.mapXY x₂ y₂).1) - * ((x₁ - I.x₀) ^ 2 * (x₂ - I.x₀) ^ 2 * (lam ^ 2 - x₁ - x₂ - I.x₀) ^ 2)) - * (((I.mapXY x₂ y₂).1 - (I.mapXY x₁ y₁).1) * ((x₁ - I.x₀) ^ 2 * (x₂ - I.x₀) ^ 2)) ^ 2) - = (2 : F) ^ 10 - * ((((I.mapXY x₂ y₂).2 - (I.mapXY x₁ y₁).2) * ((x₁ - I.x₀) ^ 3 * (x₂ - I.x₀) ^ 3)) ^ 2 - * (lam ^ 2 - x₁ - x₂ - I.x₀) ^ 2) := by - have hN₁ : I.xnum x₁ = x₁ * (x₁ - I.x₀) ^ 2 - + 2 * (3 * I.x₀ ^ 2 + I.domain.A) * (x₁ - I.x₀) - + 4 * (I.x₀ ^ 3 + I.domain.A * I.x₀ + I.domain.B) := rfl - have hN₂ : I.xnum x₂ = x₂ * (x₂ - I.x₀) ^ 2 - + 2 * (3 * I.x₀ ^ 2 + I.domain.A) * (x₂ - I.x₀) - + 4 * (I.x₀ ^ 3 + I.domain.A * I.x₀ + I.domain.B) := rfl - have hN₃ : I.xnum (lam ^ 2 - x₁ - x₂) = (lam ^ 2 - x₁ - x₂) * (lam ^ 2 - x₁ - x₂ - I.x₀) ^ 2 - + 2 * (3 * I.x₀ ^ 2 + I.domain.A) * (lam ^ 2 - x₁ - x₂ - I.x₀) - + 4 * (I.x₀ ^ 3 + I.domain.A * I.x₀ + I.domain.B) := rfl + have hkeyc : (2 : F)^10 + * ((((I.mapXY (lam^2 - x₁ - x₂) y₃).1 + (I.mapXY x₁ y₁).1 + (I.mapXY x₂ y₂).1) + * ((x₁ - I.x₀)^2 * (x₂ - I.x₀)^2 * (lam^2 - x₁ - x₂ - I.x₀)^2)) + * (((I.mapXY x₂ y₂).1 - (I.mapXY x₁ y₁).1) * ((x₁ - I.x₀)^2 * (x₂ - I.x₀)^2))^2) + = (2 : F)^10 + * ((((I.mapXY x₂ y₂).2 - (I.mapXY x₁ y₁).2) * ((x₁ - I.x₀)^3 * (x₂ - I.x₀)^3))^2 + * (lam^2 - x₁ - x₂ - I.x₀)^2) := by + have hN₁ : I.xnum x₁ = x₁ * (x₁ - I.x₀)^2 + + 2 * (3 * I.x₀^2 + I.domain.A) * (x₁ - I.x₀) + + 4 * (I.x₀^3 + I.domain.A * I.x₀ + I.domain.B) := rfl + have hN₂ : I.xnum x₂ = x₂ * (x₂ - I.x₀)^2 + + 2 * (3 * I.x₀^2 + I.domain.A) * (x₂ - I.x₀) + + 4 * (I.x₀^3 + I.domain.A * I.x₀ + I.domain.B) := rfl + have hN₃ : I.xnum (lam^2 - x₁ - x₂) = (lam^2 - x₁ - x₂) * (lam^2 - x₁ - x₂ - I.x₀)^2 + + 2 * (3 * I.x₀^2 + I.domain.A) * (lam^2 - x₁ - x₂ - I.x₀) + + 4 * (I.x₀^3 + I.domain.A * I.x₀ + I.domain.B) := rfl rw [hsumX, hΔX, hΔY, hN₁, hN₂, hN₃] - linear_combination I.s ^ 6 * hcert + I.s ^ 6 * (x₁ - x₂) * nsv ^ 2 * hcorr - have hkey : ((I.mapXY (lam ^ 2 - x₁ - x₂) y₃).1 + (I.mapXY x₁ y₁).1 + (I.mapXY x₂ y₂).1) - * ((I.mapXY x₂ y₂).1 - (I.mapXY x₁ y₁).1) ^ 2 - = ((I.mapXY x₂ y₂).2 - (I.mapXY x₁ y₁).2) ^ 2 := + linear_combination I.s^6 * hcert + I.s^6 * (x₁ - x₂) * nsv^2 * hcorr + have hkey : ((I.mapXY (lam^2 - x₁ - x₂) y₃).1 + (I.mapXY x₁ y₁).1 + (I.mapXY x₂ y₂).1) + * ((I.mapXY x₂ y₂).1 - (I.mapXY x₁ y₁).1)^2 + = ((I.mapXY x₂ y₂).2 - (I.mapXY x₁ y₁).2)^2 := mul_right_cancel₀ (mul_ne_zero (mul_ne_zero (pow_ne_zero 6 hd₁) (pow_ne_zero 6 hd₂)) (pow_ne_zero 2 hd₃)) (mul_left_cancel₀ (pow_ne_zero 10 h2) (by linear_combination hkeyc)) have hdiv : (((I.mapXY x₂ y₂).2 - (I.mapXY x₁ y₁).2) - / ((I.mapXY x₂ y₂).1 - (I.mapXY x₁ y₁).1)) ^ 2 - = (I.mapXY (lam ^ 2 - x₁ - x₂) y₃).1 + (I.mapXY x₁ y₁).1 + (I.mapXY x₂ y₂).1 := by + / ((I.mapXY x₂ y₂).1 - (I.mapXY x₁ y₁).1))^2 + = (I.mapXY (lam^2 - x₁ - x₂) y₃).1 + (I.mapXY x₁ y₁).1 + (I.mapXY x₂ y₂).1 := by rw [div_pow, ← hkey] exact mul_div_cancel_right₀ _ (pow_ne_zero 2 hXne) linear_combination -hdiv @@ -200,38 +200,38 @@ theorem tangent_x_compat (h2 : (2 : F) ≠ 0) (h₁ : OnCurve I.domain.A I.domain.B (x₁, y₁)) (h₃ : OnCurve I.domain.A I.domain.B (x₃, y₃)) (hy₁ : y₁ ≠ 0) - (hlam : lam = (3 * x₁ ^ 2 + I.domain.A) / (2 * y₁)) - (hx₃ : x₃ = lam ^ 2 - x₁ - x₁) + (hlam : lam = (3 * x₁^2 + I.domain.A) / (2*y₁)) + (hx₃ : x₃ = lam^2 - x₁ - x₁) (hy₃ : y₃ = lam * (x₁ - x₃) - y₁) : (I.mapXY x₃ y₃).1 = - ((3 * (I.mapXY x₁ y₁).1 ^ 2 + I.codomain.A) / (2 * (I.mapXY x₁ y₁).2)) ^ 2 + ((3 * (I.mapXY x₁ y₁).1^2 + I.codomain.A) / (2 * (I.mapXY x₁ y₁).2))^2 - (I.mapXY x₁ y₁).1 - (I.mapXY x₁ y₁).1 := by have hd₁ : x₁ - I.x₀ ≠ 0 := sub_ne_zero.mpr (I.ne_x₀ h₁) have hd₃ : x₃ - I.x₀ ≠ 0 := sub_ne_zero.mpr (I.ne_x₀ h₃) - have hc₁ : y₁ ^ 2 = x₁ ^ 3 + I.domain.A * x₁ + I.domain.B := h₁ + have hc₁ : y₁^2 = x₁^3 + I.domain.A * x₁ + I.domain.B := h₁ have h2y : (2 : F) * y₁ ≠ 0 := mul_ne_zero h2 hy₁ - have hslope : lam * (2 * y₁) = 3 * x₁ ^ 2 + I.domain.A := by + have hslope : lam * (2*y₁) = 3 * x₁^2 + I.domain.A := by rw [hlam, div_mul_cancel₀ _ h2y] set v' : F := y₁ - lam * (x₁ - I.x₀) with hv' have hL : y₁ = lam * (x₁ - I.x₀) + v' := by linear_combination -hv' have hbridgeT := tangent_psi3_bridge (x₁ - I.x₀) lam v' I.x₀ I.domain.A I.domain.B (by linear_combination hc₁ - (y₁ + lam * (x₁ - I.x₀) + v') * hL) - (by linear_combination hslope - 2 * lam * hL) + (by linear_combination hslope - 2*lam*hL) I.psi3 have hsem_k := tangent_k_semantics (x₁ - I.x₀) lam v' I.x₀ I.domain.A I.domain.B (by linear_combination hc₁ - (y₁ + lam * (x₁ - I.x₀) + v') * hL) - (by linear_combination hslope - 2 * lam * hL) + (by linear_combination hslope - 2*lam*hL) have hsem_t := tangent_t_semantics (x₁ - I.x₀) lam v' I.x₀ I.domain.A I.domain.B (by linear_combination hc₁ - (y₁ + lam * (x₁ - I.x₀) + v') * hL) - (by linear_combination hslope - 2 * lam * hL) + (by linear_combination hslope - 2*lam*hL) have hcorrT := tangent_correction (x₁ - I.x₀) lam v' I.x₀ I.domain.A I.domain.B (by linear_combination hc₁ - (y₁ + lam * (x₁ - I.x₀) + v') * hL) - (by linear_combination hslope - 2 * lam * hL) + (by linear_combination hslope - 2*lam*hL) obtain ⟨kv, hkv⟩ : ∃ k : F, k = 2 * (lam * (x₁ - I.x₀) + v') * I.ynum x₁ * (x₁ - I.x₀) := ⟨_, rfl⟩ obtain ⟨tv, htv⟩ : ∃ t : F, - t = 3 * I.xnum x₁ ^ 2 - + (I.domain.A - 10 * (3 * I.x₀ ^ 2 + I.domain.A)) * (x₁ - I.x₀) ^ 4 := ⟨_, rfl⟩ + t = 3 * (I.xnum x₁)^2 + + (I.domain.A - 10 * (3 * I.x₀^2 + I.domain.A)) * (x₁ - I.x₀)^4 := ⟨_, rfl⟩ have hcertT := tangent_x_certificate (x₁ - I.x₀) lam v' I.x₀ kv tv hbridgeT (by @@ -242,14 +242,14 @@ theorem tangent_x_compat (h2 : (2 : F) ≠ 0) have ht := htv simp only [xnum, v, u] at ht linear_combination ht + hsem_t) - have hX₁ : (I.mapXY x₁ y₁).1 * (x₁ - I.x₀) ^ 2 = I.s ^ 2 * I.xnum x₁ := by + have hX₁ : (I.mapXY x₁ y₁).1 * (x₁ - I.x₀)^2 = I.s^2 * I.xnum x₁ := by simp only [mapXY] exact div_mul_cancel₀ _ (pow_ne_zero 2 hd₁) - have hX₃ : (I.mapXY x₃ y₃).1 * (x₃ - I.x₀) ^ 2 = I.s ^ 2 * I.xnum x₃ := by + have hX₃ : (I.mapXY x₃ y₃).1 * (x₃ - I.x₀)^2 = I.s^2 * I.xnum x₃ := by simp only [mapXY] exact div_mul_cancel₀ _ (pow_ne_zero 2 hd₃) - have hY₁ : (I.mapXY x₁ y₁).2 * (x₁ - I.x₀) ^ 3 - = I.s ^ 3 * ((lam * (x₁ - I.x₀) + v') * I.ynum x₁) := by + have hY₁ : (I.mapXY x₁ y₁).2 * (x₁ - I.x₀)^3 + = I.s^3 * ((lam * (x₁ - I.x₀) + v') * I.ynum x₁) := by simp only [mapXY] rw [← hL] exact div_mul_cancel₀ _ (pow_ne_zero 3 hd₁) @@ -257,43 +257,43 @@ theorem tangent_x_compat (h2 : (2 : F) ≠ 0) intro h0 have himg := I.onCurve_mapXY h₁ exact hc (I.mapXY x₁ y₁).1 (by rw [← h0, Prod.mk.eta]; exact himg) - have h2Y : ((2 : F) * (I.mapXY x₁ y₁).2) * (x₁ - I.x₀) ^ 4 = I.s ^ 3 * kv := by - linear_combination 2 * (x₁ - I.x₀) * hY₁ - I.s ^ 3 * hkv - have h3X : (3 * (I.mapXY x₁ y₁).1 ^ 2 + I.codomain.A) * (x₁ - I.x₀) ^ 4 - = I.s ^ 4 * tv := by + have h2Y : ((2 : F) * (I.mapXY x₁ y₁).2) * (x₁ - I.x₀)^4 = I.s^3 * kv := by + linear_combination 2 * (x₁ - I.x₀) * hY₁ - I.s^3 * hkv + have h3X : (3 * (I.mapXY x₁ y₁).1^2 + I.codomain.A) * (x₁ - I.x₀)^4 + = I.s^4 * tv := by linear_combination - 3 * ((I.mapXY x₁ y₁).1 * (x₁ - I.x₀) ^ 2 + I.s ^ 2 * I.xnum x₁) * hX₁ - + (x₁ - I.x₀) ^ 4 * I.codomain_A - I.s ^ 4 * htv + 3 * ((I.mapXY x₁ y₁).1 * (x₁ - I.x₀)^2 + I.s^2 * I.xnum x₁) * hX₁ + + (x₁ - I.x₀)^4 * I.codomain_A - I.s^4 * htv have hsumXT : ((I.mapXY x₃ y₃).1 + (I.mapXY x₁ y₁).1 + (I.mapXY x₁ y₁).1) - * ((x₁ - I.x₀) ^ 2 * (x₃ - I.x₀) ^ 2) - = I.s ^ 2 * (I.xnum x₃ * (x₁ - I.x₀) ^ 2 + 2 * I.xnum x₁ * (x₃ - I.x₀) ^ 2) := by - linear_combination (x₁ - I.x₀) ^ 2 * hX₃ + 2 * (x₃ - I.x₀) ^ 2 * hX₁ + * ((x₁ - I.x₀)^2 * (x₃ - I.x₀)^2) + = I.s^2 * (I.xnum x₃ * (x₁ - I.x₀)^2 + 2 * I.xnum x₁ * (x₃ - I.x₀)^2) := by + linear_combination (x₁ - I.x₀)^2 * hX₃ + 2 * (x₃ - I.x₀)^2 * hX₁ subst hx₃ - have hkeycT : (2 : F) ^ 2 - * ((((I.mapXY (lam ^ 2 - x₁ - x₁) y₃).1 + (I.mapXY x₁ y₁).1 + (I.mapXY x₁ y₁).1) - * ((x₁ - I.x₀) ^ 2 * (lam ^ 2 - x₁ - x₁ - I.x₀) ^ 2)) - * (((2 : F) * (I.mapXY x₁ y₁).2) * (x₁ - I.x₀) ^ 4) ^ 2) - = (2 : F) ^ 2 - * (((3 * (I.mapXY x₁ y₁).1 ^ 2 + I.codomain.A) * (x₁ - I.x₀) ^ 4) ^ 2 - * ((x₁ - I.x₀) ^ 2 * (lam ^ 2 - x₁ - x₁ - I.x₀) ^ 2)) := by - have hN₁ : I.xnum x₁ = x₁ * (x₁ - I.x₀) ^ 2 - + 2 * (3 * I.x₀ ^ 2 + I.domain.A) * (x₁ - I.x₀) - + 4 * (I.x₀ ^ 3 + I.domain.A * I.x₀ + I.domain.B) := rfl - have hN₃ : I.xnum (lam ^ 2 - x₁ - x₁) = (lam ^ 2 - x₁ - x₁) * (lam ^ 2 - x₁ - x₁ - I.x₀) ^ 2 - + 2 * (3 * I.x₀ ^ 2 + I.domain.A) * (lam ^ 2 - x₁ - x₁ - I.x₀) - + 4 * (I.x₀ ^ 3 + I.domain.A * I.x₀ + I.domain.B) := rfl + have hkeycT : (2 : F)^2 + * ((((I.mapXY (lam^2 - x₁ - x₁) y₃).1 + (I.mapXY x₁ y₁).1 + (I.mapXY x₁ y₁).1) + * ((x₁ - I.x₀)^2 * (lam^2 - x₁ - x₁ - I.x₀)^2)) + * (((2 : F) * (I.mapXY x₁ y₁).2) * (x₁ - I.x₀)^4)^2) + = (2 : F)^2 + * (((3 * (I.mapXY x₁ y₁).1^2 + I.codomain.A) * (x₁ - I.x₀)^4)^2 + * ((x₁ - I.x₀)^2 * (lam^2 - x₁ - x₁ - I.x₀)^2)) := by + have hN₁ : I.xnum x₁ = x₁ * (x₁ - I.x₀)^2 + + 2 * (3 * I.x₀^2 + I.domain.A) * (x₁ - I.x₀) + + 4 * (I.x₀^3 + I.domain.A * I.x₀ + I.domain.B) := rfl + have hN₃ : I.xnum (lam^2 - x₁ - x₁) = (lam^2 - x₁ - x₁) * (lam^2 - x₁ - x₁ - I.x₀)^2 + + 2 * (3 * I.x₀^2 + I.domain.A) * (lam^2 - x₁ - x₁ - I.x₀) + + 4 * (I.x₀^3 + I.domain.A * I.x₀ + I.domain.B) := rfl rw [hsumXT, h2Y, h3X, hN₁, hN₃] - linear_combination I.s ^ 8 * hcertT + I.s ^ 8 * kv ^ 2 * hcorrT - have hkeyT : ((I.mapXY (lam ^ 2 - x₁ - x₁) y₃).1 + (I.mapXY x₁ y₁).1 + (I.mapXY x₁ y₁).1) - * ((2 : F) * (I.mapXY x₁ y₁).2) ^ 2 - = (3 * (I.mapXY x₁ y₁).1 ^ 2 + I.codomain.A) ^ 2 := + linear_combination I.s^8 * hcertT + I.s^8 * kv^2 * hcorrT + have hkeyT : ((I.mapXY (lam^2 - x₁ - x₁) y₃).1 + (I.mapXY x₁ y₁).1 + (I.mapXY x₁ y₁).1) + * ((2 : F) * (I.mapXY x₁ y₁).2)^2 + = (3 * (I.mapXY x₁ y₁).1^2 + I.codomain.A)^2 := mul_right_cancel₀ (mul_ne_zero (pow_ne_zero 10 hd₁) (pow_ne_zero 2 hd₃)) (mul_left_cancel₀ (pow_ne_zero 2 h2) (by linear_combination hkeycT)) - have hdivT : ((3 * (I.mapXY x₁ y₁).1 ^ 2 + I.codomain.A) - / (2 * (I.mapXY x₁ y₁).2)) ^ 2 - = (I.mapXY (lam ^ 2 - x₁ - x₁) y₃).1 + (I.mapXY x₁ y₁).1 + (I.mapXY x₁ y₁).1 := by + have hdivT : ((3 * (I.mapXY x₁ y₁).1^2 + I.codomain.A) + / (2 * (I.mapXY x₁ y₁).2))^2 + = (I.mapXY (lam^2 - x₁ - x₁) y₃).1 + (I.mapXY x₁ y₁).1 + (I.mapXY x₁ y₁).1 := by rw [div_pow, ← hkeyT] - have h2Yne : ((2 : F) * (I.mapXY x₁ y₁).2) ^ 2 ≠ 0 := + have h2Yne : ((2 : F) * (I.mapXY x₁ y₁).2)^2 ≠ 0 := pow_ne_zero 2 (mul_ne_zero h2 hY₁ne) exact mul_div_cancel_right₀ _ h2Yne linear_combination -hdivT @@ -349,8 +349,8 @@ theorem map_add_x (h2 : (2 : F) ≠ 0) · -- doubling have hyq : Q.y = P.y := by have hsq : (P.y - Q.y) * (P.y + Q.y) = 0 := by - have e1 : P.y ^ 2 = P.x ^ 3 + I.domain.A * P.x + I.domain.B := hP1 - have e2 : Q.y ^ 2 = Q.x ^ 3 + I.domain.A * Q.x + I.domain.B := hQ1 + have e1 : P.y^2 = P.x^3 + I.domain.A * P.x + I.domain.B := hP1 + have e2 : Q.y^2 = Q.x^3 + I.domain.A * Q.x + I.domain.B := hQ1 rw [hxx] at e1 linear_combination e1 - e2 rcases mul_eq_zero.mp hsq with h | h @@ -363,16 +363,16 @@ theorem map_add_x (h2 : (2 : F) ≠ 0) subst hQP -- the domain doubling output have hpair : add I.domain.A (Q.x, Q.y) (Q.x, Q.y) - = (((3 * Q.x ^ 2 + I.domain.A) / (2 * Q.y)) ^ 2 - Q.x - Q.x, - ((3 * Q.x ^ 2 + I.domain.A) / (2 * Q.y)) - * (Q.x - (((3 * Q.x ^ 2 + I.domain.A) / (2 * Q.y)) ^ 2 - Q.x - Q.x)) - Q.y) := by + = (((3 * Q.x^2 + I.domain.A) / (2 * Q.y))^2 - Q.x - Q.x, + ((3 * Q.x^2 + I.domain.A) / (2 * Q.y)) + * (Q.x - (((3 * Q.x^2 + I.domain.A) / (2 * Q.y))^2 - Q.x - Q.x)) - Q.y) := by unfold add rw [if_neg hQ0, if_neg hQ0, if_pos rfl, if_neg hyy] - have hxagree : (Q + Q).x = ((3 * Q.x ^ 2 + I.domain.A) / (2 * Q.y)) ^ 2 - Q.x - Q.x := by + have hxagree : (Q + Q).x = ((3 * Q.x^2 + I.domain.A) / (2 * Q.y))^2 - Q.x - Q.x := by show (add I.domain.A (Q.x, Q.y) (Q.x, Q.y)).1 = _ rw [hpair] - have hyagree : (Q + Q).y = ((3 * Q.x ^ 2 + I.domain.A) / (2 * Q.y)) - * (Q.x - (((3 * Q.x ^ 2 + I.domain.A) / (2 * Q.y)) ^ 2 - Q.x - Q.x)) - Q.y := by + have hyagree : (Q + Q).y = ((3 * Q.x^2 + I.domain.A) / (2 * Q.y)) + * (Q.x - (((3 * Q.x^2 + I.domain.A) / (2 * Q.y))^2 - Q.x - Q.x)) - Q.y := by show (add I.domain.A (Q.x, Q.y) (Q.x, Q.y)).2 = _ rw [hpair] have h₃ : OnCurve I.domain.A I.domain.B ((Q + Q).x, (Q + Q).y) := by @@ -396,7 +396,7 @@ theorem map_add_x (h2 : (2 : F) ≠ 0) ((I.mapXY Q.x Q.y).1, (I.mapXY Q.x Q.y).2)).1 have haddimg : (add I.codomain.A ((I.mapXY Q.x Q.y).1, (I.mapXY Q.x Q.y).2) ((I.mapXY Q.x Q.y).1, (I.mapXY Q.x Q.y).2)).1 - = ((3 * (I.mapXY Q.x Q.y).1 ^ 2 + I.codomain.A) / (2 * (I.mapXY Q.x Q.y).2)) ^ 2 + = ((3 * (I.mapXY Q.x Q.y).1^2 + I.codomain.A) / (2 * (I.mapXY Q.x Q.y).2))^2 - (I.mapXY Q.x Q.y).1 - (I.mapXY Q.x Q.y).1 := by unfold add rw [if_neg himgQ0, if_neg himgQ0, if_pos rfl, @@ -408,16 +408,16 @@ theorem map_add_x (h2 : (2 : F) ≠ 0) intro hcon exact hxx (I.abscissa_inj h2 hd hP1 hQ1 hcon) have hpair : add I.domain.A (P.x, P.y) (Q.x, Q.y) - = (((Q.y - P.y) / (Q.x - P.x)) ^ 2 - P.x - Q.x, + = (((Q.y - P.y) / (Q.x - P.x))^2 - P.x - Q.x, ((Q.y - P.y) / (Q.x - P.x)) - * (P.x - (((Q.y - P.y) / (Q.x - P.x)) ^ 2 - P.x - Q.x)) - P.y) := by + * (P.x - (((Q.y - P.y) / (Q.x - P.x))^2 - P.x - Q.x)) - P.y) := by unfold add rw [if_neg hP0, if_neg hQ0, if_neg hxx] - have hxagree : (P + Q).x = ((Q.y - P.y) / (Q.x - P.x)) ^ 2 - P.x - Q.x := by + have hxagree : (P + Q).x = ((Q.y - P.y) / (Q.x - P.x))^2 - P.x - Q.x := by show (add I.domain.A (P.x, P.y) (Q.x, Q.y)).1 = _ rw [hpair] have hyagree : (P + Q).y = ((Q.y - P.y) / (Q.x - P.x)) - * (P.x - (((Q.y - P.y) / (Q.x - P.x)) ^ 2 - P.x - Q.x)) - P.y := by + * (P.x - (((Q.y - P.y) / (Q.x - P.x))^2 - P.x - Q.x)) - P.y := by show (add I.domain.A (P.x, P.y) (Q.x, Q.y)).2 = _ rw [hpair] have h₃ : OnCurve I.domain.A I.domain.B ((P + Q).x, (P + Q).y) := by @@ -435,7 +435,7 @@ theorem map_add_x (h2 : (2 : F) ≠ 0) have haddimg : (add I.codomain.A ((I.mapXY P.x P.y).1, (I.mapXY P.x P.y).2) ((I.mapXY Q.x Q.y).1, (I.mapXY Q.x Q.y).2)).1 = (((I.mapXY Q.x Q.y).2 - (I.mapXY P.x P.y).2) - / ((I.mapXY Q.x Q.y).1 - (I.mapXY P.x P.y).1)) ^ 2 + / ((I.mapXY Q.x Q.y).1 - (I.mapXY P.x P.y).1))^2 - (I.mapXY P.x P.y).1 - (I.mapXY Q.x Q.y).1 := by unfold add rw [if_neg himgP0, if_neg himgQ0, if_neg hXne] @@ -446,8 +446,8 @@ theorem map_add_x (h2 : (2 : F) ≠ 0) theorem map_neg (P : SWPoint I.domain) : I.map (-P) = -I.map P := by by_cases hP : OnCurve I.domain.A I.domain.B (P.x, P.y) · have hnP : OnCurve I.domain.A I.domain.B ((-P).x, (-P).y) := by - have h : P.y ^ 2 = P.x ^ 3 + I.domain.A * P.x + I.domain.B := hP - show (-P.y) ^ 2 = P.x ^ 3 + I.domain.A * P.x + I.domain.B + have h : P.y^2 = P.x^3 + I.domain.A * P.x + I.domain.B := hP + show (-P.y)^2 = P.x^3 + I.domain.A * P.x + I.domain.B linear_combination h apply SWPoint.ext_pair rw [map, dif_pos hnP, map, dif_pos hP] @@ -462,8 +462,8 @@ omit [DecidableEq F] in private theorem eq_or_eq_neg_of_x_eq {E : SWCurve F} {R S : SWPoint E} (hR : OnCurve E.A E.B (R.x, R.y)) (hS : OnCurve E.A E.B (S.x, S.y)) (hx : R.x = S.x) : R = S ∨ R = -S := by - have h1 : R.y ^ 2 = R.x ^ 3 + E.A * R.x + E.B := hR - have h2 : S.y ^ 2 = S.x ^ 3 + E.A * S.x + E.B := hS + have h1 : R.y^2 = R.x^3 + E.A * R.x + E.B := hR + have h2 : S.y^2 = S.x^3 + E.A * S.x + E.B := hS rw [hx] at h1 have h0 : (R.y - S.y) * (R.y + S.y) = 0 := by linear_combination h1 - h2 rcases mul_eq_zero.mp h0 with h | h diff --git a/CompElliptic/Isogenies/ThreeIsogeny.lean b/CompElliptic/Isogenies/ThreeIsogeny.lean index 6ff6c1e..3369062 100644 --- a/CompElliptic/Isogenies/ThreeIsogeny.lean +++ b/CompElliptic/Isogenies/ThreeIsogeny.lean @@ -98,8 +98,8 @@ structure ThreeIsogeny (F : Type*) [Field F] where /-- `x₀` is a root of the domain's degree-3 division polynomial `ψ₃(X) = 3·X⁴ + 6·A·X² + 12·B·X - A²`. -/ psi3 : 3 * x₀^4 + 6 * domain.A * x₀^2 + 12 * domain.B * x₀ - domain.A^2 = 0 - /-- The square of the kernel ordinate, `y₀² = x₀³ + A·x₀ + B`, is a nonsquare: the - kernel points exist only over a quadratic extension. -/ + /-- The square of the kernel ordinate, `y₀² = x₀³ + A·x₀ + B`, is a nonsquare, + so the kernel points exist only over a quadratic extension. -/ kernel_irrational : ¬ IsSquare (x₀^3 + domain.A * x₀ + domain.B) /-- The codomain's `A`, as Vélu's formulae and the scaling dictate. -/ codomain_A : codomain.A = s^4 * (domain.A - 10 * (3 * x₀^2 + domain.A)) @@ -147,15 +147,15 @@ theorem ne_x₀ {x y : F} (h : OnCurve I.domain.A I.domain.B (x, y)) : x ≠ I.x ``` R. = PolynomialRing(QQ, order='lex') g = x^3 + a*x + b - psi3 = 3*x0^4 + 6*a*x0^2 + 12*b*x0 - a^2 - v = 2*(3*x0^2 + a) - u = 4*(x0^3 + a*x0 + b) + psi3 = 3 * x0^4 + 6 * a * x0^2 + 12*b*x0 - a^2 + v = 2 * (3 * x0^2 + a) + u = 4 * (x0^3 + a*x0 + b) D = x - x0 - xnum = x*D^2 + v*D + u + xnum = x * D^2 + v*D + u ynum = D^3 - v*D - 2*u A1 = a - 5*v - B1 = b - 7*(u + v*x0) - diff = g*ynum^2 - (xnum^3 + A1*xnum*D^4 + B1*D^6) + B1 = b - 7 * (u + v*x0) + diff = g * ynum^2 - (xnum^3 + A1 * xnum * D^4 + B1 * D^6) q, r = diff.quo_rem(psi3) assert r == 0 print(q) @@ -217,31 +217,31 @@ with this Sage script: ``` R. = PolynomialRing(QQ) g0 = x0^3 + a*x0 + b - psi3 = 3*x0^4 + 6*a*x0^2 + 12*b*x0 - a^2 - v = 2*(3*x0^2 + a) + psi3 = 3 * x0^4 + 6 * a * x0^2 + 12*b*x0 - a^2 + v = 2 * (3 * x0^2 + a) uc = 4*g0 - xnum = lambda t: t*(t - x0)^2 + v*(t - x0) + uc - H = xnum(u)*(w - x0)^2 - xnum(w)*(u - x0)^2 - G = H // (u - w) # exact: (u - w) divides H - A2 = R(G.coefficient({w: 2})) # = (u - x0)^2 - A1 = R(G.coefficient({w: 1})) - disc = A1^2 - 4*A2*R(G.coefficient({w: 0})) - E = disc - 16*g0*y1^2 - c1 = R(-16*g0) - c3 = (E - c1*(y1^2 - (u^3 + a*u + b))) // psi3 # exact division - assert (2*A2*w + A1)^2 - 16*g0*y1^2 - 4*A2*G - c1*(y1^2 - (u^3+a*u+b)) - c3*psi3 == 0 + xnum = lambda t: t * (t - x0)^2 + v * (t - x0) + uc + H = xnum(u) * (w - x0)^2 - xnum(w) * (u - x0)^2 + G = H // (u - w) # exact: (u - w) divides H + A2 = R(G.coefficient({w: 2})) # = (u - x0)^2 + A1 = R(G.coefficient({w: 1})) + disc = A1^2 - 4 * A2 * R(G.coefficient({w: 0})) + E = disc - 16 * g0 * y1^2 + c1 = R(-16*g0) + c3 = (E - c1 * (y1^2 - (u^3 + a*u + b))) // psi3 # exact division + assert (2*A2*w + A1)^2 - 16 * g0 * y1^2 - 4*A2*G - c1 * (y1^2 - (u^3 + a*u + b)) - c3*psi3 == 0 ``` `G = 0` is the condition for the two abscissas to collide. It is quadratic in `w`, with leading coefficient `A2 = (u - x₀)²`, and its roots are the abscissas of the translates `P ± T`. Its discriminant (the squared difference of its roots, scaled by `A2²`) is -therefore forced to be `(x(P+T) - x(P-T))²·A2² = 16·y₀²·y₁²`, modulo the curve equation +therefore forced to be `(x(P + T) - x(P - T))²·A2² = 16·y₀²·y₁²`, modulo the curve equation and `ψ₃`. Completing the square and multiplying through by `u - w` gives the identity `abscissa_inj` consumes, with `c3 = -4·(u - x₀)²`. -/ /-- Distinct rational abscissas have distinct image abscissas. A collision would make the second abscissa a rational root of a quadratic whose discriminant is -`(x(P+T) - x(P-T))²`, the squared difference of the abscissas of the two kernel +`(x(P + T) - x(P - T))²`, the squared difference of the abscissas of the two kernel translates. That discriminant is `16·y₀²·y₁²` up to the square `(x₁ - x₀)⁴`, so a rational root exhibits the nonsquare `y₀²` as a square, contradicting `kernel_irrational`. The degenerate case `y₁ = 0` is rational 2-torsion, which `hd`