From a giant divisible orbit to transitivity

The published version observes that a giant orbit with complement smaller than p is the whole punctured Markoff surface if every orbit cardinality is divisible by p. This module proves that finite-orbit argument and combines it with Chen's component-divisibility theorem, using Martin's later elementary proof.

theorem BGS.Markoff.puncturedMarkoffTransitiveAt_of_small_orbitComplement_and_orbitCard_dvd (p : ℕ) [Fact (Nat.Prime p)] (x : PuncturedMarkoffSurface (ZMod p)) (hsmall : orbitComplementCard x < p) (hdiv : ∀ (y : PuncturedMarkoffSurface (ZMod p)), p ∣ (puncturedGammaOrbit y).ncard) : PuncturedMarkoffTransitiveAt p

If one orbit has complement smaller than p and every orbit cardinality is divisible by p, then the action is transitive.

theorem BGS.Markoff.exists_orbitComplementCard_lt_prime_of_hasGiantOrbitAt (p : ℕ) (hp : Nat.Prime p) (epsilon : ℝ) (hepsilon : epsilon < 1) (hgiant : HasGiantOrbitAt p epsilon) : ∃ (x : PuncturedMarkoffSurface (ZMod p)), orbitComplementCard x < p

A p^epsilon giant-orbit bound with epsilon < 1 has complement strictly smaller than p.

theorem BGS.Markoff.puncturedMarkoffTransitiveAt_of_hasGiantOrbitAt_and_orbitCard_dvd (p : ℕ) (hp : Nat.Prime p) (epsilon : ℝ) (hepsilon : epsilon < 1) (hgiant : HasGiantOrbitAt p epsilon) (hdiv : ∀ (y : PuncturedMarkoffSurface (ZMod p)), p ∣ (puncturedGammaOrbit y).ncard) : PuncturedMarkoffTransitiveAt p

The published short route from a giant orbit and orbit-cardinality divisibility to punctured finite-field transitivity at the given prime.

theorem BGS.Markoff.eventually_puncturedMarkoffTransitiveAt_of_giantOrbit_and_orbitCard_dvd (epsilon : ℝ) (hepsilon : epsilon < 1) (hgiant : ∃ (p0 : ℕ), ∀ (p : ℕ), Nat.Prime p → p0 ≤ p → HasGiantOrbitAt p epsilon) (hdiv : ∀ (p : ℕ), Nat.Prime p → 3 < p → ∀ (y : PuncturedMarkoffSurface (ZMod p)), p ∣ (puncturedGammaOrbit y).ncard) : ∃ (p0 : ℕ), ∀ (p : ℕ), Nat.Prime p → p0 ≤ p → PuncturedMarkoffTransitiveAt p

Eventual giant-orbit control with any fixed exponent below one, combined with orbit divisibility for primes larger than three, gives eventual punctured finite-field transitivity.

theorem BGS.Markoff.eventually_puncturedMarkoffTransitiveAt_of_giantOrbit (epsilon : ℝ) (hepsilon : epsilon < 1) (hgiant : ∃ (p0 : ℕ), ∀ (p : ℕ), Nat.Prime p → p0 ≤ p → HasGiantOrbitAt p epsilon) : ∃ (p0 : ℕ), ∀ (p : ℕ), Nat.Prime p → p0 ≤ p → PuncturedMarkoffTransitiveAt p

Chen's component-divisibility theorem, through Martin's elementary proof, turns any eventual giant-orbit estimate with exponent below one into eventual punctured finite-field transitivity.