Fixed-point-free low-order traces on the two rotation tori

The nonparabolic low-order trace set omits the global parabolic set and uses only eigenvalues whose square is not one. Inversion is therefore fixed-point-free on both the split and norm-one sources, giving

2 * |nonparabolic low traces| ≤ (bound - 1) * M.

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

Nonparabolic bounded-order traces represented in either the split torus or the quadratic norm-one torus.

Equations

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

theorem BGS.Markoff.mem_nonparabolicConcreteLowOrderTraceSet_of_rotationOrder_lt {p : ℕ} [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (t : ZMod p) (bound : ℕ) (hnonparabolic : t ^ 2 ≠ 4) (hsmall : rotationOrder t < bound) : t ∈ nonparabolicConcreteLowOrderTraceSet p bound

Every nonparabolic trace of small rotation order lies in the fixed-point-free concrete trace set.

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

The exact fixed-point-free maximal-divisor trace count.

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

At bound = d + 1, the fixed-point-free trace estimate has the exact coefficient d.