Section 17 core after the induction and lifting reductions

The joint Label 3/4 induction first removes common genes and handles every positive level at which the two sigma columns agree. Consequently this file starts precisely from condition (17.1) of Djoković: whenever prime^[k] Y is nonzero at a positive level, the two sigma columns are unequal. The remaining proof is the type9--type17 classification from §17.

theorem Mix2LambdaPi.exists_mutation_le_reduced (m : ℕ) (X Y : nMix2LambdaPi (m + 2)) (hXY : ↑X < ↑Y) (hcommon : ¬∃ (g : Gene), 0 < ↑↑X g ∧ 0 < ↑↑Y g) (hsigeq : ¬∃ (k : ℕ), 0 < k ∧ (⇑Chromosome.prime)^[k] ↑↑Y ≠ 0 ∧ Sigma.sigma (↑↑X) k = Sigma.sigma (↑↑Y) k) : ∃ (Z : ↥(Variety.Mix (2 • Variety.Lambda, Variety.Pi))), Step (↑X) Z ∧ Z ≤ ↑Y

The primitive-classification core of §17 for Mix (2 • Lambda, Pi).

The hypotheses are disjointness and the negation of a positive sigma-agreement level. The latter is the Lean form of the reduction leading to (17.1).