Explicit quotient coordinates on the Fermat cubic

Given an affine point (x,y) of x³ + y³ = 1 with x, y ≠ 0 and any cube root W of w = (x+1)/(x+y), the point (W,T) with T = r/W, r = (1+x+y)/(x+y), lies on the cubic and has Hessian addition coordinates exactly (x,y).

This is the algebraic content of "(x,y) is the image of (W,T) under Q ↦ Q + πQ", proved directly from the defining equation: no group law, Frobenius endomorphism, or algebraic closure is involved. Note the direction — w and z are produced in K first, and W, T are only cube roots chosen afterwards.

def KasamiCyclicAdditive.FermatCubic.quotientT {K : Type u_1} [Field K] (x y W : K) : K

The explicit degree-three quotient lift of (x, y) through a chosen cube root W of (x + 1) / (x + y).

Equations

• KasamiCyclicAdditive.FermatCubic.quotientT x y W = (1 + x + y) / (x + y) / W

theorem KasamiCyclicAdditive.FermatCubic.explicit_quotient_coordinates {K : Type u_1} [Field K] [CharP K 2] {x y W : K} (hx : x ≠ 0) (hy : y ≠ 0) (hxy : x ^ 3 + y ^ 3 = 1) (hW : W ^ 3 = (x + 1) / (x + y)) : have T := quotientT x y W; T ^ 3 = (y + 1) / (x + y) ∧ W ^ 3 + T ^ 3 = 1 ∧ hessD W T (W ^ 2) (T ^ 2) ≠ 0 ∧ hessX W T (W ^ 2) (T ^ 2) / hessD W T (W ^ 2) (T ^ 2) = x ∧ hessY W T (W ^ 2) (T ^ 2) / hessD W T (W ^ 2) (T ^ 2) = y

Explicit quotient-coordinate lemma.

Let K have characteristic two and let (x,y) be a non-3-torsion affine point of the Fermat cubic

x^3 + y^3 = 1

with x,y ≠ 0.

Suppose W is any cube root of w = (x+1)/(x+y), and let T = quotientT x y W be the lift ((1+x+y)/(x+y))/W. Then

• T^3 = (y+1)/(x+y),

• hence W^3+T^3=1,

• the Hessian denominator for (W,T) and (W^2,T^2) is nonzero,

• and the Hessian addition coordinates are exactly (x,y):

  hessX(W,T,W²,T²) / hessD(W,T,W²,T²) = x, hessY(W,T,W²,T²) / hessD(W,T,W²,T²) = y.

This is the explicit algebraic statement that (x,y) is the image of (W,T) under the quotient map represented by Q ↦ Q + Frobenius(Q), established from the formulas above alone, with no elliptic-curve group law.