The even-dimensional root-existence branch: the quotient-first bridge

The quotient-first route to RootEqSolvable in even dimension.

The route. Let K = F_{2^n} with n even, target (p,q) with p,q ≠ 0.

1. PointFrobenius.exists_gMap_preimage inverts the prime-to-3 factor G on E(K) directly (no algebraic closure), producing Y with G(Y) = t3 - P.
2. Y is not 3-torsion (since t3 - P isn't), so Y = (x,y) with x,y ≠ 0.
3. Base-change (x,y) to F = AlgebraicClosure K.
4. Pick any cube root W of (x+1)/(x+y) in F and build T as in FermatCubic.explicit_quotient_coordinates: this gives a point Q = (W,T) with Q + π Q = (x,y)_F, i.e. Q is a preimage of (x,y)_F under the "quotient" map id + π.
5. Since G and 1 + π commute (both are polynomials in π), and G transports along the base-change map basePt K F (which itself commutes with π), (1 + π)(G(Q)) = G(Q + π Q) = G((x,y)_F) = (t3 - P)_F. Combined with the abstract factorization (1+π) ∘ G = 1 + π^k (Isogeny.gMap_factor), this gives (1 + π^k) Q = t3 - P over F, i.e. phi k W T = P over F.
6. The Frobenius-twist relation π^n Q = Q + ptInf α needed by exists_twisted_root_equation follows from Q + π Q being K-rational (hence fixed by the n-th Frobenius power) together with π^n commuting with 1 + π: this puts π^n Q - Q in ker(1+π), which is exactly the three points at infinity (frobFixed_eq_ptInf, a small self-contained restatement that needs no kernel-split machinery).
7. exists_twisted_root_equation gives the ambient twisted-root equation, and since W^3, T^3 were built from K-rational data before the cube root was chosen, they are already algebraMap-images of elements of K — no fixed-field descent theorem is needed.

theorem KasamiCyclicAdditive.EvenAssembly.frobFixed_eq_ptInf {F : Type u_1} [Field F] [DecidableEq F] [CharP F 2] {C : (FermatCubic.fer F).toAffine.Point} (hC : C + (PointFrobenius.frobPt F) C = 0) : ∃ (a : F) (ha : a ^ 3 = 1), C = FermatCubic.ptInf a ha

If C is fixed by -π (i.e. C + π C = 0), then C is one of the three points at infinity: ker(1 + π) = K0.

theorem KasamiCyclicAdditive.rootEquationSolvable_even {K : Type u_1} [Field K] [Fintype K] [CharP K 2] {n k m : ℕ} (hn : Even n) (hkn : k.Coprime n) (hcard : Fintype.card K = 2 ^ n) (he : 2 ^ k + 1 = 3 * m) (hm : m.Coprime (2 ^ n - 1)) : RootEqSolvable m K

The even branch: the quotient-first bridge. For even n the twisted root equation is solvable at every affine Fermat target with nonzero coordinates, by the route set out in the module docstring.