Wiring the middle-game trace escape to Markoff moves

The orbit of a split fiber point with parameter s is parametrized by the coset s * Subgroup.zpowers w. Its second coordinate is therefore a scaled twisted trace, not the unscaled subgroup trace used in MiddleGameCorvajaZannierStep. The first two theorems make this discrepancy explicit.

For the distinguished parameter s = 1, the scaling disappears. The final theorem wires the existing Corvaja--Zannier escape theorem all the way to a point in the same rotation orbit whose second coordinate has strictly larger rotation order. Its remaining htraceCoverage hypothesis states the separate split/nonsplit classification interface that must be constructed for the chosen family of right subgroups.

theorem BGS.Markoff.splitFiberOrbit_secondCoordinate_eq_scaledTwistedTrace {E : Type u_1} [Field E] (w s h : Eˣ) : (splitFiberPoint w (s * h)).u2 = ↑s * twistedUnitTrace (splitFiberProduct w / ↑s ^ 2) h

The exact second-coordinate formula on a translated split rotation orbit. The factor s and the replacement of splitFiberProduct w by splitFiberProduct w / s^2 are indispensable.

theorem BGS.Markoff.splitFiberOrbit_secondCoordinate_eq_weightedSplitTorusTrace {E : Type u_1} [Field E] (w s h : Eˣ) : (splitFiberPoint w (s * h)).u2 = weightedSplitTorusTrace (↑s) (splitFiberProduct w * ↑s⁻¹) h

Source-faithful weighted form of the orbit-coordinate identity. Here alpha = s, beta = splitFiberProduct w / s, and hence alpha * beta is the invariant splitFiberProduct w. This is the correct subgroup equation for an arbitrary starting point; it avoids incorrectly replacing a coset by a subgroup.

theorem BGS.Markoff.splitFiberOrbit_weights_mul {E : Type u_1} [Field E] (w s : Eˣ) : ↑s * (splitFiberProduct w * ↑s⁻¹) = splitFiberProduct w

The product of the two weights in the preceding identity is exactly the fiber invariant. Thus the paper's nondegeneracy condition is alpha * beta != 1.

theorem BGS.Markoff.exists_iterate_splitFiberPoint_eq_mul_zpowers {E : Type u_1} [Field E] [Finite E] (w s : Eˣ) (h : ↥(Subgroup.zpowers w)) : ∃ (n : ℕ), normalizedRotate1^[n] (splitFiberPoint w s) = splitFiberPoint w (s * ↑h)

Every translated parameter s * h with h in the cyclic subgroup generated by w is an actual forward iterate of the normalized Markoff rotation through splitFiberPoint w s.

theorem BGS.Markoff.splitFiberBaseOrbit_secondCoordinate_eq_twistedUnitTrace {E : Type u_1} [Field E] (w : Eˣ) (h : ↥(Subgroup.zpowers w)) : (splitFiberPoint w ↑h).u2 = twistedUnitTrace (splitFiberProduct w) ↑h

At the base parameter 1, the orbit-coordinate formula is exactly the unscaled trace equation used by the Corvaja--Zannier counting module.

theorem BGS.Markoff.algebraMap_quadraticNormFiberOrbit_secondCoordinate_eq_scaledTwistedTrace (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) (s : ↑(quadraticConicNormFiber p t ht ht0)) (h : ↥(quadraticNormOneTorus p)) : (algebraMap (ZMod p) (quadraticFiniteField p)) (quadraticNormFiberPoint p t ht ht0 w (quadraticNormFiberMulNormOne p (quadraticFiberProductUnit p t ht ht0) s h)).u2 = ↑↑s * twistedUnitTrace (splitFiberProduct ↑w / ↑↑s ^ 2) ↑h

The nonsplit conic parametrization has the same translated-coset obstruction after scalar extension to the quadratic field. This is the exact formula that an eventual coset form of the Corvaja--Zannier estimate must consume.

theorem BGS.Markoff.exists_splitFiberBaseOrbitPoint_with_larger_secondRotationOrder {E : Type u_1} [Field E] [Fintype E] (p : ℕ) (w : Eˣ) (rightSubgroup : ℕ → Subgroup Eˣ) (hrightOrder : ∀ d ∈ middleGameCandidateOrders p (Nat.card ↥(Subgroup.zpowers w)), Nat.card ↥(rightSubgroup d) = d) (hCZ : splitFiberProduct w ≠ 1 → ∀ d ∈ middleGameCandidateOrders p (Nat.card ↥(Subgroup.zpowers w)), ↑(traceEquationSolutions (splitFiberProduct w) (Subgroup.zpowers w) (rightSubgroup d)).card ≤ corvajaZannierTraceUpperBound p (Nat.card ↥(Subgroup.zpowers w)) (Nat.card ↥(rightSubgroup d))) (hsigma : splitFiberProduct w ≠ 1) (hcurrentOrder : 0 < Nat.card ↥(Subgroup.zpowers w)) (hcube : (corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card)) ^ 3 < Nat.card ↥(Subgroup.zpowers w)) (hlinear : corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card) * Nat.card ↥(Subgroup.zpowers w) < p) (htraceCoverage : ∀ (t : E), rotationOrder t ≤ Nat.card ↥(Subgroup.zpowers w) → ∃ d ∈ middleGameCandidateOrders p (Nat.card ↥(Subgroup.zpowers w)), ∃ (h₂ : ↥(rightSubgroup d)), t = twistedUnitTrace 1 ↑h₂) : ∃ (h : ↥(Subgroup.zpowers w)), Nat.card ↥(Subgroup.zpowers w) < rotationOrder (splitFiberPoint w ↑h).u2 ∧ ∃ (n : ℕ), normalizedRotate1^[n] (splitFiberPoint w 1) = splitFiberPoint w ↑h

The Corvaja--Zannier escape, specialized to the cyclic subgroup generated by the current split eigenvalue, produces an actual Markoff rotation iterate whose second-coordinate order is strictly larger.

htraceCoverage is not the deep Corvaja--Zannier bound. It is the still-missing concrete classification assertion that every trace of order at most the current order is represented in the chosen indexed right subgroup. Keeping it explicit prevents the split and norm-one torus cases from being conflated.