Assembly of the giant orbit

This file connects the selected split cage component to the original punctured Markoff action, bounds the complement by the already-counted small-order set, and assembles Theorem 1 first from explicit specialized estimates and then from the reusable general Hasse--Weil interface. The interface is inhabited in BGS.HasseWeil.GeneralBivariateAffineHasseWeil; the parameter-free endpoint is exported by BGS.Markoff.Assembly.Unconditional.

def BGS.Markoff.normalizedSurfaceOfPunctured {R : Type u_1} [CommRing R] (x : ↑(normalizedPuncturedSurface R)) : NormalizedMarkoffSurface R

Regard a normalized punctured point as a point of the normalized surface.

Equations

• BGS.Markoff.normalizedSurfaceOfPunctured x = ⟨↑x, ⋯⟩

def BGS.Markoff.normalizePuncturedPoint {R : Type u_1} [Field R] [Invertible 3] (x : PuncturedMarkoffSurface R) : NormalizedMarkoffSurface R

The normalized surface point underlying an original punctured point.

Equations

• BGS.Markoff.normalizePuncturedPoint x = BGS.Markoff.normalizedSurfaceOfPunctured ((BGS.Markoff.puncturedNormalizationEquiv R) x)

theorem BGS.Markoff.normalizePuncturedPoint_smul {R : Type u_1} [Field R] [Invertible 3] (g : ↥(Gamma R)) (z : PuncturedMarkoffSurface R) : normalizePuncturedPoint (g • z) = (normalizedGammaPerm R g) (normalizePuncturedPoint z)

Normalizing an original punctured point intertwines the two Gamma actions.

theorem BGS.Markoff.samePuncturedComponent_iff_sameNormalizedComponent {R : Type u_1} [Field R] [Invertible 3] (x y : PuncturedMarkoffSurface R) : SamePuncturedComponent x y ↔ SameNormalizedComponent (normalizedSurfaceOfPunctured ((puncturedNormalizationEquiv R) x)) (normalizedSurfaceOfPunctured ((puncturedNormalizationEquiv R) y))

Normalization identifies the punctured component relation with the transported component relation on normalized surface points.

theorem BGS.Markoff.exists_normalizedPunctured_splitCagePoint (p : ℕ) [Fact (Nat.Prime p)] (hpSeven : 7 ≤ p) : ∃ (x : ↑(normalizedPuncturedSurface (ZMod p))), IsInSplitCage p (normalizedSurfaceOfPunctured x)

For every sufficiently large prime, an explicit split conic point supplies a punctured base point in the selected cage.

theorem BGS.Markoff.eventually_natCeil_rpow_add_one_le_rpow {δ η : ℝ} (hδ : 0 < δ) (hδη : δ < η) : ∀ᶠ (p : ℕ) in Filter.atTop, ↑(⌈↑p ^ δ⌉₊ + 1) ≤ ↑p ^ η

A ceiling buffer over a smaller real power is eventually bounded by any strictly larger real power.

theorem BGS.Markoff.maximalCoordinateRotationOrder_le_rpow_of_not_same_splitCageComponent (p : ℕ) [Fact (Nat.Prime p)] [Invertible 3] {δ : ℝ} (c x : NormalizedMarkoffSurface (ZMod p)) (hescape : ∀ (z : NormalizedMarkoffSurface (ZMod p)), ↑p ^ δ < ↑(maximalCoordinateRotationOrder ↑z) → ∃ (y : NormalizedMarkoffSurface (ZMod p)), SameNormalizedComponent z y ∧ IsInSplitCage p y) (hconnected : ∀ (y : NormalizedMarkoffSurface (ZMod p)), IsInSplitCage p y → SameNormalizedComponent c y) (hnot : ¬SameNormalizedComponent c x) : ↑(maximalCoordinateRotationOrder ↑x) ≤ ↑p ^ δ

If every point above the middle-game cutoff reaches a connected split cage, then every point outside the chosen cage component has small maximal order.

theorem BGS.Markoff.eventually_hasGiantOrbit_of_specializedEstimates (hBound : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] [inst_1 : Fintype (quadraticFiniteField p)], WeightedTraceTorsionIntersectionBound p (quadraticFiniteField p)) (splitCoefficient : ℕ) (hSplitWeil : WeightedSplitTraceWeilBoundAssumption splitCoefficient) (nonsplitCoefficient : ℕ) (hNonsplitWeil : SeededNonsplitTraceWeilBoundAssumption nonsplitCoefficient) (cageCoefficient : ℕ) (hCageEstimate : CageWitnessPointEstimate cageCoefficient) (epsilon : ℝ) : 0 < epsilon → ∃ (p0 : ℕ), ∀ (p : ℕ), Nat.Prime p → p0 ≤ p → HasGiantOrbitAt p epsilon

Intermediate assembly relative to a neutral weighted-trace torsion-intersection bound and three specialized point-count estimates.

The public endpoint supplies the weighted-trace bound from the completed Corvaja--Zannier theorem and derives the three point-count specializations from the general affine Hasse--Weil theorem.

theorem BGS.Markoff.theoremOneStatement_of_specializedEstimates (hBound : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] [inst_1 : Fintype (quadraticFiniteField p)], WeightedTraceTorsionIntersectionBound p (quadraticFiniteField p)) (splitCoefficient : ℕ) (hSplitWeil : WeightedSplitTraceWeilBoundAssumption splitCoefficient) (nonsplitCoefficient : ℕ) (hNonsplitWeil : SeededNonsplitTraceWeilBoundAssumption nonsplitCoefficient) (cageCoefficient : ℕ) (hCageEstimate : CageWitnessPointEstimate cageCoefficient) : TheoremOneStatement

Modular bound-injection form of Theorem 1.

It exposes the neutral weighted-trace torsion-intersection contract together with the split, nonsplit, and cage point-count specializations. The public endpoint below supplies these inputs from the completed Corvaja--Zannier theorem and the remaining general affine Hasse--Weil input.

theorem BGS.Markoff.theoremOneStatement_of_generalHasseWeil_and_nonsplitHasseAdapter (hHasse : External.GeneralBivariateAffineHasseWeilTheorem) (nonsplitCoefficient : ℕ) (hNonsplitWeil : SeededNonsplitTraceWeilBoundAssumption nonsplitCoefficient) : TheoremOneStatement

The near-final Theorem 1 assembly with Corvaja--Zannier discharged by the in-repository theorem. This intermediate adapter keeps the general affine Hasse--Weil input explicit, together with its descended nonsplit adapter.

theorem BGS.Markoff.theoremOneStatement_of_generalHasseWeil (hHasse : External.GeneralBivariateAffineHasseWeilTheorem) : TheoremOneStatement

BGS Theorem 1 with Corvaja--Zannier fully discharged.

The in-repository Corvaja--Zannier theorem supplies the middle-game estimate. This theorem is the general-interface assembly step; the parameter-free public endpoint is BGS.Markoff.theoremOneStatement.