Diagonalizing an arbitrary nonzero nonparabolic Markoff fiber

This module closes the algebraic interface required by the weighted middle-game order escape. Every normalized Markoff point whose fixed coordinate is nonzero and nonparabolic becomes an explicit splitFiberPoint w s after scalar extension to the canonical quadratic field.

The trace-zero fiber is excluded explicitly. Its conic is singular and the existing splitFiberEquiv / quadraticNormFiberEquiv APIs correctly require nonzero trace; no false torus parametrization is introduced for that branch.

theorem BGS.Markoff.rotationOrder_zero_le_four (p : ℕ) [Fact (Nat.Prime p)] : rotationOrder 0 ≤ 4

The singular trace-zero rotation has order at most four. This keeps the trace-zero fiber outside every middle-game range whose current order is greater than four, without pretending that its singular conic is a torus.

theorem BGS.Markoff.algebraMapNormalizedPoint_splitFiberPoint (p : ℕ) [Fact (Nat.Prime p)] (w s : (ZMod p)ˣ) : algebraMapNormalizedPoint p (splitFiberPoint w s) = splitFiberPoint ((Units.map ↑(algebraMap (ZMod p) (quadraticFiniteField p))) w) ((Units.map ↑(algebraMap (ZMod p) (quadraticFiniteField p))) s)

Scalar extension carries the explicit split fiber parametrization to the corresponding parametrization over the quadratic field.

theorem BGS.Markoff.exists_diagonalizedFiberPoint_of_nonzero_nonparabolic (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (x : NormalizedPoint (ZMod p)) (hx : IsNormalizedMarkoff x) (hnonzero : x.u1 ≠ 0) (hnonparabolic : x.u1 ^ 2 ≠ 4) : ∃ (w : (quadraticFiniteField p)ˣ) (s : (quadraticFiniteField p)ˣ), ↑w ^ 2 ≠ 1 ∧ algebraMapNormalizedPoint p x = splitFiberPoint w s

Every normalized nonzero nonparabolic fiber point admits the diagonalized scalar-extension presentation consumed by exists_iterate_with_larger_secondRotationOrder_of_diagonalizedFiber.

theorem BGS.Markoff.exists_iterate_with_larger_secondRotationOrder_of_nonzero_nonparabolic (p : ℕ) [Fact (Nat.Prime p)] [Fintype (quadraticFiniteField p)] (hpTwo : p ≠ 2) (delta : ℝ) (hdelta : delta ≤ 1 / 2) (x : NormalizedPoint (ZMod p)) (hx : IsNormalizedMarkoff x) (hnonzero : x.u1 ≠ 0) (hnonparabolic : x.u1 ^ 2 ≠ 4) (hbelowEndgame : ↑(rotationOrder x.u1) < ↑p ^ (1 / 2 + delta)) (hcube : (corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card)) ^ 3 < rotationOrder x.u1) (hlinear : corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card) * rotationOrder x.u1 < p) (hCZ : ∀ (w s : (quadraticFiniteField p)ˣ), ↑w ^ 2 ≠ 1 → algebraMapNormalizedPoint p x = splitFiberPoint w s → ↑s * (splitFiberProduct w * ↑s⁻¹) ≠ 1 → ∀ d ∈ middleGameCandidateOrders p (rotationOrder x.u1), ↑(weightedTraceEquationSolutions (↑s) (splitFiberProduct w * ↑s⁻¹) (Subgroup.zpowers w) (middleGameRightSubgroup p d)).card ≤ corvajaZannierTraceUpperBound p (rotationOrder x.u1) (Nat.card ↥(middleGameRightSubgroup p d))) : ∃ (n : ℕ), rotationOrder x.u1 < rotationOrder (normalizedRotate1^[n] x).u2

Complete nonzero nonparabolic middle-game order escape. All algebraic and combinatorial wiring is discharged internally. The only deep hypothesis is the weighted Corvaja--Zannier estimate, stated uniformly for whichever split or norm-one diagonalization the point has.