theorem
Mix2LambdaPi.type14_rank_one_target_add_rest_le_of_gaps
{N q : ℕ}
{ε : GeneType}
(hε : ε ≠ GeneType.NonPolarized)
(X Y : nMix2LambdaPi N)
(hXY : ↑X < ↑Y)
(restval : Chromosome)
(hXeq : ↑(X14 ⋯ hε) + restval = ↑↑X)
(hgap_odd :
∀ (j : ℕ),
1 ≤ j →
j ≤ 2 * q + 3 →
¬Even j →
(1, 1) + Chromosome.signature ((⇑Chromosome.prime)^[j] ↑↑X) ≤ Chromosome.signature ((⇑Chromosome.prime)^[j] ↑↑Y))
(hgap_even :
∀ (j : ℕ),
1 ≤ j →
j ≤ 2 * q + 3 →
Even j →
Chromosome.signature (Gene.ofRank 1 ε) + Chromosome.signature (Gene.ofRank 1 ε) + Chromosome.signature ((⇑Chromosome.prime)^[j] ↑↑X) ≤ Chromosome.signature ((⇑Chromosome.prime)^[j] ↑↑Y))
:
Dominance assembly for the rank-one lower endpoint of type14,
2g^ε(1)+2g^{-ε}(2q+3) → 2g(0)+2g(2q+4).
The target-source signature delta is only parity-dependent in the middle
window: odd levels need (1,1) slack, while even levels need two copies of the
rank-one ε signature.
theorem
Mix2LambdaPi.exists_mutation_le_type14_of_decomp
{N m n : ℕ}
{ε : GeneType}
(hε : ε ≠ GeneType.NonPolarized)
(h_le : m ≤ n)
(X Y : nMix2LambdaPi N)
(restval : Chromosome)
(hXeq : ↑(X14 h_le hε) + restval = ↑↑X)
(hrest : restval ∈ Variety.Mix (2 • Variety.Lambda, Variety.Pi))
(hZle : ↑(Y14 h_le hε) + restval ≤ ↑↑Y)
:
∃ (Z : ↥(Variety.Mix (2 • Variety.Lambda, Variety.Pi))), Step (↑X) Z ∧ Z ≤ ↑Y
A thin theorem-level wrapper for general type14. The caller supplies the source decomposition and the dominance bound after replacing the source by the type14 target.
theorem
Mix2LambdaPi.exists_mutation_le_type14_of_genes
{N m n : ℕ}
{ε : GeneType}
(hε : ε ≠ GeneType.NonPolarized)
(h_le : m ≤ n)
(X Y : nMix2LambdaPi N)
(gdouble gopp : Gene)
(hdouble_type : gdouble.type = ε)
(hopp_type : gopp.type = -ε)
(hdouble_rank : gdouble.rank = 2 * m + 1)
(hopp_rank : gopp.rank = 2 * n + 1)
(hdouble : 2 ≤ ↑↑X gdouble)
(hopp : 2 ≤ ↑↑X gopp)
(hne : gdouble ≠ gopp)
(hZle :
↑(Y14 h_le hε) + (↑↑X - Finsupp.single gdouble 1 - Finsupp.single gdouble 1 - Finsupp.single gopp 1 - Finsupp.single gopp 1) ≤ ↑↑Y)
:
∃ (Z : ↥(Variety.Mix (2 • Variety.Lambda, Variety.Pi))), Step (↑X) Z ∧ Z ≤ ↑Y
Concrete-gene wrapper for general type14. This packages the source
decomposition 2g^ε(2m+1)+2g^{-ε}(2n+1)+rest and the rest membership; the
caller still supplies the final dominance bound for the type14 target plus the
rest. The rank-one boundary used in §17 Case 3 is the specialization m = 0.