Irreducibility of the odd coprime split trace cover

The key source-side argument is a residue decomposition. Every polynomial in x,y is written uniquely as a sum of terms

x^r * y^s * q_{r,s}(x^d, y^e), with r < d and s < e.

Evaluation in the Kummer tower sends the coefficient polynomial q_{r,s} to the degree-one base trace curve at (u*v,v). Irreducibility of that already-proved degree-one curve therefore forces each q_{r,s} to be divisible by the base cover equation. Power substitution then shows that the original polynomial is divisible by the (d,e) cover equation. This proves the source-division theorem without assuming the target irreducibility or either comparison-map injectivity statement.

noncomputable def BGS.Markoff.finTwoExponent (i j : ℕ) : Fin 2 →₀ ℕ

A two-variable exponent with the displayed exponents in coordinates 0,1.

Equations

• BGS.Markoff.finTwoExponent i j = Finsupp.single 0 i + Finsupp.single 1 j

theorem BGS.Markoff.monomial_finTwoExponent {K : Type u_1} [Field K] (i j : ℕ) (c : K) : (MvPolynomial.monomial (finTwoExponent i j)) c = MvPolynomial.C c * MvPolynomial.X 0 ^ i * MvPolynomial.X 1 ^ j

theorem BGS.Markoff.finTwoExponent_of_finsupp (ex : Fin 2 →₀ ℕ) : finTwoExponent (ex 0) (ex 1) = ex

noncomputable def BGS.Markoff.splitTracePowerSubstitution {K : Type u_1} [Field K] (e d : ℕ) : MvPolynomial (Fin 2) K →ₐ[K] MvPolynomial (Fin 2) K

Substitute x^d,y^e for the two variables.

Equations

• BGS.Markoff.splitTracePowerSubstitution e d = MvPolynomial.aeval ![MvPolynomial.X 0 ^ d, MvPolynomial.X 1 ^ e]

@[simp]

theorem BGS.Markoff.splitTracePowerSubstitution_X_zero {K : Type u_1} [Field K] (e d : ℕ) : (splitTracePowerSubstitution e d) (MvPolynomial.X 0) = MvPolynomial.X 0 ^ d

@[simp]

theorem BGS.Markoff.splitTracePowerSubstitution_X_one {K : Type u_1} [Field K] (e d : ℕ) : (splitTracePowerSubstitution e d) (MvPolynomial.X 1) = MvPolynomial.X 1 ^ e

theorem BGS.Markoff.splitTracePowerSubstitution_C {K : Type u_1} [Field K] (e d : ℕ) (c : K) : (splitTracePowerSubstitution e d) (MvPolynomial.C c) = MvPolynomial.C c

