theorem MixPi2Lambda.type11_target_add_rest_le_of_diagonal_gap {N m n : ℕ} {ε : GeneType} (hε : ε ≠ GeneType.NonPolarized) (h_le : m ≤ n) (X Y : nMixPi2Lambda N) (hXY : ↑X < ↑Y) (restval : Chromosome) (hXeq : ↑(X11 h_le hε) + restval = ↑↑X) (hgap_pred : Chromosome.signature (Gene.ofRank 1 (-ε)) + Chromosome.signature ((⇑Chromosome.prime)^[2 * m + 1] ↑↑X) ≤ Chromosome.signature ((⇑Chromosome.prime)^[2 * m + 1] ↑↑Y)) (hgap_mid : ∀ (j : ℕ), 2 * m + 1 < j → j ≤ 2 * n + 2 → (1, 1) + Chromosome.signature ((⇑Chromosome.prime)^[j] ↑↑X) ≤ Chromosome.signature ((⇑Chromosome.prime)^[j] ↑↑Y)) : ↑(Y11 h_le hε) + restval ≤ ↑↑Y

Dominance for a type11 target plus an arbitrary rest term, assuming the source decomposition and the diagonal slack through the active type11 window.

theorem MixPi2Lambda.exists_mutation_le_type11_of_decomp {N m n : ℕ} {ε : GeneType} (hε : ε ≠ GeneType.NonPolarized) (h_le : m ≤ n) (X Y : nMixPi2Lambda N) (restval : Chromosome) (hXeq : ↑(X11 h_le hε) + restval = ↑↑X) (hrest : restval ∈ Variety.Mix (Variety.Pi, 2 • Variety.Lambda)) (hZle : ↑(Y11 h_le hε) + restval ≤ ↑↑Y) : ∃ (Z : ↥(Variety.Mix (Variety.Pi, 2 • Variety.Lambda))), Step (↑X) Z ∧ Z ≤ ↑Y

A thin theorem-level wrapper for type11. The caller supplies the concrete source decomposition and the dominance bound after replacing the source by the type11 target.

theorem MixPi2Lambda.exists_mutation_le_type11_of_genes {N m n : ℕ} {ε : GeneType} (hε : ε ≠ GeneType.NonPolarized) (h_le : m ≤ n) (X Y : nMixPi2Lambda N) (gε gpos gneg : Gene) (hgε : gε.type = ε) (hgpos : gpos.type = GeneType.Positive) (hgneg : gneg.type = GeneType.Negative) (hgε_rank : gε.rank = 2 * m + 2) (hgpos_rank : gpos.rank = 2 * n + 2) (hrank : gpos.rank = gneg.rank) (hεcopy : 1 ≤ ↑↑X gε) (hpos : 1 ≤ ↑↑X gpos) (hneg : 1 ≤ ↑↑X gneg) (hne_ε_pos : gε ≠ gpos) (hne_ε_neg : gε ≠ gneg) (hne_pos_neg : gpos ≠ gneg) (hZle : ↑(Y11 h_le hε) + (↑↑X - Finsupp.single gε 1 - Finsupp.single gpos 1 - Finsupp.single gneg 1) ≤ ↑↑Y) : ∃ (Z : ↥(Variety.Mix (Variety.Pi, 2 • Variety.Lambda))), Step (↑X) Z ∧ Z ≤ ↑Y

Concrete-gene wrapper for type11. This packages the source decomposition and rest membership; the caller still supplies the final dominance bound for the type11 target plus the rest.

theorem MixPi2Lambda.exists_mutation_le_type11_of_genes_with_diagonal_gap {N m n : ℕ} {ε : GeneType} (hε : ε ≠ GeneType.NonPolarized) (h_le : m ≤ n) (X Y : nMixPi2Lambda N) (hXY : ↑X < ↑Y) (gε gpos gneg : Gene) (hgε : gε.type = ε) (hgpos : gpos.type = GeneType.Positive) (hgneg : gneg.type = GeneType.Negative) (hgε_rank : gε.rank = 2 * m + 2) (hgpos_rank : gpos.rank = 2 * n + 2) (hrank : gpos.rank = gneg.rank) (hεcopy : 1 ≤ ↑↑X gε) (hpos : 1 ≤ ↑↑X gpos) (hneg : 1 ≤ ↑↑X gneg) (hne_ε_pos : gε ≠ gpos) (hne_ε_neg : gε ≠ gneg) (hne_pos_neg : gpos ≠ gneg) (hgap_pred : Chromosome.signature (Gene.ofRank 1 (-ε)) + Chromosome.signature ((⇑Chromosome.prime)^[2 * m + 1] ↑↑X) ≤ Chromosome.signature ((⇑Chromosome.prime)^[2 * m + 1] ↑↑Y)) (hgap_mid : ∀ (j : ℕ), 2 * m + 1 < j → j ≤ 2 * n + 2 → (1, 1) + Chromosome.signature ((⇑Chromosome.prime)^[j] ↑↑X) ≤ Chromosome.signature ((⇑Chromosome.prime)^[j] ↑↑Y)) : ∃ (Z : ↥(Variety.Mix (Variety.Pi, 2 • Variety.Lambda))), Step (↑X) Z ∧ Z ≤ ↑Y

Concrete-gene wrapper for type11 with the standard diagonal-gap profile. The caller supplies the diagonal slack only through the active type11 window; outside that window the source and target have identical iterated signatures.