§16 Case A Branch A: the g₃ sub-case assemblies for Mix (Pi, Lambda).

This is the PL-specific m = 1, b₁ = d₁ sub-case of §16 Case 2. Here g₁ = g(1) is the minimal (odd-rank) nonpolarized gene, g₂ = g⁺(2n'+2) is the minimal gene of X - g₁, and X - g₁ - g₂ contains a negative or nonpolarized gene g₃ of minimal rank t. The mutation g₂ + g₃ → g(2n'+1) + g(t+1) (t even, type7) or g₂ + g₃ → g(2n'+1) + g⁺(t+1) (t odd, type6) gives Z ≤ Y, using the level-1-anchored a-propagation branchA_g3_aprop (odd j) and half_le_sigma_diff_at_r (even j).

theorem MixPiLambda.Ywin_below_pl {N : ℕ} (X Y : nMixPiLambda N) (hXY : ↑X < ↑Y) (gk : Gene) (hgk : 0 < ↑↑X gk) {j : ℕ} (hj : j < gk.rank) : (⇑Chromosome.prime)^[j] ↑↑Y ≠ 0

prime^[j] Y ≠ 0 for j below the rank of any gene of X (via dominance).

theorem MixPiLambda.branchA_g3_exists {N : ℕ} (X Y : nMixPiLambda N) (hXY : ↑X < ↑Y) (ha : (Sigma.sigma (↑↑X) 1).1 < (Sigma.sigma (↑↑Y) 1).1) (g₁ g₂ : Gene) (hg₁NP : g₁.type = GeneType.NonPolarized) (hg₁rank : g₁.rank = 1) (hmult1 : ↑↑X g₁ = 1) (hg₁min : ∀ g ∈ (↑↑X).support, g₁.rank ≤ g.rank) (hg₂pos : g₂.type = GeneType.Positive) : ∃ g₃ ∈ (↑↑X - Finsupp.single g₁ 1 - Finsupp.single g₂ 1).support, g₃.type ≠ GeneType.Positive

§16 g₃ existence: when g₁ = g(1) and g₂ = g⁺(2n'+2) are the two minimal genes and a₁ < c₁ (ha), the remainder X - g₁ - g₂ contains a negative or nonpolarized gene. Otherwise every non-positive gene of X is g₁ (rank 1), and the a-propagation branchA_g3_aprop forces 1 ≤ 0 at a level beyond maxRank.

theorem MixPiLambda.one_le_signature_snd_of_contains_negative_mix {X : Chromosome} {gneg : Gene} (hgneg : gneg.type = GeneType.Negative) (hXgneg : 0 < X gneg) : 1 ≤ (Chromosome.signature ((⇑Chromosome.prime)^[gneg.rank - 1] X)).2

Mirror of one_le_signature_fst_of_contains_positive_mix for the b-component: a negative gene g⁻(r) forces 1 ≤ b-signature at level r - 1.

theorem MixPiLambda.branchA_g3_Ynonzero_top {N : ℕ} (X Y : nMixPiLambda N) (hXY : ↑X < ↑Y) (hcommon : ¬∃ (g : Gene), 0 < ↑↑X g ∧ 0 < ↑↑Y g) (nn : ℕ) (g₃ : Gene) (hg₃_rank : g₃.rank = 2 * nn + 2) (hg₃_neg : g₃.type = GeneType.Negative) (hXg₃ : 0 < ↑↑X g₃) : (⇑Chromosome.prime)^[2 * nn + 2] ↑↑Y ≠ 0

§16 g₃ top boundary (type7, Mix (Pi, Lambda)). With g₃ = g⁻(2nn+2) a negative gene of X (disjoint from Y) and t = 2nn+2 even, prime^[t] Y ≠ 0: otherwise the level t-1 survivors of Y would all sit at rank 1 and, being neither g⁻(t) (disjoint) nor NP(t) (even rank), contribute 0 to the b-component, contradicting the b-bound from g₃.

theorem MixPiLambda.branchA_g3_assembly_type6 {N : ℕ} (X Y : nMixPiLambda N) (hXY : ↑X < ↑Y) (hsigeq : ¬∃ (k : ℕ), 0 < k ∧ (⇑Chromosome.prime)^[k] ↑↑Y ≠ 0 ∧ Sigma.sigma (↑↑X) k = Sigma.sigma (↑↑Y) k) (n' nn : ℕ) (hmn : n' ≤ nn) (g₂ g₃ : Gene) (hg₂_rank : g₂.rank = 2 * n' + 2) (hg₂_pos : g₂.type = GeneType.Positive) (hg₃_rank : g₃.rank = 2 * nn + 3) (hg₃_np : g₃.type = GeneType.NonPolarized) (hXg₂ : 0 < ↑↑X g₂) (hXg₃ : 0 < (↑↑X - Finsupp.single g₂ 1) g₃) (hne : g₂ ≠ g₃) (hprop_odd : ∀ (j : ℕ), 2 * n' + 1 < j → j ≤ 2 * nn + 3 → Odd j → (Sigma.sigma (↑↑X) j).1 + 1 ≤ (Sigma.sigma (↑↑Y) j).1) (hYwin : ∀ (j : ℕ), 2 * n' + 1 ≤ j → j < 2 * nn + 3 → (⇑Chromosome.prime)^[j] ↑↑Y ≠ 0) : ∃ (Z : ↥(Variety.Mix (Variety.Pi, Variety.Lambda))), Step (↑X) Z ∧ Z ≤ ↑Y

§16 g₃ assembly, t odd (type6): g₂ + g₃ → g(2n'+1) + g⁺(t+1), with g₂ = g⁺(2n'+2) and g₃ = NP(2nn+3). Odd levels absorb the (1,0) boost via the a-propagation; even levels absorb the (1/2,1/2) via half_le_sigma_diff_at_r.

theorem MixPiLambda.branchA_g3_assembly_type7 {N : ℕ} (X Y : nMixPiLambda N) (hXY : ↑X < ↑Y) (hsigeq : ¬∃ (k : ℕ), 0 < k ∧ (⇑Chromosome.prime)^[k] ↑↑Y ≠ 0 ∧ Sigma.sigma (↑↑X) k = Sigma.sigma (↑↑Y) k) (n' nn : ℕ) (hmn : n' ≤ nn) (g₂ g₃ : Gene) (hg₂_rank : g₂.rank = 2 * n' + 2) (hg₂_pos : g₂.type = GeneType.Positive) (hg₃_rank : g₃.rank = 2 * nn + 2) (hg₃_neg : g₃.type = GeneType.Negative) (hXg₂ : 0 < ↑↑X g₂) (hXg₃ : 0 < (↑↑X - Finsupp.single g₂ 1) g₃) (hne : g₂ ≠ g₃) (hprop_odd : ∀ (j : ℕ), 2 * n' + 1 < j → j ≤ 2 * nn + 1 → Odd j → (Sigma.sigma (↑↑X) j).1 + 1 ≤ (Sigma.sigma (↑↑Y) j).1) (hYwin : ∀ (j : ℕ), 2 * n' + 1 ≤ j → j ≤ 2 * nn + 2 → (⇑Chromosome.prime)^[j] ↑↑Y ≠ 0) : ∃ (Z : ↥(Variety.Mix (Variety.Pi, Variety.Lambda))), Step (↑X) Z ∧ Z ≤ ↑Y

§16 g₃ assembly, t even (type7): g₂ + g₃ → g(2n'+1) + g(t+1), with g₂ = g⁺(2n'+2) and g₃ = g⁻(2nn+2). Odd levels absorb the (1,0) via the a-propagation; even levels (including the top j = t, gated by hYwin) absorb (1/2,1/2) via half_le_sigma_diff_at_r.