Odd common-prime Kummer classes on the split trace curve

This module proves the rational-function and quadratic-base obstructions needed when an odd prime divides both covering exponents. Exact height-one-prime divisibility rules out nontrivial powers of the residual ratio (1 - sigma * X) / (1 - X), and a norm calculation upgrades this to independence of the two degree-one trace-coordinate classes modulo an odd prime.

Turning this base-field class calculation into irreducibility for noncoprime covers still requires the roots-of-unity eigencharacter descent in the first Kummer extension.

theorem BGS.Markoff.splitTraceResidualRatio_pow_ne_primePower {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (hnondegenerate : sigma ≠ 1) (q a : ℕ) (_hq : Nat.Prime q) (ha : 0 < a) (haq : a < q) (z : RatFunc K) : z ^ q ≠ ((1 - RatFunc.C sigma * RatFunc.X) / (1 - RatFunc.X)) ^ a

No nontrivial power below a prime exponent of the residual trace ratio can itself be a prime power in the rational-function field. This is the height-one-prime obstruction at sigma * X - 1; the denominator prime 1 - X is distinct precisely when sigma != 1.

theorem BGS.Markoff.RatFunc.X_mul_splitTraceRadicand_eq_residualRatio {K : Type u_1} [Field K] (sigma : K) : RatFunc.X * splitTraceRadicand sigma = (1 - RatFunc.C sigma * RatFunc.X) / (1 - RatFunc.X)

The residual ratio is exactly X * splitTraceRadicand sigma in the rational base of the trace curve.

theorem BGS.Markoff.splitTrace_X_mul_radicand_pow_ne_primePower {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (hnondegenerate : sigma ≠ 1) (q a : ℕ) (hq : Nat.Prime q) (ha : 0 < a) (haq : a < q) (z : RatFunc K) : z ^ q ≠ (RatFunc.X * splitTraceRadicand sigma) ^ a

Trace-radicand form of the odd-common-prime residual obstruction.

theorem BGS.Markoff.splitTrace_X_mul_radicand_pow_ne_primePower_of_not_dvd {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (hnondegenerate : sigma ≠ 1) (q a : ℕ) (hq : Nat.Prime q) (hqa : ¬q ∣ a) (z : RatFunc K) : z ^ q ≠ (RatFunc.X * splitTraceRadicand sigma) ^ a

Divisibility form used after taking norms: the exponent of the residual ratio need only be nonzero modulo q.

theorem BGS.Markoff.splitTraceBaseCoordinates_mixedPower_ne_oddPrimePower {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (hnondegenerate : sigma ≠ 1) (q a b : ℕ) (hq : Nat.Prime q) (hqTwo : q ≠ 2) (haq : a < q) (hbq : b < q) (hab : a ≠ 0 ∨ b ≠ 0) (z : SplitTraceBaseFunctionField K sigma) : z ^ q ≠ (splitTraceBaseU sigma * splitTraceBaseV sigma) ^ a * splitTraceBaseV sigma ^ b

Odd-prime Kummer-class independence of the two degree-one trace coordinates. The norm first forces the two character exponents to agree; the remaining diagonal character is exactly the residual rational function handled above.