Split-cage nonparabolic complement frontier

The split-cage base supplies the only geometric input needed for the even-sign factor four: every signed image of the base point returns to its Gamma component. This module discharges both sign-invariance hypotheses of the nonparabolic complement frontier automatically.

theorem BGS.Markoff.four_dvd_puncturedComponentComplementFinset_card_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) : 4 ∣ (puncturedComponentComplementFinset p c).card

A split-cage base above the half-order threshold has a component complement whose cardinality is divisible by four.

theorem BGS.Markoff.puncturedMarkoffTransitiveAt_of_splitCage_nonparabolicComplement_pairedMaximalDivisor_frontier (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)) (hcube : ∀ (d : ℕ), 0 < d → 8 * p ≤ (d * maximalDivisorCountSum p (d + 1)) ^ 2 → (6 * maximalDivisorCountSum p (d + 1)) ^ 3 < d) (hlinear : ∀ (d : ℕ), ↑d < ↑p ^ (5 / 6) → 24 * maximalDivisorCountSum p (d + 1) * d < p) (hlarge : ∀ (z : NormalizedMarkoffSurface (ZMod p)), ↑p ^ (5 / 6) ≤ ↑(maximalCoordinateRotationOrder ↑z) → SameNormalizedComponent (normalizedSurfaceOfPunctured ((puncturedNormalizationEquiv (ZMod p)) c)) z) : PuncturedMarkoffTransitiveAt p

Nonparabolic paired-maximal-divisor frontier with the even-sign invariance and factor-four hypotheses discharged by a split-cage base.