noncomputable def BGS.Markoff.splitTracePolynomialResidueBlocks {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (p : MvPolynomial (Fin 2) K) : Fin (splitTraceEtaKummerPolynomial sigma e).natDegree × Fin (splitTraceXiKummerPolynomial sigma e d).natDegree →₀ MvPolynomial (Fin 2) K

The polynomial coefficient in one residue block. A monomial x^i y^j contributes X^(i/d) Y^(j/e) to block (j mod e, i mod d).

Equations

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

@[simp]

theorem BGS.Markoff.splitTracePolynomialResidueBlocks_zero {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) : splitTracePolynomialResidueBlocks sigma hsigma e d heOdd hdOdd 0 = 0

theorem BGS.Markoff.splitTracePolynomialResidueBlocks_add {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (p q : MvPolynomial (Fin 2) K) : splitTracePolynomialResidueBlocks sigma hsigma e d heOdd hdOdd (p + q) = splitTracePolynomialResidueBlocks sigma hsigma e d heOdd hdOdd p + splitTracePolynomialResidueBlocks sigma hsigma e d heOdd hdOdd q

@[simp]

theorem BGS.Markoff.splitTracePolynomialResidueBlocks_monomial {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (ex : Fin 2 →₀ ℕ) (c : K) : splitTracePolynomialResidueBlocks sigma hsigma e d heOdd hdOdd ((MvPolynomial.monomial ex) c) = Finsupp.single (splitTraceMonomialNormalIndex sigma hsigma e d heOdd hdOdd (ex 0) (ex 1)) ((MvPolynomial.monomial (finTwoExponent (ex 0 / d) (ex 1 / e))) c)

noncomputable def BGS.Markoff.splitTraceRecomposeResidueBlocks {K : Type u_1} [Field K] (sigma : K) (e d : ℕ) (q : Fin (splitTraceEtaKummerPolynomial sigma e).natDegree × Fin (splitTraceXiKummerPolynomial sigma e d).natDegree →₀ MvPolynomial (Fin 2) K) : MvPolynomial (Fin 2) K

Reassemble residue blocks after power substitution.

Equations

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

theorem BGS.Markoff.splitTracePowerSubstitution_monomial {K : Type u_1} [Field K] (e d i j : ℕ) (c : K) : (splitTracePowerSubstitution e d) ((MvPolynomial.monomial (finTwoExponent i j)) c) = MvPolynomial.C c * MvPolynomial.X 0 ^ (d * i) * MvPolynomial.X 1 ^ (e * j)

theorem BGS.Markoff.splitTraceRecomposeResidueBlocks_single_monomial {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (i j : ℕ) (c : K) : splitTraceRecomposeResidueBlocks sigma e d (Finsupp.single (splitTraceMonomialNormalIndex sigma hsigma e d heOdd hdOdd i j) ((MvPolynomial.monomial (finTwoExponent (i / d) (j / e))) c)) = (MvPolynomial.monomial (finTwoExponent i j)) c

theorem BGS.Markoff.splitTraceRecomposeResidueBlocks_add {K : Type u_1} [Field K] (sigma : K) (e d : ℕ) (q r : Fin (splitTraceEtaKummerPolynomial sigma e).natDegree × Fin (splitTraceXiKummerPolynomial sigma e d).natDegree →₀ MvPolynomial (Fin 2) K) : splitTraceRecomposeResidueBlocks sigma e d (q + r) = splitTraceRecomposeResidueBlocks sigma e d q + splitTraceRecomposeResidueBlocks sigma e d r

theorem BGS.Markoff.splitTraceRecomposeResidueBlocks_polynomial {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (p : MvPolynomial (Fin 2) K) : splitTraceRecomposeResidueBlocks sigma e d (splitTracePolynomialResidueBlocks sigma hsigma e d heOdd hdOdd p) = p

Exact reconstruction from the residue blocks.

noncomputable def BGS.Markoff.splitTraceBaseResidueEvaluation {K : Type u_1} [Field K] (sigma : K) : MvPolynomial (Fin 2) K →ₐ[K] SplitTraceBaseFunctionField K sigma

Evaluate a residue-block polynomial on the degree-one base cover coordinates (u*v,v).

Equations

• BGS.Markoff.splitTraceBaseResidueEvaluation sigma = MvPolynomial.aeval ![BGS.Markoff.splitTraceBaseU sigma * BGS.Markoff.splitTraceBaseV sigma, BGS.Markoff.splitTraceBaseV sigma]

theorem BGS.Markoff.splitTraceBaseResidueEvaluation_monomial {K : Type u_1} [Field K] (sigma : K) (a b : ℕ) (c : K) : (splitTraceBaseResidueEvaluation sigma) ((MvPolynomial.monomial (finTwoExponent a b)) c) = (algebraMap K (SplitTraceBaseFunctionField K sigma)) c * splitTraceBaseU sigma ^ a * splitTraceBaseV sigma ^ (a + b)

theorem BGS.Markoff.splitTraceBaseResidueEvaluation_residueBlock {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (p : MvPolynomial (Fin 2) K) (ji : Fin (splitTraceEtaKummerPolynomial sigma e).natDegree × Fin (splitTraceXiKummerPolynomial sigma e d).natDegree) : (splitTraceBaseResidueEvaluation sigma) ((splitTracePolynomialResidueBlocks sigma hsigma e d heOdd hdOdd p) ji) = (splitTracePolynomialSyntacticNormalForm sigma hsigma e d heOdd hdOdd p) ji

Each syntactic Kummer coefficient is exactly the degree-one base-curve evaluation of the corresponding residue-block polynomial.

theorem BGS.Markoff.splitTracePolynomialToKummerTop_one_one_eq_baseResidueEvaluation {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (q : MvPolynomial (Fin 2) K) : (splitTracePolynomialToKummerTop sigma hsigma 1 1 splitTracePolynomialToKummerTop_one_one_eq_baseResidueEvaluation._proof_1 splitTracePolynomialToKummerTop_one_one_eq_baseResidueEvaluation._proof_1 splitTracePolynomialToKummerTop_one_one_eq_baseResidueEvaluation._proof_2) q = (IsScalarTower.toAlgHom K (SplitTraceBaseFunctionField K sigma) (SplitTraceXiFunctionField K sigma 1 1)) ((splitTraceBaseResidueEvaluation sigma) q)

For the degree-one tower, evaluation at the two Kummer roots is just base-curve evaluation at (u*v,v), followed by the canonical inclusion of the base function field.

theorem BGS.Markoff.splitTraceBaseResiduePolynomial_mem_baseCover {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (hnondegenerate : sigma ≠ 1) (q : MvPolynomial (Fin 2) K) (hq : (splitTraceBaseResidueEvaluation sigma) q = 0) : q ∈ Ideal.span {splitTraceCoverPolynomial 1 sigma 1 1}

The independently proved irreducibility of the degree-one trace curve gives the exact kernel of base residue evaluation.

theorem BGS.Markoff.splitTracePowerSubstitution_baseCover {K : Type u_1} [Field K] (sigma : K) (e d : ℕ) : (splitTracePowerSubstitution e d) (splitTraceCoverPolynomial 1 sigma 1 1) = splitTraceCoverPolynomial 1 sigma d e

Power substitution carries the degree-one base equation to the exact (d,e) cover equation.

theorem BGS.Markoff.splitTraceResidueBlockTerm_mem_coverIdeal {K : Type u_1} [Field K] (sigma : K) (e d : ℕ) (hsigma : sigma ≠ 0) (hnondegenerate : sigma ≠ 1) (ji : Fin (splitTraceEtaKummerPolynomial sigma e).natDegree × Fin (splitTraceXiKummerPolynomial sigma e d).natDegree) (q : MvPolynomial (Fin 2) K) (hq : (splitTraceBaseResidueEvaluation sigma) q = 0) : MvPolynomial.X 0 ^ ↑ji.2 * MvPolynomial.X 1 ^ ↑ji.1 * (splitTracePowerSubstitution e d) q ∈ Ideal.span {splitTraceCoverPolynomial 1 sigma d e}

Every residue-block term whose coefficient vanishes on the degree-one base curve is already in the principal ideal of the full power-cover equation.

theorem BGS.Markoff.splitTracePolynomialSyntacticNormalForm_division_of_oddCoprime {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hnondegenerate : sigma ≠ 1) (p : MvPolynomial (Fin 2) K) (hnormal : splitTracePolynomialSyntacticNormalForm sigma hsigma e d heOdd hdOdd p = 0) : p ∈ Ideal.span {splitTraceCoverPolynomial 1 sigma d e}

The missing source-division theorem for the nondegenerate odd-coprime cover. Its proof is entirely bottom-up: residue decomposition, the independently proved degree-one kernel, and exact power substitution.

theorem BGS.Markoff.splitTraceLaurentToKummerTop_injective_of_oddCoprime {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (hnondegenerate : sigma ≠ 1) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) : Function.Injective ⇑(splitTraceLaurentToKummerTop sigma hsigma e d heOdd hdOdd hde)

The explicit Laurent comparison is injective in the nondegenerate odd-coprime range; no irreducibility premise remains.

theorem BGS.Markoff.splitTraceAffineToKummerTop_injective_of_oddCoprime {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (hnondegenerate : sigma ≠ 1) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) : Function.Injective ⇑(splitTraceAffineToKummerTop sigma hsigma e d heOdd hdOdd hde)

The affine comparison is injective in the same range because the coordinate-product localization has already been proved faithful.

theorem BGS.Markoff.splitTraceCoverPolynomial_irreducible_of_oddCoprime {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (hnondegenerate : sigma ≠ 1) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) : Irreducible (splitTraceCoverPolynomial 1 sigma d e)

The normalized split trace-cover polynomial is irreducible for nondegenerate odd coprime exponents. No characteristic restriction is needed.