The elementary asymptotic in the giant-orbit assembly

The concrete small-order count is 2 * (2 + 2 * B^2)^2. This file proves that choosing B ≤ p^(ε/5) makes that count at most p^ε for all sufficiently large p. No dynamical claim about the cage complement is used here.

theorem BGS.Markoff.smallOrderPointBound_le_rpow {p bound : ℕ} {ε : ℝ} (hThirtyTwo : 32 ≤ ↑p ^ (ε / 5)) (hbound : ↑bound ≤ ↑p ^ (ε / 5)) : ↑(2 * (2 + 2 * bound ^ 2) ^ 2) ≤ ↑p ^ ε

Once p^(ε/5) absorbs the fixed constant, the explicit polynomial bound is at most p^ε.

theorem BGS.Markoff.eventually_smallOrderPointBound_le_rpow {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (p : ℕ) in Filter.atTop, ∀ (bound : ℕ), ↑bound ≤ ↑p ^ (ε / 5) → ↑(2 * (2 + 2 * bound ^ 2) ^ 2) ≤ ↑p ^ ε

The explicit polynomial small-order bound is eventually absorbed by the target real power.

theorem BGS.Markoff.puncturedSmallOrderSet_card_le_rpow_of_bound {p : ℕ} [Fact (Nat.Prime p)] [Invertible 3] (hpTwo : p ≠ 2) {ε : ℝ} (bound : ℕ) (hThirtyTwo : 32 ≤ ↑p ^ (ε / 5)) (hbound : ↑bound ≤ ↑p ^ (ε / 5)) : ↑(puncturedMarkoffPointsWithSmallFirstTwoRotationOrders p bound).card ≤ ↑p ^ ε

The counted punctured small-order set satisfies the target bound as soon as its order cutoff is at most p^(ε/5) and the harmless constant has been absorbed.