Torsion eigenvalue traces force the complex Markoff origin

This is the characteristic-zero contradiction at the heart of the opening. Once each coordinate of a complex normalized Markoff point is represented by a torsion eigenvalue and its reciprocal, the unit-circle defect argument forces all three coordinates to vanish.

theorem BGS.Markoff.norm_coe_eq_one_of_isOfFinOrder (w : ℂˣ) (hw : IsOfFinOrder w) : ‖↑w‖ = 1

A finite-order complex unit has norm one.

theorem BGS.Markoff.complex_normalizedMarkoff_eq_origin_of_torsion_traces (x : NormalizedPoint ℂ) (hx : IsNormalizedMarkoff x) (h₁ : ∃ (w₁ : ℂˣ), IsOfFinOrder w₁ ∧ x.u1 = splitTorusTrace w₁) (h₂ : ∃ (w₂ : ℂˣ), IsOfFinOrder w₂ ∧ x.u2 = splitTorusTrace w₂) (h₃ : ∃ (w₃ : ℂˣ), IsOfFinOrder w₃ ∧ x.u3 = splitTorusTrace w₃) : x = normalizedOrigin

A complex normalized Markoff point whose three coordinates are reciprocal traces of torsion eigenvalues is the origin.