theorem Mix2LambdaPi.mutation_type9_ne {ε : GeneType} {k : ℕ} : Gene.ofRank (2 * k + 2) GeneType.NonPolarized + Gene.ofRank (2 * k + 2) GeneType.NonPolarized ≠ Gene.ofRank (2 * k + 1) ε + Gene.ofRank (2 * k + 3) (-ε)

theorem Mix2LambdaPi.mutation_type9_iterate_signature_eq {ε : GeneType} {k : ℕ} (i j : ℕ) (hi : i ≤ j) : Chromosome.signature ((⇑Chromosome.prime)^[i] (Gene.ofRank (2 * k + 2 + j) GeneType.NonPolarized + Gene.ofRank (2 * k + 2 + j) GeneType.NonPolarized)) = Chromosome.signature ((⇑Chromosome.prime)^[i] (Gene.ofRank (2 * k + 1 + j) ε + Gene.ofRank (2 * k + 3 + j) (-ε)))

theorem Mix2LambdaPi.mutation_type9_signature_eq {ε : GeneType} {k : ℕ} : Chromosome.signature (Gene.ofRank (2 * k + 2) GeneType.NonPolarized + Gene.ofRank (2 * k + 2) GeneType.NonPolarized) = Chromosome.signature (Gene.ofRank (2 * k + 1) ε + Gene.ofRank (2 * k + 3) (-ε))

theorem Mix2LambdaPi.mutation_type9_le {ε : GeneType} {k : ℕ} : Gene.ofRank (2 * k + 2) GeneType.NonPolarized + Gene.ofRank (2 * k + 2) GeneType.NonPolarized ≤ Gene.ofRank (2 * k + 1) ε + Gene.ofRank (2 * k + 3) (-ε)

noncomputable def Mix2LambdaPi.X9 (k : ℕ) : ↥(Variety.Mix (2 • Variety.Lambda, Variety.Pi))

Equations

• Mix2LambdaPi.X9 k = ⟨Gene.ofRank (2 * k + 2) GeneType.NonPolarized + Gene.ofRank (2 * k + 2) GeneType.NonPolarized, ⋯⟩

theorem Mix2LambdaPi.X9_eq (k : ℕ) : ↑(X9 k) = Gene.ofRank (2 * k + 2) GeneType.NonPolarized + Gene.ofRank (2 * k + 2) GeneType.NonPolarized

@[simp]

theorem Mix2LambdaPi.neg_X9 (k : ℕ) : -X9 k = X9 k

noncomputable def Mix2LambdaPi.Y9 {ε : GeneType} (k : ℕ) (hε : ε ≠ GeneType.NonPolarized) : ↥(Variety.Mix (2 • Variety.Lambda, Variety.Pi))

Equations

• Mix2LambdaPi.Y9 k hε = ⟨Gene.ofRank (2 * k + 1) ε + Gene.ofRank (2 * k + 3) (-ε), ⋯⟩

theorem Mix2LambdaPi.Y9_eq {ε : GeneType} (k : ℕ) (hε : ε ≠ GeneType.NonPolarized) : ↑(Y9 k hε) = Gene.ofRank (2 * k + 1) ε + Gene.ofRank (2 * k + 3) (-ε)

@[simp]

theorem Mix2LambdaPi.neg_Y9 {ε : GeneType} (k : ℕ) (hε : ε ≠ GeneType.NonPolarized) : -Y9 k hε = Y9 k ⋯