Fixed-point-free small-order counts on the punctured surface

Restricting both counted coordinates to nonparabolic traces removes the two-torsion correction from the torus trace count. The resulting transported punctured set satisfies

2 * |small nonparabolic points| ≤ ((bound - 1) * M) ^ 2.

noncomputable def BGS.Markoff.normalizedPuncturedMarkoffPointsWithSmallNonparabolicFirstTwoRotationOrders (p : ℕ) [Fact (Nat.Prime p)] (bound : ℕ) : Finset ↑(normalizedPuncturedSurface (ZMod p))

Normalized punctured points whose first two coordinates are both nonparabolic and have rotation order below bound.

Equations

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

@[simp]

theorem BGS.Markoff.mem_normalizedPuncturedMarkoffPointsWithSmallNonparabolicFirstTwoRotationOrders_iff {p : ℕ} [Fact (Nat.Prime p)] {bound : ℕ} {x : ↑(normalizedPuncturedSurface (ZMod p))} : x ∈ normalizedPuncturedMarkoffPointsWithSmallNonparabolicFirstTwoRotationOrders p bound ↔ rotationOrder (↑x).u1 < bound ∧ rotationOrder (↑x).u2 < bound ∧ (↑x).u1 ^ 2 ≠ 4 ∧ (↑x).u2 ^ 2 ≠ 4

theorem BGS.Markoff.normalizedPuncturedSmallNonparabolicOrderValues_subset_traceSet {p : ℕ} [Fact (Nat.Prime p)] [Invertible 3] (hpTwo : p ≠ 2) (bound : ℕ) : Finset.map { toFun := Subtype.val, inj' := ⋯ } (normalizedPuncturedMarkoffPointsWithSmallNonparabolicFirstTwoRotationOrders p bound) ⊆ normalizedMarkoffPointsWithFirstTwoCoordinatesIn (nonparabolicConcreteLowOrderTraceSet p bound)

Forgetting the puncture embeds the nonparabolic small-order set into the ambient set cut out by the fixed-point-free trace set.

noncomputable def BGS.Markoff.puncturedMarkoffPointsWithSmallNonparabolicFirstTwoRotationOrders (p : ℕ) [Fact (Nat.Prime p)] [Invertible 3] (bound : ℕ) : Finset (PuncturedMarkoffSurface (ZMod p))

Original punctured points transported from the normalized nonparabolic small-order set.

Equations

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

theorem BGS.Markoff.puncturedMarkoffPointsWithSmallNonparabolicFirstTwoRotationOrders_card_eq_normalized {p : ℕ} [Fact (Nat.Prime p)] [Invertible 3] (bound : ℕ) : (puncturedMarkoffPointsWithSmallNonparabolicFirstTwoRotationOrders p bound).card = (normalizedPuncturedMarkoffPointsWithSmallNonparabolicFirstTwoRotationOrders p bound).card

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

The fixed-point-free trace pairing on both coordinates gives a square bound with no additive parabolic correction.

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

At bound = d + 1, the low-order square has coefficient exactly d.