Nondegeneracy of the actual middle-game trace-curve coefficients

The geometric Corvaja--Zannier theorem needs more than a formal weighted equation. This module proves that the two weights coming from every nonzero nonparabolic Markoff fiber are nonzero and that their product is not one. These are the exact coefficient hypotheses used by the subsequent absolute-irreducibility and non-subtorus proofs.

theorem BGS.Markoff.weightedTraceCurve_isCorvajaZannierAdmissible_of_nondegenerateWeights {K : Type u_1} [Field K] (alpha beta : K) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) (hnondegenerate : alpha * beta ≠ 1) : WeightedTraceCurveIsCorvajaZannierAdmissible alpha beta

The explicit nonzero and nondegeneracy conditions imply every geometric Corvaja--Zannier admissibility condition for the weighted trace curve.

theorem BGS.Markoff.splitFiberOrbit_weightedTraceCoefficients_nondegenerate {E : Type u_1} [Field E] (w s : Eˣ) (hw : ↑w ^ 2 ≠ 1) (htrace : splitTorusTrace w ≠ 0) (hfour : 4 ≠ 0) : ↑s ≠ 0 ∧ splitFiberProduct w * ↑s⁻¹ ≠ 0 ∧ ↑s * (splitFiberProduct w * ↑s⁻¹) ≠ 1

The two weighted trace coefficients attached to a nonzero split-fiber trace are both nonzero, and their product is the nondegenerate fiber invariant.

theorem BGS.Markoff.four_ne_zero_quadraticFiniteField_of_prime_ne_two (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) : 4 ≠ 0

Four remains nonzero in the canonical quadratic extension of an odd prime field.

theorem BGS.Markoff.diagonalizedFiber_weightedTraceCoefficients_nondegenerate (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (x : NormalizedPoint (ZMod p)) (hnonzero : x.u1 ≠ 0) (w s : (quadraticFiniteField p)ˣ) (hw : ↑w ^ 2 ≠ 1) (hpoint : algebraMapNormalizedPoint p x = splitFiberPoint w s) : ↑s ≠ 0 ∧ splitFiberProduct w * ↑s⁻¹ ≠ 0 ∧ ↑s * (splitFiberProduct w * ↑s⁻¹) ≠ 1

Concrete nondegeneracy for every diagonalized presentation of a nonzero nonparabolic normalized Markoff fiber.

theorem BGS.Markoff.diagonalizedFiber_weightedTraceCurve_isCorvajaZannierAdmissible (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (x : NormalizedPoint (ZMod p)) (hnonzero : x.u1 ≠ 0) (w s : (quadraticFiniteField p)ˣ) (hw : ↑w ^ 2 ≠ 1) (hpoint : algebraMapNormalizedPoint p x = splitFiberPoint w s) : WeightedTraceCurveIsCorvajaZannierAdmissible (↑s) (splitFiberProduct w * ↑s⁻¹)

Every actual diagonalized nonzero nonparabolic Markoff fiber supplies a Corvaja--Zannier-admissible weighted trace curve; this is no longer an independent geometric premise of the order-escape theorem.