Nonparabolic complement frontier

Instead of maximizing the rotation order on one bad orbit, this route maximizes it on the entire complement of a fixed punctured component. That complement is Vieta-invariant, so its cardinality is divisible by p. Assuming the expected even-sign divisibility by four, every nonempty complement therefore has at least 4 * p points.

The parabolic endgame bridge puts the whole complement in the fixed-point-free small-order set. Consequently its maximal order d forces

8 * p ≤ (d * M) ^ 2,

with no additive parabolic correction.

noncomputable def BGS.Markoff.puncturedComponentComplementFinset (p : ℕ) [Fact (Nat.Prime p)] (c : PuncturedMarkoffSurface (ZMod p)) : Finset (PuncturedMarkoffSurface (ZMod p))

The finite complement of the punctured component of c.

Equations

• BGS.Markoff.puncturedComponentComplementFinset p c = {x : BGS.Markoff.PuncturedMarkoffSurface (ZMod p) | ¬BGS.Markoff.SamePuncturedComponent c x}

@[simp]

theorem BGS.Markoff.mem_puncturedComponentComplementFinset_iff {p : ℕ} [Fact (Nat.Prime p)] {c x : PuncturedMarkoffSurface (ZMod p)} : x ∈ puncturedComponentComplementFinset p c ↔ ¬SamePuncturedComponent c x

theorem BGS.Markoff.puncturedComponentComplementFinset_vieta1_mem_iff {p : ℕ} [Fact (Nat.Prime p)] (c x : PuncturedMarkoffSurface (ZMod p)) : (vieta1PuncturedPerm (ZMod p)) x ∈ puncturedComponentComplementFinset p c ↔ x ∈ puncturedComponentComplementFinset p c

theorem BGS.Markoff.puncturedComponentComplementFinset_vieta2_mem_iff {p : ℕ} [Fact (Nat.Prime p)] (c x : PuncturedMarkoffSurface (ZMod p)) : (vieta2PuncturedPerm (ZMod p)) x ∈ puncturedComponentComplementFinset p c ↔ x ∈ puncturedComponentComplementFinset p c

theorem BGS.Markoff.puncturedComponentComplementFinset_vieta3_mem_iff {p : ℕ} [Fact (Nat.Prime p)] (c x : PuncturedMarkoffSurface (ZMod p)) : (vieta3PuncturedPerm (ZMod p)) x ∈ puncturedComponentComplementFinset p c ↔ x ∈ puncturedComponentComplementFinset p c

theorem BGS.Markoff.prime_dvd_puncturedComponentComplementFinset_card (p : ℕ) [Fact (Nat.Prime p)] (hpThree : 3 < p) (c : PuncturedMarkoffSurface (ZMod p)) : p ∣ (puncturedComponentComplementFinset p c).card

The complement of one component is itself Vieta-invariant, hence its cardinality is divisible by the characteristic prime.

theorem BGS.Markoff.four_mul_prime_le_puncturedComponentComplementFinset_card (p : ℕ) [Fact (Nat.Prime p)] (hpThree : 3 < p) (c : PuncturedMarkoffSurface (ZMod p)) (hnonempty : (puncturedComponentComplementFinset p c).Nonempty) (hfour : 4 ∣ (puncturedComponentComplementFinset p c).card) : 4 * p ≤ (puncturedComponentComplementFinset p c).card

Combining Vieta p-divisibility with a supplied even-sign four-divisibility gives the exact 4 * p lower bound for a nonempty component complement.

theorem BGS.Markoff.puncturedMarkoffTransitiveAt_of_nonparabolicComplement_pairedMaximalDivisor_frontier (p : ℕ) [Fact (Nat.Prime p)] [Invertible 3] (hpThree : 3 < p) (c : PuncturedMarkoffSurface (ZMod p)) (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) (hsign : ∀ (s : EvenSign) (x : PuncturedMarkoffSurface (ZMod p)), s • x ∈ puncturedComponentComplementFinset p c ↔ x ∈ puncturedComponentComplementFinset p c) (hfour : 4 ∣ (puncturedComponentComplementFinset p c).card) : PuncturedMarkoffTransitiveAt p

Complement-maximal paired frontier with the fixed-point-free low-order count. The even-sign action is kept explicit: hsign records invariance of the component complement, while hfour supplies the remaining free-action cardinality consequence.