Explicit endgame and cage connectivity

This file separates the finite-prime endgame wiring from its closed numerical certificates. The structural lemmas below consume the exact primitive-trace inequalities at a fixed prime; the final wrappers discharge those inequalities from explicitStrongApproximationCutoff.

theorem BGS.Markoff.exists_iterate_nonparabolicPoint_with_maximal_secondRotation_of_explicitInequalities (p : ℕ) [Fact (Nat.Prime p)] (hpFive : 5 ≤ p) (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (x : ↑(normalizedFiber1 t)) (hSplitExplicit : ∀ (orbitExponent orbitOrder : ℕ), orbitExponent * orbitOrder = p - 1 → ↑p ^ (5 / 6) ≤ ↑orbitOrder → ↑orbitExponent * ↑(p - 1).divisors.card ^ 2 * (33 * √↑p) < ↑p) (hNonsplitExplicit : ∀ (orbitExponent orbitOrder : ℕ), orbitExponent * orbitOrder = p + 1 → ↑p ^ (5 / 6) ≤ ↑orbitOrder → ↑orbitExponent * ↑(p - 1).divisors.card ^ 2 * (34 * √↑p) < ↑p) (hlarge : ↑p ^ (5 / 6) ≤ ↑(rotationOrder t)) : ∃ (n : ℕ), rotationOrder (normalizedRotate1^[n] ↑x).u2 = p - 1

The fixed-prime semisimple endgame. Its only numerical inputs are the two displayed primitive-trace inequalities, with the fixed coefficients 33 and 34 already obtained from the coefficient-8 affine Hasse--Weil bound.

theorem BGS.Markoff.exists_iterate_point_with_maximal_secondRotation_of_explicitInequalities (p : ℕ) [Fact (Nat.Prime p)] (hpFive : 5 ≤ p) (t : ZMod p) (x : ↑(normalizedFiber1 t)) (hSplitExplicit : ∀ (orbitExponent orbitOrder : ℕ), orbitExponent * orbitOrder = p - 1 → ↑p ^ (5 / 6) ≤ ↑orbitOrder → ↑orbitExponent * ↑(p - 1).divisors.card ^ 2 * (33 * √↑p) < ↑p) (hNonsplitExplicit : ∀ (orbitExponent orbitOrder : ℕ), orbitExponent * orbitOrder = p + 1 → ↑p ^ (5 / 6) ≤ ↑orbitOrder → ↑orbitExponent * ↑(p - 1).divisors.card ^ 2 * (34 * √↑p) < ↑p) (hzero : 4 < ↑p ^ (5 / 6)) (hlarge : ↑p ^ (5 / 6) ≤ ↑(rotationOrder t)) : ∃ (n : ℕ), rotationOrder (normalizedRotate1^[n] ↑x).u2 = p - 1

Fixed-prime first-coordinate endgame, including the parabolic branch and the trace-zero exclusion.

theorem BGS.Markoff.exists_splitMaximalFiberBridge_of_explicitInequality (p : ℕ) [Fact (Nat.Prime p)] (hpFive : 5 ≤ p) (hexplicit : ↑(p - 1).divisors.card ^ 2 * (100522 * √↑p) < ↑p) (axis other : NormalizedCoordinateAxis) (xi eta : ZMod p) (hxi : IsSplitMaximalTrace p xi) (heta : IsSplitMaximalTrace p eta) : ∃ (middle : NormalizedCoordinateAxis) (y : ZMod p), middle ≠ axis ∧ middle ≠ other ∧ IsSplitMaximalTrace p y ∧ NormalizedFibersMeet (normalizedFiberAt axis xi) (normalizedFiberAt middle y) ∧ NormalizedFibersMeet (normalizedFiberAt other eta) (normalizedFiberAt middle y)

The pointwise primitive cage relation converted into the fiber bridge used by cage connectivity.

theorem BGS.Markoff.splitCage_connected_of_explicitInequality (p : ℕ) [Fact (Nat.Prime p)] [Invertible 3] (hpSeven : 7 ≤ p) (hexplicit : ↑(p - 1).divisors.card ^ 2 * (100522 * √↑p) < ↑p) (x y : NormalizedMarkoffSurface (ZMod p)) (hxCage : IsInSplitCage p x) (hyCage : IsInSplitCage p y) : SameNormalizedComponent x y

Pointwise connectivity of the selected cage from its closed numerical inequality.

theorem BGS.Markoff.exists_explicit_sameComponent_maximalRotation_of_large_firstCoordinate {p : ℕ} [Fact (Nat.Prime p)] [Invertible 3] (hp : explicitStrongApproximationCutoff ≤ p) (x : NormalizedMarkoffSurface (ZMod p)) (hlarge : ↑p ^ (5 / 6) ≤ ↑(rotationOrder (↑x).u1)) : ∃ (y : NormalizedMarkoffSurface (ZMod p)), SameNormalizedComponent x y ∧ rotationOrder (↑y).u2 = p - 1

At the closed cutoff, the first-coordinate endgame reaches a maximal split rotation with no residual numerical or geometric assumptions.

theorem BGS.Markoff.exists_explicit_sameComponent_splitCage_of_large_firstCoordinate {p : ℕ} [Fact (Nat.Prime p)] [Invertible 3] (hp : explicitStrongApproximationCutoff ≤ p) (x : NormalizedMarkoffSurface (ZMod p)) (hlarge : ↑p ^ (5 / 6) ≤ ↑(rotationOrder (↑x).u1)) : ∃ (y : NormalizedMarkoffSurface (ZMod p)), SameNormalizedComponent x y ∧ IsInSplitCage p y

First-coordinate form of the explicit large-order-to-cage endgame.

theorem BGS.Markoff.exists_explicit_sameComponent_splitCage_of_some_largeCoordinate {p : ℕ} [Fact (Nat.Prime p)] [Invertible 3] (hp : explicitStrongApproximationCutoff ≤ p) (x : NormalizedMarkoffSurface (ZMod p)) (hlarge : ↑p ^ (5 / 6) ≤ ↑(rotationOrder (↑x).u1) ∨ ↑p ^ (5 / 6) ≤ ↑(rotationOrder (↑x).u2) ∨ ↑p ^ (5 / 6) ≤ ↑(rotationOrder (↑x).u3)) : ∃ (y : NormalizedMarkoffSurface (ZMod p)), SameNormalizedComponent x y ∧ IsInSplitCage p y

If one of the three coordinate rotations is explicitly large, the point reaches the selected split cage.

theorem BGS.Markoff.explicit_splitCage_connected {p : ℕ} [Fact (Nat.Prime p)] [Invertible 3] (hp : explicitStrongApproximationCutoff ≤ p) (x y : NormalizedMarkoffSurface (ZMod p)) (hx : IsInSplitCage p x) (hy : IsInSplitCage p y) : SameNormalizedComponent x y

The selected split cage is connected at the closed cutoff.

theorem BGS.Markoff.explicit_sameNormalizedComponent_of_largeOrder_to_splitCage {p : ℕ} [Fact (Nat.Prime p)] [Invertible 3] (hp : explicitStrongApproximationCutoff ≤ p) (base x : NormalizedMarkoffSurface (ZMod p)) (hbase : IsInSplitCage p base) (hlarge : ↑p ^ (5 / 6) ≤ ↑(rotationOrder (↑x).u1) ∨ ↑p ^ (5 / 6) ≤ ↑(rotationOrder (↑x).u2) ∨ ↑p ^ (5 / 6) ≤ ↑(rotationOrder (↑x).u3)) : SameNormalizedComponent base x

A large-order point is in the component of any chosen base point of the selected split cage. This is the endgame statement consumed by the maximal bad-orbit argument.