Normal forms in the split trace-cover Kummer tower

The full kernel calculation for the Laurent trace-cover map requires reducing arbitrary Laurent polynomials to a bounded monomial normal form. This file proves the risky uniqueness half of that calculation: the bounded eta--xi monomials are linearly independent over the quadratic base function ring, so no nontrivial reduced normal form can vanish in the iterated Kummer algebra.

This basis statement only uses that the two defining binomials are monic. Irreducibility, proved in TraceCurveKummer, is needed later to regard the same rings as fields, but is not smuggled into the normal-form interface.

theorem BGS.Markoff.adjoinRootTower_normalMonomials_linearIndependent {R : Type u_1} [CommRing R] (f : Polynomial R) (hf : f.Monic) (g : Polynomial (AdjoinRoot f)) (hg : g.Monic) : LinearIndependent R fun (ji : Fin f.natDegree × Fin g.natDegree) => (algebraMap (AdjoinRoot f) (AdjoinRoot g)) (AdjoinRoot.root f ^ ↑ji.1) * AdjoinRoot.root g ^ ↑ji.2

Iterating two monic AdjoinRoot constructions gives a linearly independent rectangular family of powers. This generic lemma keeps the typeclass structures fixed before the concrete Kummer polynomials are substituted.

theorem BGS.Markoff.splitTraceEtaKummerPolynomial_monic {K : Type u_1} [Field K] (sigma : K) (e : ℕ) (he : e ≠ 0) : (splitTraceEtaKummerPolynomial sigma e).Monic

theorem BGS.Markoff.splitTraceXiKummerPolynomial_monic {K : Type u_1} [Field K] (sigma : K) (e d : ℕ) (hd : d ≠ 0) : (splitTraceXiKummerPolynomial sigma e d).Monic

theorem BGS.Markoff.splitTraceEtaXiNormalMonomials_linearIndependent {K : Type u_1} [Field K] (sigma : K) (e d : ℕ) (he : e ≠ 0) (hd : d ≠ 0) : LinearIndependent (AdjoinRoot (splitTraceBaseKummerPolynomial sigma)) fun (ji : Fin (splitTraceEtaKummerPolynomial sigma e).natDegree × Fin (splitTraceXiKummerPolynomial sigma e d).natDegree) => splitTraceEtaRootInXiField sigma e d ^ ↑ji.1 * splitTraceXiRoot sigma e d ^ ↑ji.2

A bounded eta--xi normal form has unique coefficients over the base function ring. Equivalently, its linear-combination evaluation map into the Kummer top algebra is injective.

theorem BGS.Markoff.splitTraceEtaXiNormalMonomials_linearIndependent_of_oddCoprime {K : Type u_1} [Field K] (sigma : K) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (_hde : d.Coprime e) : LinearIndependent (AdjoinRoot (splitTraceBaseKummerPolynomial sigma)) fun (ji : Fin (splitTraceEtaKummerPolynomial sigma e).natDegree × Fin (splitTraceXiKummerPolynomial sigma e d).natDegree) => splitTraceEtaRootInXiField sigma e d ^ ↑ji.1 * splitTraceXiRoot sigma e d ^ ↑ji.2

In the odd-coprime situation used by the endgame, oddness supplies the required positive exponents for the bounded normal-form theorem.

theorem BGS.Markoff.splitTraceEtaXiNormalForm_evaluation_eq_zero_iff {K : Type u_1} [Field K] (sigma : K) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) (c : Fin (splitTraceEtaKummerPolynomial sigma e).natDegree × Fin (splitTraceXiKummerPolynomial sigma e d).natDegree →₀ AdjoinRoot (splitTraceBaseKummerPolynomial sigma)) : (Finsupp.linearCombination (AdjoinRoot (splitTraceBaseKummerPolynomial sigma)) fun (ji : Fin (splitTraceEtaKummerPolynomial sigma e).natDegree × Fin (splitTraceXiKummerPolynomial sigma e d).natDegree) => splitTraceEtaRootInXiField sigma e d ^ ↑ji.1 * splitTraceXiRoot sigma e d ^ ↑ji.2) c = 0 ↔ c = 0

In the odd-coprime endgame range, a reduced rectangular normal form evaluates to zero in the Kummer top algebra exactly when every coefficient is zero. This is the concrete kernel statement available before the separate existence-of-normal-form reduction for Laurent polynomials.