Validity of the affine Fermat-incidence chart

This file formalises and verifies the affine Fermat-incidence chart. Throughout, K is a field of characteristic two (algebraic closedness is nowhere needed), E is the Fermat cubic X^3+Y^3=Z^3 with origin O=[1:1:0], realised through the Weierstrass model fer (see FermatCubic.Curve), pi is the Frobenius x ↦ x^2 and t3 = (1,0).

• hessD, hessX, hessY are the chart denominator and its two numerators;
• phi is the map Q ↦ -(Q + pi^k Q) + t3;
• hessDenom_ne_zero : the Hessian denominator is nonzero;
• hessCoords_ne_zero : both affine coordinates are nonzero;
• exists_twisted_root_equation produces the twisted root equation.

The Frobenius-twist hypothesis is stated as pi^n Q = Q + C with C = ptInf c a point at infinity; the three points at infinity are the three points of K0 = ker (1+pi), cf. neg_ptInf.

theorem KasamiCyclicAdditive.FermatCubic.frob_fermat {K : Type u_1} [Field K] [CharP K 2] {W T : K} (h : W ^ 3 + T ^ 3 = 1) (k : ℕ) : (W ^ 2 ^ k) ^ 3 + (T ^ 2 ^ k) ^ 3 = 1

The Frobenius pi^k preserves the Fermat equation.

The algebra of the Hessian numerators

theorem KasamiCyclicAdditive.FermatCubic.hess_key {K : Type u_1} [Field K] [CharP K 2] {W T A B : K} (hD : hessD W T A B = 0) : hessX W T A B * A = hessY W T A B * T

With a vanishing Hessian denominator, N_x * A = N_y * T. With A and T nonzero this makes the two numerators vanish simultaneously.

theorem KasamiCyclicAdditive.FermatCubic.hess_cube_left {K : Type u_1} [Field K] [CharP K 2] {W T A B : K} (hT : T ≠ 0) (hX : hessX W T A B = 0) (hD : hessD W T A B = 0) : A ^ 3 = W ^ 3

N_x = 0 and D0 = 0 force A^3 = W^3.

theorem KasamiCyclicAdditive.FermatCubic.hess_cube_right {K : Type u_1} [Field K] [CharP K 2] {W T A B : K} (hW : W ≠ 0) (hY : hessY W T A B = 0) (hD : hessD W T A B = 0) : B ^ 3 = T ^ 3

N_y = 0 and D0 = 0 force B^3 = T^3.

def KasamiCyclicAdditive.FermatCubic.t3 (K : Type u_2) [Field K] [CharP K 2] : (fer K).toAffine.Point

The 3-torsion point t3 = (1,0).

Equations

• KasamiCyclicAdditive.FermatCubic.t3 K = KasamiCyclicAdditive.FermatCubic.pt 1 0 ⋯

theorem KasamiCyclicAdditive.FermatCubic.three_torsion_t3 {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] : 3 • t3 K = 0

t3 = (1,0) is 3-torsion.

theorem KasamiCyclicAdditive.FermatCubic.neg_add_t3 {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] {x y d : K} (hx : x ≠ 0) (hy : y ≠ 0) (hd : d ≠ 0) (h1 : (x / d) ^ 3 + (y / d) ^ 3 = 1) (h2 : (x / y) ^ 3 + (d / y) ^ 3 = 1) : -pt (x / d) (y / d) h1 + t3 K = pt (x / y) (d / y) h2

The chart computation behind the twisted root equation: if (x/d, y/d) is an affine Fermat point with all of x, y, d nonzero, then -(x/d, y/d) + t3 = (x/y, d/y).

def KasamiCyclicAdditive.FermatCubic.phi {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] (k : ℕ) (W T : K) (h : W ^ 3 + T ^ 3 = 1) : (fer K).toAffine.Point

phi k Q = -(Q + pi^k Q) + t3.

Equations

• One or more equations did not get rendered due to their size.

theorem KasamiCyclicAdditive.FermatCubic.three_torsion_phi {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] {k : ℕ} {W T : K} (h : W ^ 3 + T ^ 3 = 1) (hsum : 3 • (pt W T h + pt (W ^ 2 ^ k) (T ^ 2 ^ k) ⋯) = 0) : 3 • phi k W T h = 0

If Q + pi^k Q is 3-torsion then so is Phi_k(Q).

theorem KasamiCyclicAdditive.FermatCubic.hessNum_ne_zero_of_hessD_eq_zero {K : Type u_1} [Field K] [CharP K 2] {W T A B : K} (hT : T ≠ 0) (hA : A ≠ 0) (hD : hessD W T A B = 0) (hN : ¬(hessX W T A B = 0 ∧ hessY W T A B = 0)) : hessX W T A B ≠ 0 ∧ hessY W T A B ≠ 0

With a vanishing Hessian denominator the two numerators vanish together, so if they do not both vanish then neither does.

theorem KasamiCyclicAdditive.FermatCubic.eq_neg_of_hessD_eq_zero {K : Type u_1} [Field K] [CharP K 2] {W T A B : K} (h : W ^ 3 + T ^ 3 = 1) (h2 : A ^ 3 + B ^ 3 = 1) (hT : T ≠ 0) (hD : hessD W T A B = 0) (hAT : A = T) : pt A B h2 = -pt W T h

With a vanishing Hessian denominator, A = T says that the second point is the negative of the first.

