From base sign-stability to complement divisibility

Because Gamma normalizes the even-sign subgroup, it is enough to connect the four sign changes of one base point back to that base component. Every even sign change then preserves the whole component and its finite complement.

theorem BGS.Markoff.samePuncturedComponent_evenSign_smul_iff_of_base_stable {R : Type u_1} [CommRing R] (c x : PuncturedMarkoffSurface R) (hbase : ∀ (s : EvenSign), SamePuncturedComponent c (s • c)) (s : EvenSign) : SamePuncturedComponent c (s • x) ↔ SamePuncturedComponent c x

If all even-sign changes of the base point lie in its Gamma component, then every even sign preserves membership in that component.

theorem BGS.Markoff.puncturedComponentComplementFinset_evenSign_mem_iff_of_base_stable (p : ℕ) [Fact (Nat.Prime p)] (c x : PuncturedMarkoffSurface (ZMod p)) (hbase : ∀ (s : EvenSign), SamePuncturedComponent c (s • c)) (s : EvenSign) : s • x ∈ puncturedComponentComplementFinset p c ↔ x ∈ puncturedComponentComplementFinset p c

Base sign-stability makes the finite component complement invariant under every even sign.

theorem BGS.Markoff.four_dvd_puncturedComponentComplementFinset_card_of_base_sign_stable (p : ℕ) [Fact (Nat.Prime p)] (hpThree : 3 < p) (c : PuncturedMarkoffSurface (ZMod p)) (hbase : ∀ (s : EvenSign), SamePuncturedComponent c (s • c)) : 4 ∣ (puncturedComponentComplementFinset p c).card

The expected factor four in the complement size follows from the sole geometric input that the four sign changes of the base point return to its Gamma component.