The elementary small-order point count

This module connects matrix rotation order to the concrete split/nonsplit trace set and then to the normalized fixed-fiber bound. It is the counting step omitted from the paper's final assembly; no dynamical assertion about escaping to the cage is assumed here.

noncomputable def BGS.Markoff.normalizedMarkoffPointsWithSmallFirstTwoRotationOrders (p : ℕ) [Fact (Nat.Prime p)] (bound : ℕ) : Finset (NormalizedPoint (ZMod p))

Normalized Markoff points whose first two matrix rotation orders are below bound.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BGS.Markoff.mem_normalizedMarkoffPointsWithSmallFirstTwoRotationOrders_iff {p : ℕ} [Fact (Nat.Prime p)] {bound : ℕ} {x : NormalizedPoint (ZMod p)} : x ∈ normalizedMarkoffPointsWithSmallFirstTwoRotationOrders p bound ↔ IsNormalizedMarkoff x ∧ rotationOrder x.u1 < bound ∧ rotationOrder x.u2 < bound

theorem BGS.Markoff.normalizedMarkoffPointsWithSmallFirstTwoRotationOrders_subset_traceSet {p : ℕ} [Fact (Nat.Prime p)] [Invertible 3] (hpTwo : p ≠ 2) (bound : ℕ) : normalizedMarkoffPointsWithSmallFirstTwoRotationOrders p bound ⊆ normalizedMarkoffPointsWithFirstTwoCoordinatesIn (concreteLowOrderTraceSet p bound)

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

The concrete low-order trace set, counted using the divisors of the two torus orders.

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

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

The fully connected crude count used in the giant-orbit assembly.

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

The normalized small-order point count obtained from the divisor-sensitive trace count.

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