theorem
Mix2LambdaPi.exists_mutation_le_type9
{N : ℕ}
(X Y : nMix2LambdaPi N)
(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))
(p : ℕ)
(g : Gene)
(hgNP : g.type = GeneType.NonPolarized)
(hgrank : g.rank = 2 * p + 2)
(hXg2 : 2 ≤ ↑↑X g)
:
∃ (Z : ↥(Variety.Mix (2 • Variety.Lambda, Variety.Pi))), Step (↑X) Z ∧ Z ≤ ↑Y
The first reduction in §17 for Label 3: replace a double nonpolarized gene by the type9 target.
theorem
Mix2LambdaPi.exists_mutation_le_of_nonpolarized
{N : ℕ}
(X Y : nMix2LambdaPi N)
(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))
(g : Gene)
(hXg : 0 < ↑↑X g)
(hgNP : g.type = GeneType.NonPolarized)
:
∃ (Z : ↥(Variety.Mix (2 • Variety.Lambda, Variety.Pi))), Step (↑X) Z ∧ Z ≤ ↑Y