§16 propagation core for Mix (Lambda, Pi) Branch A Case 1.

This is the hard inequality engine of §16: the hprop_even output consumed by exists_mutation_le_caseA_branchA_case1. Kept in a light file (imports only Prelim + Drops) so build iteration is fast.

theorem MixLambdaPi.rank_drop_le {Z : Chromosome} (hZ : Z ∈ Variety.Mix (Variety.Lambda, Variety.Pi)) (i : ℕ) : (Sigma.sigma Z i).1 + (Sigma.sigma Z i).2 - ((Sigma.sigma Z (i + 1)).1 + (Sigma.sigma Z (i + 1)).2) ≤ (Sigma.sigma Z 0).1 + (Sigma.sigma Z 0).2 - ((Sigma.sigma Z 1).1 + (Sigma.sigma Z 1).2)

Telescoped: the rank-drop at level i is at most the rank-drop at level 0.

theorem MixLambdaPi.KEY_Y {N : ℕ} (X Y : nMixLambdaPi N) (hXY : ↑X < ↑Y) (ha : (Sigma.sigma (↑↑X) 1).1 < (Sigma.sigma (↑↑Y) 1).1) {i : ℕ} (hi : Even i) : (Sigma.sigma (↑↑Y) i).1 - (Sigma.sigma (↑↑Y) (i + 2)).1 ≤ (Sigma.sigma (↑↑X) 0).1 + (Sigma.sigma (↑↑X) 0).2 - ((Sigma.sigma (↑↑X) 1).1 + (Sigma.sigma (↑↑X) 1).2) - 1

KEY_Y: the §16 bound on Y's a-component 2-step drop by r_0 - r_1 - 1.

theorem MixLambdaPi.cells {Z : Chromosome} : ↑(Chromosome.rank Z) - ↑(Chromosome.rank (Chromosome.prime Z)) = Finsupp.sum Z fun (x : Gene) (m : ℕ) => ↑m

theorem MixLambdaPi.twostep {W : Chromosome} {i : ℕ} (hW : ∀ g ∈ W.support, i + 2 ≤ g.rank) : (Sigma.sigma W i).1 - (Sigma.sigma W (i + 2)).1 = Finsupp.sum W fun (x : Gene) (m : ℕ) => ↑m

theorem MixLambdaPi.twostep_snd {W : Chromosome} {i : ℕ} (hW : ∀ g ∈ W.support, i + 2 ≤ g.rank) : (Sigma.sigma W i).2 - (Sigma.sigma W (i + 2)).2 = Finsupp.sum W fun (x : Gene) (m : ℕ) => ↑m

b-component analogue of twostep: the 2-step drop of the second sigma component equals the gene count, when all genes survive both steps.

theorem MixLambdaPi.sig_fst_isInt_even {Z : Chromosome} (hZ : Z ∈ Variety.Mix (Variety.Lambda, Variety.Pi)) {i : ℕ} (hi : Even i) : ∃ (z : ℤ), (Sigma.sigma Z i).1 = ↑z

Even-level integrality: at even level, the first signature component of a Mix (Lambda, Pi) element is an integer (Pi part integral; even part has even ranks so r/2 ∈ ℤ).

theorem MixLambdaPi.branchA_hprop_even_gen {N : ℕ} (X Y : nMixLambdaPi N) (hXY : ↑X < ↑Y) (ha : (Sigma.sigma (↑↑X) 1).1 < (Sigma.sigma (↑↑Y) 1).1) (m' n' : ℕ) : m' ≤ n' → ∀ (gm : Gene) (hgm_rank : gm.rank = 2 * m' + 2) (hgm_np : gm.type = GeneType.NonPolarized) (hgm1 : ↑↑X gm = 1) (hmin : ∀ g ∈ (↑↑X).support, 2 * m' + 2 ≤ g.rank) (h2nd : ∀ g ∈ (↑↑X - Finsupp.single gm 1).support, 2 * n' + 2 ≤ g.rank) (ha_m : (Sigma.sigma (↑↑X) (2 * m' + 2)).1 < (Sigma.sigma (↑↑Y) (2 * m' + 2)).1) (j : ℕ), 2 * m' + 2 ≤ j → j ≤ 2 * n' + 2 → Even j → (Sigma.sigma (↑↑X) j).1 + 1 ≤ (Sigma.sigma (↑↑Y) j).1

Generalized §16 drop-chain telescoping (gk-free). Given only the minimal nonpolarized gene gm of rank 2m'+2 with multiplicity one (hgm1), X minimal-rank ≥ 2m'+2 (hmin), and X - gm rank ≥ 2n'+2 (h2nd), the §16 chain propagates the strict start a_X(m) < a_Y(m) to a full-unit gap at every even level of [2m'+2, 2n'+2]. The proof never inspects the second gene, so it is reused (via sign-duality) for the b-component in Case 2 with a polarized second gene.

theorem MixLambdaPi.branchA_case1_hprop_even {N : ℕ} (X Y : nMixLambdaPi N) (hXY : ↑X < ↑Y) (ha : (Sigma.sigma (↑↑X) 1).1 < (Sigma.sigma (↑↑Y) 1).1) (m' n' : ℕ) (hmn : m' ≤ n') (gm gk : Gene) (hgm_rank : gm.rank = 2 * m' + 2) (hgm_np : gm.type = GeneType.NonPolarized) (hgk_rank : gk.rank = 2 * n' + 2) (hgk_np : gk.type = GeneType.NonPolarized) (hXgm : 0 < ↑↑X gm) : 0 < (↑↑X - Finsupp.single gm 1) gk → ∀ (hne : gm ≠ gk) (hmin : ∀ g ∈ (↑↑X).support, 2 * m' + 2 ≤ g.rank) (h2nd : ∀ g ∈ (↑↑X - Finsupp.single gm 1).support, 2 * n' + 2 ≤ g.rank) (ha_m : (Sigma.sigma (↑↑X) (2 * m' + 2)).1 < (Sigma.sigma (↑↑Y) (2 * m' + 2)).1) (j : ℕ), 2 * m' + 2 ≤ j → j ≤ 2 * n' + 2 → Even j → (Sigma.sigma (↑↑X) j).1 + 1 ≤ (Sigma.sigma (↑↑Y) j).1

§16 drop-chain telescoping for Branch A Case 1 (gk nonpolarized of rank 2n'+2). Derives mult(gm)=1 from disjointness of the two genes, then defers to gen.