§16 Case A Branch A: Case 2 bottom-chain + boundary for Mix (Pi, Lambda). #
Parity-mirror of the corresponding pieces in MixLambdaPi/CaseA.lean. For
Mix (Pi, Lambda) the minimal nonpolarized gene g₁ has ODD rank 2m'+1, so the
bottom-chain b_m < d_m (and the a-version for the g⁻ charge) is anchored at the
odd level 2m'+1 and only applies for m' ≥ 1 (the m'=0, i.e. m=1, case is the
separate g₃ sub-case). The Case-2 top boundary is prime^[2n'+2] Y ≠ 0.
§16 bottom-chain b_m < d_m for Branch A Case 2, Mix (Pi, Lambda), at the odd
anchor m = 2m'+1 with m' ≥ 1. Uses the odd branch of cond_15_7_Mix_Pi_Lambda,
rank antitonicity, the level-1 gap, and twostep_snd = cells.
§16 bottom-chain a_m < c_m for Branch A Case 2, Mix (Pi, Lambda) (the
g⁻ charge via sign-duality). a-component analogue of branchA_case2_bm_lt.
Top-boundary nonvanishing for §16 Branch A Case 2 (Mix (Pi, Lambda),
gk = g⁺(2n'+2)): prime^[2n'+2] Y ≠ 0. b-mirror style: if it vanished,
prime^[2n'+1] Y (which lives in Mix (Lambda, Pi), oddPart ∈ Pi) would consist only of
rank-1 polarized genes, none positive (a positive g⁺(1) would trace to Y gk = 0 by
disjointness), so its first signature component is 0, contradicting a_X(2n'+1) ≥ 1.
Branch A Case 1 driver (Mix (Pi, Lambda)). Chains the propagation core and the
type4 assembly.
Branch A Case 2 driver (g₂ = g⁺(k), Mix (Pi, Lambda)). Chains the
b-propagation, the top boundary, and the type5 assembly.
Branch A edge case: X is a single nonpolarized gene g₁ (no second gene). Vacuous:
Y of equal rank with X ≤ Y forces Y = X (the unique odd-rank gene shape).
Branch A Case 1, b-component sub-branch (b_m < d_m): the sign-dual of
case1_full (apply Case 1 to -X, -Y, then negate). Level-1 asymmetry is sidestepped
since case1_full takes the self-dual total-rank gap.
Branch A Case 2 driver, g₂ = g⁻(k) charge (via sign-duality to the g⁺ driver
applied to (-X, -Y)). Takes the anchor a-strict ha_anchor (from am_lt for m'≥1,
or directly from ha when m'=0).
§16 Case 2 m=1, b₁=d₁ sub-case (the PL-specific g₃ leaf). Here g₁=g(1),
g₂=g⁺(k), a₁<c₁ (ha) and b₁=d₁, so X - g₁ - g₂ contains a negative or
nonpolarized gene g₃ of minimal rank t; the mutation g₂+g₃ → g(k-1)+g(t+1)
(t even) or g₂+g₃ → g(k-1)+g⁺(t+1) (t odd) gives Z ≤ Y. Formalization target.
Branch A Case 2: the second gene g₂ is polarized (§16 Case 2). Dispatches on
g₂'s charge (g⁺ direct / g⁻ sign-dual) and, at m'=0 (m=1), on b₁ vs d₁.
Branch A, multiplicity-one sub-case (X g₁ = 1). Extract g₂ of minimal rank in
X - g₁ and split on its polarization (§16 Cases 1–2); no second gene → vacuous edge.
Branch A of §16 Case A for Mix (Pi, Lambda): minimal-rank gene g₁
nonpolarized (odd rank). Dispatch on whether X ⊇ 2g(m).