Maximal candidate orders in the Markoff middle game

Every ordinary candidate order divides a divisibility-maximal candidate, and the canonical roots-of-unity subgroups are monotone under that divisibility. Hence the Corvaja--Zannier union only needs maximal orders.

def BGS.Markoff.middleGameMaximalOrders (p currentOrder : ℕ) : Finset ℕ

The maximal orders below the current order used by the middle-game cover.

Equations

• BGS.Markoff.middleGameMaximalOrders p currentOrder = BGS.NumberTheory.maximalDivisorsBelow (p - 1) (currentOrder + 1) ∪ BGS.NumberTheory.maximalDivisorsBelow (p + 1) (currentOrder + 1)

theorem BGS.Markoff.middleGameMaximalOrders_card_le (p currentOrder : ℕ) : (middleGameMaximalOrders p currentOrder).card ≤ (NumberTheory.maximalDivisorsBelow (p - 1) (currentOrder + 1)).card + (NumberTheory.maximalDivisorsBelow (p + 1) (currentOrder + 1)).card

theorem BGS.Markoff.middleGameMaximalOrders_subset_candidateOrders {p currentOrder : ℕ} (hp : 1 < p) : middleGameMaximalOrders p currentOrder ⊆ middleGameCandidateOrders p currentOrder

theorem BGS.Markoff.exists_dvd_middleGameMaximalOrder {p currentOrder d : ℕ} (hp : 1 < p) (hd : d ∈ middleGameCandidateOrders p currentOrder) : ∃ m ∈ middleGameMaximalOrders p currentOrder, d ∣ m

theorem BGS.Markoff.middleGameRightSubgroup_mono (p d m : ℕ) [Fact (Nat.Prime p)] (hdm : d ∣ m) : middleGameRightSubgroup p d ≤ middleGameRightSubgroup p m

theorem BGS.Markoff.exists_middleGameMaximalOrder_trace_of_nonparabolic (p currentOrder : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (hp : 1 < p) (t : ZMod p) (hnonparabolic : t ^ 2 ≠ 4) (hsmall : rotationOrder t ≤ currentOrder) : ∃ m ∈ middleGameMaximalOrders p currentOrder, ∃ (h₂ : ↥(middleGameRightSubgroup p m)), (algebraMap (ZMod p) (quadraticFiniteField p)) t = splitTorusTrace ↑h₂

theorem BGS.Markoff.middleGameMaximalOrder_rightSubgroup_natCard (p currentOrder m : ℕ) [Fact (Nat.Prime p)] (hp : 1 < p) (hm : m ∈ middleGameMaximalOrders p currentOrder) : Nat.card ↥(middleGameRightSubgroup p m) = m