The split trace Kummer tower for arbitrary positive exponents

This module combines cyclic eigencharacter descent with the trace curve's explicit Kummer-class calculations. It handles primes common to both covering exponents, proving that the second radicand remains non-power after adjoining an arbitrary positive root of the first coordinate. Consequently the second Kummer polynomial is irreducible without a coprimality assumption, under the explicit roots-of-unity hypotheses used by the descent.

theorem BGS.Markoff.splitTraceXiRadicand_not_primePower_of_commonPrime {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (hnondegenerate : sigma ≠ 1) (i : K) (hi : i ^ 2 = -1) (e : ℕ) (he : 0 < e) (zeta : K) (hzeta : IsPrimitiveRoot zeta e) (q : ℕ) (hq : Nat.Prime q) (hqe : q ∣ e) (z : SplitTraceEtaFunctionField K sigma e) : z ^ q ≠ splitTraceXiRadicand sigma e

The second trace radicand is not a common-prime power after adjoining an arbitrary positive e-th root of the first coordinate.

theorem BGS.Markoff.splitTraceXiKummerPolynomial_irreducible_of_primitiveRoot {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (hnondegenerate : sigma ≠ 1) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (zeta : K) (hzeta : IsPrimitiveRoot zeta e) : Irreducible (splitTraceXiKummerPolynomial sigma e d)

With a primitive e-th root in the constant field, the xi Kummer polynomial is irreducible for arbitrary positive exponents; coprimality is no longer required.

theorem BGS.Markoff.generalSplitTraceKummerTower_cover_maps_to_zero_of_primitiveRoot {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (hnondegenerate : sigma ≠ 1) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (zeta : K) (hzeta : IsPrimitiveRoot zeta e) : (generalSplitTracePolynomialToKummerTop sigma e d) (splitTraceCoverPolynomial 1 sigma d e) = 0

The roots of the arbitrary positive-exponent Kummer tower satisfy the cleared affine cover equation.

theorem BGS.Markoff.splitTraceCoverPolynomial_irreducible_of_primitiveRoot {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (hnondegenerate : sigma ≠ 1) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (zeta : K) (hzeta : IsPrimitiveRoot zeta e) : Irreducible (splitTraceCoverPolynomial 1 sigma d e)

The normalized split trace-cover polynomial is irreducible for arbitrary positive exponents over a field containing a square root of -1 and a primitive e-th root of unity.