theorem
MixPi2Lambda.exists_mutation_le_pair_positive_double_of_high_zero
{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)
(hrank : gpos.rank = gneg.rank)
(hgpos : gpos.type = GeneType.Positive)
(hgneg : gneg.type = GeneType.Negative)
(hpos : 2 ≤ ↑↑X gpos)
(hneg : ↑↑X gneg = 1)
(high_zero :
∀ (q : ℕ),
gpos.rank = 2 * q + 4 →
(⇑Chromosome.prime)^[2 * q + 5] ↑↑Y = 0 →
∃ (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
theorem
MixPi2Lambda.exists_mutation_le_pair_negative_double_of_high_zero
{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)
(hrank : gpos.rank = gneg.rank)
(hgpos : gpos.type = GeneType.Positive)
(hgneg : gneg.type = GeneType.Negative)
(hpos : ↑↑X gpos = 1)
(hneg : 2 ≤ ↑↑X gneg)
(high_zero :
∀ (q : ℕ),
gneg.rank = 2 * q + 4 →
(⇑Chromosome.prime)^[2 * q + 5] ↑↑Y = 0 →
∃ (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