Periodic points on semisimple fibers

This module proves the point-level implication needed in the opening. It does not infer finite matrix order from periodicity of a single vector. Instead it uses the explicit conic parametrization: on a nonparabolic fiber, rotation multiplies the eigen-coordinate by a chosen matrix eigenvalue, so a positive return forces that eigenvalue to be torsion.

theorem BGS.Markoff.exists_splitTorusTrace_eq {K : Type u_1} [Field K] [IsAlgClosed K] (t : K) : ∃ (w : Kˣ), t = splitTorusTrace w

Every trace parameter over an algebraically closed field is w + w⁻¹ for a nonzero eigenvalue w.

theorem BGS.Markoff.periodic_nonparabolic_fiber_has_torsion_eigenvalue {K : Type u_1} [Field K] [IsAlgClosed K] {t : K} (ht : t ^ 2 ≠ 4) {x : NormalizedPoint K} (hx : x ∈ normalizedFiber1 t) {n : ℕ} (hn : 0 < n) (hperiodic : normalizedRotate1^[n] x = x) : ∃ (w : Kˣ), IsOfFinOrder w ∧ t = splitTorusTrace w

A positive return of a point on a nonparabolic normalized fiber produces a torsion eigenvalue representing the fixed trace coordinate.