Label 4 no-pair dispatcher

This file is intentionally only the glue layer: it consumes the rank split from Case34NoPairSplit and delegates the two real mutation proofs to branch solvers supplied by later modules.

theorem MixPi2Lambda.exists_mutation_le_no_pair_of_rank_branches (m : ℕ) (X Y : nMixPi2Lambda (m + 2)) (hXY : ↑X < ↑Y) (_hcommon : ∀ (g : Gene), 0 < ↑↑X g → ↑↑Y g ≤ 0) (h17_1 : ∀ (k : ℕ), 0 < k → (⇑Chromosome.prime)^[k] ↑↑Y ≠ 0 → Chromosome.rank ((⇑Chromosome.prime)^[k] ↑↑X) < Chromosome.rank ((⇑Chromosome.prime)^[k] ↑↑Y)) (hXpol : (↑↑X).IsPolarized) (_hno_pair : ¬∃ (gpos : Gene) (gneg : Gene), gpos.rank = gneg.rank ∧ gpos.type = GeneType.Positive ∧ gneg.type = GeneType.Negative ∧ 0 < ↑↑X gpos ∧ 0 < ↑↑X gneg) (rank_two : ∀ (g : Gene), 0 < ↑↑X g → (∀ (g' : Gene), 0 < ↑↑X g' → g.rank ≤ g'.rank) → g.type ≠ GeneType.NonPolarized → g.rank = 2 → ∃ (Z : ↥(Variety.Mix (Variety.Pi, 2 • Variety.Lambda))), Step (↑X) Z ∧ Z ≤ ↑Y) (rank_ge_four : ∀ (g : Gene) (q : ℕ), 0 < ↑↑X g → (∀ (g' : Gene), 0 < ↑↑X g' → g.rank ≤ g'.rank) → g.type ≠ GeneType.NonPolarized → g.rank = 2 * q + 4 → (∀ h ∈ (↑↑X).support, 2 * q + 4 ≤ h.rank) → (⇑Chromosome.prime)^[1] ↑↑X ≠ 0 → (⇑Chromosome.prime)^[1] ↑↑Y ≠ 0 → Chromosome.rank ((⇑Chromosome.prime)^[1] ↑↑X) < Chromosome.rank ((⇑Chromosome.prime)^[1] ↑↑Y) → ∃ (Z : ↥(Variety.Mix (Variety.Pi, 2 • Variety.Lambda))), Step (↑X) Z ∧ Z ≤ ↑Y) : ∃ (Z : ↥(Variety.Mix (Variety.Pi, 2 • Variety.Lambda))), Step (↑X) Z ∧ Z ≤ ↑Y

Dispatcher glue for the Label 4 no-pair tree.

Once the rank-2 boundary solver and the rank-ge-four window solver are available, this lemma turns them into the no-pair conclusion without repeating the minimal-gene bookkeeping.