The logarithmic lower-bound half of Theorem 1

The opening proves the exact inequality p ≤ 20 ^ m ^ 3 for every punctured orbit of cardinality m. This file performs the analytic conversion that the paper calls immediate and packages it with the quantifiers of EveryOrbitLargeAt and TheoremOneStatement.

theorem BGS.Markoff.subtypeVal_image_puncturedGammaOrbit {R : Type u_1} [CommRing R] (x : PuncturedMarkoffSurface R) : Subtype.val '' puncturedGammaOrbit x = gammaOrbit ↑x

Forgetting the proof that a point is nonzero maps its punctured orbit onto its orbit in the full Markoff surface.

theorem BGS.Markoff.puncturedGammaOrbit_ncard_eq_gammaOrbit_ncard {R : Type u_1} [CommRing R] (x : PuncturedMarkoffSurface R) : (puncturedGammaOrbit x).ncard = (gammaOrbit ↑x).ncard

Puncturing does not change the cardinality of a nonzero Gamma orbit.

theorem BGS.Markoff.prime_le_twenty_pow_puncturedGammaOrbit_ncard_cube (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (hpThree : p ≠ 3) (x : PuncturedMarkoffSurface (ZMod p)) : p ≤ 20 ^ (puncturedGammaOrbit x).ncard ^ 3

Punctured-orbit form of the exact opening inequality.

theorem BGS.Markoff.one_third_mul_log_rpow_le_of_prime_le_twenty_pow_cube (p orbitCard : ℕ) (hp : Nat.Prime p) (hbound : p ≤ 20 ^ orbitCard ^ 3) : 1 / 3 * (Real.log ↑p).rpow (1 / 3) ≤ ↑orbitCard

The exact exponential opening bound implies a uniform cube-root logarithmic lower bound. The deliberately coarse constant 1 / 3 avoids introducing an artificial transcendental constant into Theorem 1.

theorem BGS.Markoff.everyOrbitLargeAt_one_third (p : ℕ) (hp : Nat.Prime p) (hpFive : 5 ≤ p) : EveryOrbitLargeAt p (1 / 3)

Every punctured orbit over every prime p ≥ 5 satisfies the lower bound in Theorem 1 with the absolute constant 1 / 3.

theorem BGS.Markoff.theoremOne_everyOrbitLarge : ∃ (c : ℝ), 0 < c ∧ ∃ (p0 : ℕ), ∀ (p : ℕ), Nat.Prime p → p0 ≤ p → EveryOrbitLargeAt p c

The second conjunct of TheoremOneStatement, including its absolute constant and threshold, is completely formalized.

theorem BGS.Markoff.theoremOneStatement_of_eventually_hasGiantOrbit (hgiant : ∀ (epsilon : ℝ), 0 < epsilon → ∃ (p0 : ℕ), ∀ (p : ℕ), Nat.Prime p → p0 ≤ p → HasGiantOrbitAt p epsilon) : TheoremOneStatement

With the every-orbit lower bound now proved, TheoremOneStatement is reduced exactly to its giant-orbit conjunct.