From residue traces to the concrete cyclotomic opening bound

This file chooses eigenvalues for arbitrary normalized traces over ZMod p, including the two parabolic traces, and combines their exact orders by an lcm.

theorem BGS.Markoff.exists_residueClosure_eigenvalue_of_trace (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (t : ZMod p) : ∃ (W : (OpeningResidueClosure p)ˣ), (algebraMap (ZMod p) (OpeningResidueClosure p)) t = splitTorusTrace W ∧ IsOfFinOrder W ∧ p.Coprime (orderOf W)

Every normalized trace over an odd prime field has a finite-order eigenvalue in the fixed residue closure. Parabolic traces are represented explicitly by 1 or -1; all other traces use the split/norm-one classification.

theorem BGS.Markoff.exists_exact_eigenvalue_orders_with_cyclotomic_bound (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (x : NormalizedPoint (ZMod p)) (hx : IsNormalizedMarkoff x) (hxne : x ≠ normalizedOrigin) : ∃ (W₁ : (OpeningResidueClosure p)ˣ) (W₂ : (OpeningResidueClosure p)ˣ) (W₃ : (OpeningResidueClosure p)ˣ), (algebraMap (ZMod p) (OpeningResidueClosure p)) x.u1 = splitTorusTrace W₁ ∧ (algebraMap (ZMod p) (OpeningResidueClosure p)) x.u2 = splitTorusTrace W₂ ∧ (algebraMap (ZMod p) (OpeningResidueClosure p)) x.u3 = splitTorusTrace W₃ ∧ IsOfFinOrder W₁ ∧ IsOfFinOrder W₂ ∧ IsOfFinOrder W₃ ∧ p.Coprime (orderOf W₁) ∧ p.Coprime (orderOf W₂) ∧ p.Coprime (orderOf W₃) ∧ p ≤ 20 ^ max (orderOf W₁) (max (orderOf W₂) (orderOf W₃)) ^ 3

Every nonorigin normalized Markoff point over an odd prime field admits three compatible residue-closure eigenvalues. Their exact orders control the concrete cyclotomic opening bound.