Nonparabolic witnesses in maximal right-order subgroups

The maximal-divisor cover already represents every bounded nonparabolic trace inside a divisibility-maximal right subgroup. This module records the extra fact needed for inversion pairing: the representing eigenvalue is not fixed by inversion.

theorem BGS.Markoff.splitTorusTrace_sq_eq_four_of_sq_eq_one {K : Type u_1} [Field K] (h : Kˣ) (hsq : h ^ 2 = 1) : splitTorusTrace h ^ 2 = 4

A square-one eigenvalue has parabolic split trace.

theorem BGS.Markoff.exists_middleGameMaximalOrder_nonparabolic_trace (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₂ ∧ ↑h₂ ^ 2 ≠ 1

Every bounded nonparabolic trace is represented in a maximal candidate right subgroup by a non-two-torsion eigenvalue.