theorem mutation_type3_ne {ε : GeneType} {m n : ℕ} (h_le : m ≤ n) (hm : 1 ≤ m) : Gene.ofRankAlt m ε + Gene.ofRankAlt n (-ε) ≠ Gene.ofRankAlt (m - 1) (-ε) + Gene.ofRankAlt (n + 1) ε

theorem mutation_type3_iterate_signature_eq {ε : GeneType} {m n : ℕ} (hε : ε ≠ GeneType.NonPolarized) (h_le : m ≤ n) (hm : 1 ≤ m) (i k : ℕ) (hi : i ≤ k) : Chromosome.signature ((⇑Chromosome.prime)^[i] (Gene.ofRankAlt (m + k) ((↑k).negOnePow • ε) + Gene.ofRankAlt (n + k) ((↑k).negOnePow • -ε))) = Chromosome.signature ((⇑Chromosome.prime)^[i] (Gene.ofRankAlt (m + k - 1) ((↑k).negOnePow • -ε) + Gene.ofRankAlt (n + k + 1) ((↑k).negOnePow • ε)))

theorem mutation_type3_signature_eq {ε : GeneType} {m n : ℕ} (hε : ε ≠ GeneType.NonPolarized) (h_le : m ≤ n) (hm : 1 ≤ m) : Chromosome.signature (Gene.ofRankAlt m ε + Gene.ofRankAlt n (-ε)) = Chromosome.signature (Gene.ofRankAlt (m - 1) (-ε) + Gene.ofRankAlt (n + 1) ε)

theorem mutation_type3_le {ε : GeneType} {m n : ℕ} (hε : ε ≠ GeneType.NonPolarized) (h_le : m ≤ n) (hm : 1 ≤ m) : Gene.ofRankAlt m ε + Gene.ofRankAlt n (-ε) ≤ Gene.ofRankAlt (m - 1) (-ε) + Gene.ofRankAlt (n + 1) ε

noncomputable def Pi.X3 {ε : GeneType} {m n : ℕ} (hε : ε ≠ GeneType.NonPolarized) (hle : m ≤ n) (hm : 1 ≤ m) : ↥Variety.Pi

Equations

• Pi.X3 hε hle hm = ⟨Gene.ofRankAlt m ε + Gene.ofRankAlt n (-ε), ⋯⟩

theorem Pi.X3_eq {ε : GeneType} {m n : ℕ} (hε : ε ≠ GeneType.NonPolarized) (hle : m ≤ n) (hm : 1 ≤ m) : ↑(X3 hε hle hm) = Gene.ofRankAlt m ε + Gene.ofRankAlt n (-ε)

@[simp]

theorem Pi.neg_X3 {ε : GeneType} {m n : ℕ} (hε : ε ≠ GeneType.NonPolarized) (hle : m ≤ n) (hm : 1 ≤ m) : -X3 hε hle hm = X3 ⋯ hle hm

noncomputable def Pi.Y3 {ε : GeneType} {m n : ℕ} (hε : ε ≠ GeneType.NonPolarized) (hle : m ≤ n) (hm : 1 ≤ m) : ↥Variety.Pi

Equations

• Pi.Y3 hε hle hm = ⟨Gene.ofRankAlt (m - 1) (-ε) + Gene.ofRankAlt (n + 1) ε, ⋯⟩

theorem Pi.Y3_eq {ε : GeneType} {m n : ℕ} (hε : ε ≠ GeneType.NonPolarized) (hle : m ≤ n) (hm : 1 ≤ m) : ↑(Y3 hε hle hm) = Gene.ofRankAlt (m - 1) (-ε) + Gene.ofRankAlt (n + 1) ε

@[simp]

theorem Pi.neg_Y3 {ε : GeneType} {m n : ℕ} (hε : ε ≠ GeneType.NonPolarized) (hle : m ≤ n) (hm : 1 ≤ m) : -Y3 hε hle hm = Y3 ⋯ hle hm