Even-sign divisibility for component complements

This file specializes the free even-sign action to the finite complement used by the nonparabolic complement frontier.

theorem BGS.Markoff.four_dvd_puncturedComponentComplementFinset_card_of_evenSign_invariant (p : ℕ) [Fact (Nat.Prime p)] (hpThree : 3 < p) (c : PuncturedMarkoffSurface (ZMod p)) (hsign : ∀ (s : EvenSign) (x : PuncturedMarkoffSurface (ZMod p)), s • x ∈ puncturedComponentComplementFinset p c ↔ x ∈ puncturedComponentComplementFinset p c) : 4 ∣ (puncturedComponentComplementFinset p c).card

An even-sign-invariant component complement has cardinality divisible by four. The hypothesis is stated in the same form as the complement frontier's hsign input.