theorem
MixPi2Lambda.exists_mutation_le_pair_rank_two_positive_double_zero_successor
{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)
(gpos gneg : Gene)
(hgpos : gpos.type = GeneType.Positive)
(hgneg : gneg.type = GeneType.Negative)
(hgpos2 : gpos.rank = 2)
(hgneg2 : gneg.rank = 2)
(hpos : 2 ≤ ↑↑X gpos)
(hneg : ↑↑X gneg = 1)
(hY3 : (⇑Chromosome.prime)^[3] ↑↑Y = 0)
:
∃ (Z : ↥(Variety.Mix (Variety.Pi, 2 • Variety.Lambda))), Step (↑X) Z ∧ Z ≤ ↑Y
theorem
MixPi2Lambda.exists_mutation_le_pair_rank_two_negative_double_zero_successor
{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)
(gpos gneg : Gene)
(hgpos : gpos.type = GeneType.Positive)
(hgneg : gneg.type = GeneType.Negative)
(hgpos2 : gpos.rank = 2)
(hgneg2 : gneg.rank = 2)
(hpos : ↑↑X gpos = 1)
(hneg : 2 ≤ ↑↑X gneg)
(hY3 : (⇑Chromosome.prime)^[3] ↑↑Y = 0)
:
∃ (Z : ↥(Variety.Mix (Variety.Pi, 2 • Variety.Lambda))), Step (↑X) Z ∧ Z ≤ ↑Y