Even-sign stability of a split-cage base component

If u has full split-torus order p - 1, then -u has order at least (p - 1) / 2. Thus negating a split-maximal trace still produces a coordinate above the endgame threshold whenever

p ^ (5 / 6) ≤ (p - 1) / 2.

Every even sign change preserves or negates each normalized coordinate. Consequently, under the usual large-order-to-base hypothesis, all four even sign images of a split-cage base lie in its Gamma orbit.

@[simp]

theorem BGS.Markoff.splitTorusTrace_neg {F : Type u_1} [Field F] (u : Fˣ) : splitTorusTrace (-u) = -splitTorusTrace u

theorem BGS.Markoff.exists_fullOrder_splitUnit_of_isSplitMaximalTrace (p : ℕ) [Fact (Nat.Prime p)] (hpSeven : 7 ≤ p) (t : ZMod p) (hmax : IsSplitMaximalTrace p t) : ∃ (u : (ZMod p)ˣ), splitTorusTrace u = t ∧ orderOf u = p - 1 ∧ ↑u ^ 2 ≠ 1

A split-maximal trace is represented by a full-order split-torus unit.

theorem BGS.Markoff.half_card_sub_one_le_orderOf_neg_of_fullOrder (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (u : (ZMod p)ˣ) (huOrder : orderOf u = p - 1) : (p - 1) / 2 ≤ orderOf (-u)

Negating a full-order unit loses at most a factor of two in its order.

theorem BGS.Markoff.half_card_sub_one_le_rotationOrder_neg_splitTorusTrace (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (u : (ZMod p)ˣ) (huOrder : orderOf u = p - 1) (huSq : ↑u ^ 2 ≠ 1) : (p - 1) / 2 ≤ rotationOrder (-splitTorusTrace u)

The negated trace of a full-order split unit has rotation order at least half the split-torus cardinality.

theorem BGS.Markoff.normalizedCoordinateAt_evenSign_smul_eq_or_eq_neg {R : Type u_1} [CommRing R] [Invertible 3] (axis : NormalizedCoordinateAxis) (s : EvenSign) (x : PuncturedMarkoffSurface R) : normalizedCoordinateAt axis ↑(normalizedSurfaceOfPunctured ((puncturedNormalizationEquiv R) (s • x))) = normalizedCoordinateAt axis ↑(normalizedSurfaceOfPunctured ((puncturedNormalizationEquiv R) x)) ∨ normalizedCoordinateAt axis ↑(normalizedSurfaceOfPunctured ((puncturedNormalizationEquiv R) (s • x))) = -normalizedCoordinateAt axis ↑(normalizedSurfaceOfPunctured ((puncturedNormalizationEquiv R) x))

Normalization sends a signed point's selected coordinate either to the original normalized coordinate or to its negative.

theorem BGS.Markoff.samePuncturedComponent_evenSign_smul_of_splitCageBase (p : ℕ) [Fact (Nat.Prime p)] [Invertible 3] (hpSeven : 7 ≤ p) (c : PuncturedMarkoffSurface (ZMod p)) (hbase : IsInSplitCage p (normalizedSurfaceOfPunctured ((puncturedNormalizationEquiv (ZMod p)) c))) (hhalfThreshold : ↑p ^ (5 / 6) ≤ ↑((p - 1) / 2)) (hlarge : ∀ (z : NormalizedMarkoffSurface (ZMod p)), ↑p ^ (5 / 6) ≤ ↑(maximalCoordinateRotationOrder ↑z) → SameNormalizedComponent (normalizedSurfaceOfPunctured ((puncturedNormalizationEquiv (ZMod p)) c)) z) (s : EvenSign) : SamePuncturedComponent c (s • c)

Under the explicit half-order threshold, every even sign image of a split-cage base lies in the base Gamma component.