The seeded nonsplit endgame cover

The endgame curve is not the trace of a bare norm-one element. A fixed seed s in a nontrivial norm fibre is multiplied by the varying norm-one coordinate. After scalar extension the two weights are s and s^p; their product is Norm(s), not one.

noncomputable def BGS.Markoff.seededBaseUnitInQuadraticField (p : ℕ) [Fact (Nat.Prime p)] (u : (ZMod p)ˣ) : (quadraticFiniteField p)ˣ

A split base-field unit transported to the canonical quadratic extension.

Equations

• BGS.Markoff.seededBaseUnitInQuadraticField p u = (Units.map ↑(algebraMap (ZMod p) (BGS.Markoff.quadraticFiniteField p))) u

def BGS.Markoff.SeededNonsplitTraceCoverEquation (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (s : ↑(quadraticNormFiber p k)) (d e : ℕ) (w : ↥(quadraticNormOneTorus p)) (u : (ZMod p)ˣ) : Prop

The actual seeded nonsplit cover. The seed lies in the norm-k torsor and the varying coordinate lies in the norm-one torus.

Equations

• BGS.Markoff.SeededNonsplitTraceCoverEquation p k s d e w u = ((Algebra.trace (ZMod p) (BGS.Markoff.quadraticFiniteField p)) (↑↑s * ↑↑(w ^ d)) = BGS.Markoff.splitTorusTrace (u ^ e))

theorem BGS.Markoff.algebraMap_seededQuadraticTrace_eq_weightedSplitTorusTrace (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (s : ↑(quadraticNormFiber p k)) (d : ℕ) (w : ↥(quadraticNormOneTorus p)) : (algebraMap (ZMod p) (quadraticFiniteField p)) ((Algebra.trace (ZMod p) (quadraticFiniteField p)) (↑↑s * ↑↑(w ^ d))) = weightedSplitTorusTrace (↑↑s) (↑↑s ^ p) (↑w ^ d)

The scalar extension of the seeded trace is the weighted trace with coefficients alpha = s and beta = s^p.

theorem BGS.Markoff.seededNonsplitTraceCoverEquation_iff_weightedSplitTraceCover (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (s : ↑(quadraticNormFiber p k)) (d e : ℕ) (w : ↥(quadraticNormOneTorus p)) (u : (ZMod p)ˣ) : SeededNonsplitTraceCoverEquation p k s d e w u ↔ SplitTraceCurveEquation (↑↑s) (↑↑s ^ p) e d (seededBaseUnitInQuadraticField p u) ↑w

The actual nonsplit cover is exactly the existing weighted split cover over the quadratic field. The exponent order in SplitTraceCurveEquation is (e,d).

theorem BGS.Markoff.seededNonsplitWeights_mul (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (s : ↑(quadraticNormFiber p k)) : ↑↑s * ↑↑s ^ p = (algebraMap (ZMod p) (quadraticFiniteField p)) ↑k

The product of the scalar-extended weights is exactly the prescribed seed norm.

theorem BGS.Markoff.seededNonsplitWeights_nondegenerate (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (hk : k ≠ 1) (s : ↑(quadraticNormFiber p k)) : ↑↑s ≠ 0 ∧ ↑↑s ^ p ≠ 0 ∧ ↑↑s * ↑↑s ^ p ≠ 1

A seed of norm different from one supplies exactly the coefficient hypotheses required by the weighted split-cover irreducibility theorem.

theorem BGS.Markoff.quadraticFiberProduct_ne_one_of_prime_ne_two (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (t : ZMod p) (ht : t ^ 2 ≠ 4) : quadraticFiberProduct p t ≠ 1

For an odd prime, the existing nonzero nonparabolic conic invariant kappa(t) = t^2/(t^2-4) is not one.

theorem BGS.Markoff.quadraticFiberProductUnit_ne_one (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) : quadraticFiberProductUnit p t ht ht0 ≠ 1

The unit indexing the existing conic norm fibre is nontrivial.

theorem BGS.Markoff.existingConicSeed_nonsplitWeights_nondegenerate (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (s : ↑(quadraticConicNormFiber p t ht ht0)) : ↑↑s ≠ 0 ∧ ↑↑s ^ p ≠ 0 ∧ ↑↑s * ↑↑s ^ p ≠ 1

Every seed from the existing nonsplit conic construction has nonzero weighted coefficients whose product is the embedded invariant kappa(t), and this product is not one.

theorem BGS.Markoff.existingConicSeed_weightedCover_absolutelyIrreducible (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (s : ↑(quadraticConicNormFiber p t ht ht0)) (d e : ℕ) (hd : 0 < d) (he : 0 < e) (hdChar : ↑d ≠ 0) : Irreducible ((MvPolynomial.map (algebraMap (quadraticFiniteField p) (AlgebraicClosure (quadraticFiniteField p)))) (splitTraceCoverPolynomial (↑↑s) (↑↑s ^ p) e d))

The corrected nonsplit cover lands in the already-proved arbitrary positive-exponent weighted-cover theorem after quadratic scalar extension. In the polynomial convention the base-field exponent e is the first exponent and the norm-one exponent d is the second, so the characteristic hypothesis is required on d.

def BGS.Markoff.ExistingConicSeedNonsplitTraceCoverEquation (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (s : ↑(quadraticConicNormFiber p t ht ht0)) (d e : ℕ) (w : ↥(quadraticNormOneTorus p)) (u : (ZMod p)ˣ) : Prop

The endgame equation specialized to the seed type already constructed by the conic parametrization module.

Equations

• BGS.Markoff.ExistingConicSeedNonsplitTraceCoverEquation p t ht ht0 s d e w u = BGS.Markoff.SeededNonsplitTraceCoverEquation p (BGS.Markoff.quadraticFiberProductUnit p t ht ht0) s d e w u

theorem BGS.Markoff.existingConicSeedNonsplitTraceCoverEquation_iff_weightedSplitTraceCover (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (s : ↑(quadraticConicNormFiber p t ht ht0)) (d e : ℕ) (w : ↥(quadraticNormOneTorus p)) (u : (ZMod p)ˣ) : ExistingConicSeedNonsplitTraceCoverEquation p t ht ht0 s d e w u ↔ SplitTraceCurveEquation (↑↑s) (↑↑s ^ p) e d (seededBaseUnitInQuadraticField p u) ↑w

def BGS.Markoff.DegenerateUnseededCountermodel.UnseededNormOneTraceCountermodel (p : ℕ) [Fact (Nat.Prime p)] (d e : ℕ) (w : ↥(quadraticNormOneTorus p)) (u : (ZMod p)ˣ) : Prop

This is the tempting but incorrect unseeded model. It is retained only to state the degeneracy explicitly.

Equations

• BGS.Markoff.DegenerateUnseededCountermodel.UnseededNormOneTraceCountermodel p d e w u = (BGS.Markoff.quadraticNormOneTrace p (w ^ d) = BGS.Markoff.splitTorusTrace (u ^ e))

theorem BGS.Markoff.DegenerateUnseededCountermodel.unseededCountermodel_weights_product_eq_one (p : ℕ) [Fact (Nat.Prime p)] : 1 * 1 = 1