The real compactness lemma in the opening

The published opening rules out finite characteristic-zero orbits by first placing all three normalized trace coordinates in [-2, 2]. The elementary real inequality used at that point is proved here independently of the later cyclotomic lifting argument.

theorem BGS.Markoff.real_normalizedMarkoff_eq_origin_of_firstCoordinate_mem_Icc (x : NormalizedPoint ℝ) (hx : IsNormalizedMarkoff x) (hfirst : x.u1 ∈ Set.Icc (-2) 2) : x = normalizedOrigin

A real normalized Markoff point whose first trace coordinate lies in [-2, 2] is the origin. In particular, the published hypothesis that all three coordinates lie in this interval is more than is needed.

The proof uses 2|bc| ≤ b² + c². Since the Markoff equation makes abc equal to the nonnegative sum of three squares and |a| ≤ 2, it follows that a² ≤ 0; the remaining two squares then vanish as well.

theorem BGS.Markoff.real_normalizedMarkoff_eq_origin_of_coordinates_mem_Icc (x : NormalizedPoint ℝ) (hx : IsNormalizedMarkoff x) (hfirst : x.u1 ∈ Set.Icc (-2) 2) (_hsecond : x.u2 ∈ Set.Icc (-2) 2) (_hthird : x.u3 ∈ Set.Icc (-2) 2) : x = normalizedOrigin

Published Proposition 16's real inequality, stated with all three interval hypotheses.