theorem KasamiCyclicAdditive.FermatCubic.add_ne_add_of_hessD_eq_zero {K : Type u_1} [Field K] [CharP K 2] {W T A B : K} (hD : hessD W T A B = 0) (hXne : hessX W T A B ≠ 0) (hAT : A ≠ T) : W + T ≠ A + B

Two points with a vanishing Hessian denominator that are not negatives of one another have distinct coordinate sums, so the secant denominator does not vanish.

theorem KasamiCyclicAdditive.FermatCubic.three_torsion_add_of_hessD_eq_zero {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] {W T A B : K} (h : W ^ 3 + T ^ 3 = 1) (h2 : A ^ 3 + B ^ 3 = 1) (hT : T ≠ 0) (hA : A ≠ 0) (hD : hessD W T A B = 0) (hN : ¬(hessX W T A B = 0 ∧ hessY W T A B = 0)) : 3 • (pt W T h + pt A B h2) = 0

If the Hessian denominator of two affine Fermat points vanishes while the numerators do not both vanish, then their sum lies in E[3]: it is a point at infinity [N_x : N_y : 0].

theorem KasamiCyclicAdditive.FermatCubic.not_hess_all_eq_zero {K : Type u_1} [Field K] [CharP K 2] {W T : K} {k n : ℕ} (h : W ^ 3 + T ^ 3 = 1) (hW : W ≠ 0) (hT : T ≠ 0) (hkn : k.gcd n = 1) (hX : hessX W T (W ^ 2 ^ k) (T ^ 2 ^ k) = 0) (hY : hessY W T (W ^ 2 ^ k) (T ^ 2 ^ k) = 0) (hD : hessD W T (W ^ 2 ^ k) (T ^ 2 ^ k) = 0) (hn : ∃ (c : K), c ^ 3 = 1 ∧ W ^ 2 ^ n = c * W ∧ T ^ 2 ^ n = c ^ 2 * T) : False

The Hessian denominator and both numerators cannot vanish together: under the Frobenius-twist relation with gcd (k, n) = 1, that would force W or T to be zero.

theorem KasamiCyclicAdditive.FermatCubic.hessDenom_ne_zero {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] {W T : K} {k n : ℕ} (h : W ^ 3 + T ^ 3 = 1) (hW : W ≠ 0) (hT : T ≠ 0) (hkn : k.gcd n = 1) (hB3 : ∃ (c : K) (hc : c ^ 3 = 1), pt (W ^ 2 ^ n) (T ^ 2 ^ n) ⋯ = pt W T h + ptInf c hc) (hB5 : 3 • phi k W T h ≠ 0) : hessD W T (W ^ 2 ^ k) (T ^ 2 ^ k) ≠ 0

For an affine Fermat point with both coordinates nonzero, gcd (k, n) = 1, the Frobenius-twist relation hB3, and Phi_k(Q) not 3-torsion, the Hessian denominator D0 is nonzero.

theorem KasamiCyclicAdditive.FermatCubic.hessCoords_ne_zero {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] {W T : K} {k n : ℕ} (h : W ^ 3 + T ^ 3 = 1) (hW : W ≠ 0) (hT : T ≠ 0) (hkn : k.gcd n = 1) (hB3 : ∃ (c : K) (hc : c ^ 3 = 1), pt (W ^ 2 ^ n) (T ^ 2 ^ n) ⋯ = pt W T h + ptInf c hc) (hB5 : 3 • phi k W T h ≠ 0) : hessX W T (W ^ 2 ^ k) (T ^ 2 ^ k) ≠ 0 ∧ hessY W T (W ^ 2 ^ k) (T ^ 2 ^ k) ≠ 0

Both affine coordinates of Q + pi^k Q are nonzero.

theorem KasamiCyclicAdditive.FermatCubic.hess_weighted_sum_eq_hessD {K : Type u_1} [Field K] [CharP K 2] {W T : K} {k : ℕ} (h : W ^ 3 + T ^ 3 = 1) : W ^ (2 ^ k + 1) * hessY W T (W ^ 2 ^ k) (T ^ 2 ^ k) + hessX W T (W ^ 2 ^ k) (T ^ 2 ^ k) * T ^ (2 ^ k + 1) = hessD W T (W ^ 2 ^ k) (T ^ 2 ^ k)

The Hessian coordinates, weighted by W^(2^k+1) and T^(2^k+1), recombine to the denominator.

theorem KasamiCyclicAdditive.FermatCubic.exists_twisted_root_equation {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] {W T : K} {k n : ℕ} (h : W ^ 3 + T ^ 3 = 1) (hW : W ≠ 0) (hT : T ≠ 0) (hkn : k.gcd n = 1) (hB3 : ∃ (c : K) (hc : c ^ 3 = 1), pt (W ^ 2 ^ n) (T ^ 2 ^ n) ⋯ = pt W T h + ptInf c hc) (hB5 : 3 • phi k W T h ≠ 0) : ∃ (p : K) (q : K) (hpq : p ^ 3 + q ^ 3 = 1), phi k W T h = pt p q hpq ∧ p ≠ 0 ∧ q ≠ 0 ∧ W ^ (2 ^ k + 1) + p * T ^ (2 ^ k + 1) = q

Under the Frobenius-twist relation, phi k Q is the affine point (p, q) with p = N_x/N_y and q = D0/N_y, both nonzero, and the twisted root equation W^(2^k+1) + p*T^(2^k+1) = q holds.