Bounding the opening orders by the full Gamma orbit

The nonzero semisimple fibers use the existing conic parametrizations. Trace zero and the two parabolic traces are handled explicitly, since the generic parametrizations deliberately exclude those values.

theorem BGS.Markoff.eigenvalueOrder_le_normalizedGammaOrbit_ncard (p : ℕ) [Fact (Nat.Prime p)] [Invertible 3] (hpTwo : p ≠ 2) (x : NormalizedMarkoffSurface (ZMod p)) (hxne : ↑x ≠ normalizedOrigin) (W : (OpeningResidueClosure p)ˣ) (htrace : (algebraMap (ZMod p) (OpeningResidueClosure p)) (↑x).u1 = splitTorusTrace W) : orderOf W ≤ (normalizedGammaOrbit x).ncard

The exact order of any residue-closure eigenvalue representing the first trace is bounded by the full normalized Gamma orbit. Nonzero semisimple traces use the conic rotation cycles; trace zero and parabolic traces use the explicit exceptional lower bounds above.

theorem BGS.Markoff.prime_le_twenty_pow_normalizedGammaOrbit_ncard_cube (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (hpThree : p ≠ 3) (x : NormalizedMarkoffSurface (ZMod p)) (hxne : ↑x ≠ normalizedOrigin) : p ≤ 20 ^ (normalizedGammaOrbit x).ncard ^ 3

The concrete opening exponent can be bounded by the cardinality of the full normalized Gamma orbit. The exclusions p ≠ 2, 3 are explicit: oddness is used by the trace classification and 3 must be invertible for the transported normalized action.

theorem BGS.Markoff.normalizedGammaOrbit_normalization_eq_image {R : Type u_1} [Field R] [Invertible 3] (x : MarkoffSurface R) : normalizedGammaOrbit ((normalizationSurfaceEquiv R) x) = ⇑(normalizationSurfaceEquiv R) '' gammaOrbit x

Normalization carries the original Gamma orbit bijectively onto the transported normalized Gamma orbit.

theorem BGS.Markoff.normalizedGammaOrbit_normalization_ncard {R : Type u_1} [Field R] [Invertible 3] (x : MarkoffSurface R) : (normalizedGammaOrbit ((normalizationSurfaceEquiv R) x)).ncard = (gammaOrbit x).ncard

Original and normalized Gamma orbits have the same cardinality.

theorem BGS.Markoff.prime_le_twenty_pow_gammaOrbit_ncard_cube (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (hpThree : p ≠ 3) (x : MarkoffSurface (ZMod p)) (hxne : ↑x ≠ origin) : p ≤ 20 ^ (gammaOrbit x).ncard ^ 3

Original-coordinate form of the orbit-card opening bound.