Small-order Markoff counts using maximal divisors

This is the counting half of the paper's maximal-divisor improvement, formalized at the finite-set boundary used by the maximal-orbit argument.

def BGS.Markoff.maximalDivisorCountSum (p bound : ℕ) : ℕ

The combined number of maximal divisors below the bound for the two torus orders.

Equations

• BGS.Markoff.maximalDivisorCountSum p bound = (BGS.NumberTheory.maximalDivisorsBelow (p - 1) bound).card + (BGS.NumberTheory.maximalDivisorsBelow (p + 1) bound).card

theorem BGS.Markoff.concreteLowOrderTraceSet_card_le_maximalDivisors {p : ℕ} [Fact (Nat.Prime p)] (bound : ℕ) : (concreteLowOrderTraceSet p bound).card ≤ 2 + (bound - 1) * maximalDivisorCountSum p bound

theorem BGS.Markoff.concreteLowOrderTraceSet_succ_card_le_maximalDivisors {p : ℕ} [Fact (Nat.Prime p)] (d : ℕ) : (concreteLowOrderTraceSet p (d + 1)).card ≤ 2 + d * maximalDivisorCountSum p (d + 1)

theorem BGS.Markoff.normalizedMarkoffPointsWithSmallFirstTwoRotationOrders_card_le_maximalDivisors {p : ℕ} [Fact (Nat.Prime p)] [Invertible 3] (hpTwo : p ≠ 2) (bound : ℕ) : (normalizedMarkoffPointsWithSmallFirstTwoRotationOrders p bound).card ≤ 2 * (2 + (bound - 1) * maximalDivisorCountSum p bound) ^ 2

theorem BGS.Markoff.puncturedMarkoffPointsWithSmallFirstTwoRotationOrders_succ_card_le_maximalDivisors {p : ℕ} [Fact (Nat.Prime p)] [Invertible 3] (hpTwo : p ≠ 2) (d : ℕ) : (puncturedMarkoffPointsWithSmallFirstTwoRotationOrders p (d + 1)).card ≤ 2 * (2 + d * maximalDivisorCountSum p (d + 1)) ^ 2