theorem Mix2LambdaPi.rank_one_double_same_gene_tail_cases {m p : ℕ} (X Y : nMix2LambdaPi (m + 2)) (hXY : ↑X < ↑Y) (hcommon : ∀ (g : Gene), 0 < ↑↑X g → ↑↑Y g ≤ 0) (h17_1 : ∀ (k : ℕ), 0 < k → (⇑Chromosome.prime)^[k] ↑↑Y ≠ 0 → Chromosome.rank ((⇑Chromosome.prime)^[k] ↑↑X) < Chromosome.rank ((⇑Chromosome.prime)^[k] ↑↑Y)) (hXpol : (↑↑X).IsPolarized) (hno_pair : ¬∃ (gpos : Gene) (gneg : Gene), gpos.rank = gneg.rank ∧ gpos.type = GeneType.Positive ∧ gneg.type = GeneType.Negative ∧ 0 < ↑↑X gpos ∧ 0 < ↑↑X gneg) (g g₂ : Gene) : 0 < ↑↑X g → ∀ (hgmin : ∀ (g' : Gene), 0 < ↑↑X g' → g.rank ≤ g'.rank) (hg_pol : g.type ≠ GeneType.NonPolarized), g.rank = 2 * p + 1 → p = 0 → ∀ (hg_rank_one : g.rank = 1), ↑↑X (-g) = 0 → ∀ (hg_two : 2 ≤ ↑↑X g) (hseed1 : (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑X)).1 < (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑Y)).1 ∧ (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑X)).2 < (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑Y)).2) (hXsig1_eq : (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑X)).1 = (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑X)).2) (hYsig1_eq : (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑Y)).1 = (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑Y)).2) (hgap1 : (1, 1) + Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑X) ≤ Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑Y)) (restAfterDouble restAfterTriple tailAfterG : Chromosome), restAfterDouble = ↑↑X - Finsupp.single g 1 - Finsupp.single g 1 → restAfterDouble ≠ 0 → restAfterDouble ∈ Variety.Mix (2 • Variety.Lambda, Variety.Pi) → (⇑Chromosome.prime)^[1] ↑↑X = (⇑Chromosome.prime)^[1] restAfterDouble → ((Finsupp.sum restAfterDouble fun (x : Gene) (n : ℕ) => n) + 2 = Finsupp.sum ↑↑X fun (x : Gene) (n : ℕ) => n) → 0 < restAfterDouble g₂ → (∀ (g' : Gene), 0 < restAfterDouble g' → g₂.rank ≤ g'.rank) → 0 < ↑↑X g₂ → g₂.type ≠ GeneType.NonPolarized → Odd g₂.rank → (∀ (h : Gene), 0 < ↑↑X h → h ≠ g → 3 ≤ h.rank) → (∀ (h : Gene), 0 < ↑↑X h → h ≠ g → g₂.rank ≤ h.rank) → (g₂ = g → 3 ≤ ↑↑X g) → (g₂ ≠ g → 3 ≤ g₂.rank) → ∀ (htype16_boundary : ∀ {q : ℕ} (gsingle : Gene), gsingle.type = -g.type → gsingle.rank = 2 * q + 1 → 1 ≤ ↑↑X gsingle → ↑(Y16 ⋯ hg_pol) + (↑↑X - Finsupp.single g 1 - Finsupp.single g 1 - Finsupp.single gsingle 1) ≤ ↑↑Y → ∃ (Z : ↥(Variety.Mix (2 • Variety.Lambda, Variety.Pi))), Step (↑X) Z ∧ Z ≤ ↑Y) (htype14_boundary : ∀ {q : ℕ} (gopp : Gene), gopp.type = -g.type → gopp.rank = 2 * q + 1 → 2 ≤ ↑↑X gopp → ↑(Y14 ⋯ hg_pol) + (↑↑X - Finsupp.single g 1 - Finsupp.single g 1 - Finsupp.single gopp 1 - Finsupp.single gopp 1) ≤ ↑↑Y → ∃ (Z : ↥(Variety.Mix (2 • Variety.Lambda, Variety.Pi))), Step (↑X) Z ∧ Z ≤ ↑Y), g₂ = g → 3 ≤ ↑↑X g → ∀ (hrestAfterTriple_eq : restAfterTriple = ↑↑X - Finsupp.single g 1 - Finsupp.single g 1 - Finsupp.single g 1), (⇑Chromosome.prime)^[1] ↑↑X = (⇑Chromosome.prime)^[1] restAfterTriple → ((Finsupp.sum restAfterTriple fun (x : Gene) (n : ℕ) => n) + 3 = Finsupp.sum ↑↑X fun (x : Gene) (n : ℕ) => n) → ∀ (htailAfterG_def : tailAfterG = ↑↑X - Finsupp.single g (↑↑X g)), tailAfterG g = 0 → ∀ (htailAfterG_pos_X_ne : ∀ (h : Gene), 0 < tailAfterG h → 0 < ↑↑X h ∧ h ≠ g) (htailAfterG_rank_ge_three : ∀ (h : Gene), 0 < tailAfterG h → 3 ≤ h.rank), (tailAfterG = 0 → ∃ (Z : ↥(Variety.Mix (2 • Variety.Lambda, Variety.Pi))), Step (↑X) Z ∧ Z ≤ ↑Y) ∧ ∀ (gtail : Gene), 0 < tailAfterG gtail → (∀ (h : Gene), 0 < tailAfterG h → gtail.rank ≤ h.rank) → 3 ≤ gtail.rank → ∃ (Z : ↥(Variety.Mix (2 • Variety.Lambda, Variety.Pi))), Step (↑X) Z ∧ Z ≤ ↑Y

theorem Mix2LambdaPi.rank_one_double_same_gene_tail_frontier {m p : ℕ} (X Y : nMix2LambdaPi (m + 2)) (hXY : ↑X < ↑Y) (hcommon : ∀ (g : Gene), 0 < ↑↑X g → ↑↑Y g ≤ 0) (h17_1 : ∀ (k : ℕ), 0 < k → (⇑Chromosome.prime)^[k] ↑↑Y ≠ 0 → Chromosome.rank ((⇑Chromosome.prime)^[k] ↑↑X) < Chromosome.rank ((⇑Chromosome.prime)^[k] ↑↑Y)) (hXpol : (↑↑X).IsPolarized) (hno_pair : ¬∃ (gpos : Gene) (gneg : Gene), gpos.rank = gneg.rank ∧ gpos.type = GeneType.Positive ∧ gneg.type = GeneType.Negative ∧ 0 < ↑↑X gpos ∧ 0 < ↑↑X gneg) (g g₂ : Gene) (hgX : 0 < ↑↑X g) (hgmin : ∀ (g' : Gene), 0 < ↑↑X g' → g.rank ≤ g'.rank) (hg_pol : g.type ≠ GeneType.NonPolarized) (hp : g.rank = 2 * p + 1) (hp0 : p = 0) (hg_rank_one : g.rank = 1) (hXneg_zero : ↑↑X (-g) = 0) (hg_two : 2 ≤ ↑↑X g) (hseed1 : (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑X)).1 < (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑Y)).1 ∧ (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑X)).2 < (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑Y)).2) (hXsig1_eq : (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑X)).1 = (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑X)).2) (hYsig1_eq : (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑Y)).1 = (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑Y)).2) (hgap1 : (1, 1) + Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑X) ≤ Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑Y)) (restAfterDouble restAfterTriple tailAfterG : Chromosome) (hrestAfterDouble_eq : restAfterDouble = ↑↑X - Finsupp.single g 1 - Finsupp.single g 1) (hrestAfterDouble_ne : restAfterDouble ≠ 0) (hrestAfterDouble_mem : restAfterDouble ∈ Variety.Mix (2 • Variety.Lambda, Variety.Pi)) (hprimeX_eq_restAfterDouble : (⇑Chromosome.prime)^[1] ↑↑X = (⇑Chromosome.prime)^[1] restAfterDouble) (hrestAfterDouble_total : (Finsupp.sum restAfterDouble fun (x : Gene) (n : ℕ) => n) + 2 = Finsupp.sum ↑↑X fun (x : Gene) (n : ℕ) => n) (hg₂_rest : 0 < restAfterDouble g₂) (hg₂min : ∀ (g' : Gene), 0 < restAfterDouble g' → g₂.rank ≤ g'.rank) (hXg₂ : 0 < ↑↑X g₂) (hg₂_pol : g₂.type ≠ GeneType.NonPolarized) (hg₂_odd : Odd g₂.rank) (hX_rank_ge_three_of_ne_g : ∀ (h : Gene), 0 < ↑↑X h → h ≠ g → 3 ≤ h.rank) (hg₂min_X_ne_g : ∀ (h : Gene), 0 < ↑↑X h → h ≠ g → g₂.rank ≤ h.rank) (hg₂_same_extra : g₂ = g → 3 ≤ ↑↑X g) (hg₂_rank_ge_three_of_ne_g : g₂ ≠ g → 3 ≤ g₂.rank) (htype16_boundary : ∀ {q : ℕ} (gsingle : Gene), gsingle.type = -g.type → gsingle.rank = 2 * q + 1 → 1 ≤ ↑↑X gsingle → ↑(Y16 ⋯ hg_pol) + (↑↑X - Finsupp.single g 1 - Finsupp.single g 1 - Finsupp.single gsingle 1) ≤ ↑↑Y → ∃ (Z : ↥(Variety.Mix (2 • Variety.Lambda, Variety.Pi))), Step (↑X) Z ∧ Z ≤ ↑Y) (htype14_boundary : ∀ {q : ℕ} (gopp : Gene), gopp.type = -g.type → gopp.rank = 2 * q + 1 → 2 ≤ ↑↑X gopp → ↑(Y14 ⋯ hg_pol) + (↑↑X - Finsupp.single g 1 - Finsupp.single g 1 - Finsupp.single gopp 1 - Finsupp.single gopp 1) ≤ ↑↑Y → ∃ (Z : ↥(Variety.Mix (2 • Variety.Lambda, Variety.Pi))), Step (↑X) Z ∧ Z ≤ ↑Y) (hsame : g₂ = g) (hg_extra : 3 ≤ ↑↑X g) (hrestAfterTriple_eq : restAfterTriple = ↑↑X - Finsupp.single g 1 - Finsupp.single g 1 - Finsupp.single g 1) (hprimeX_eq_restAfterTriple : (⇑Chromosome.prime)^[1] ↑↑X = (⇑Chromosome.prime)^[1] restAfterTriple) (hrestAfterTriple_total : (Finsupp.sum restAfterTriple fun (x : Gene) (n : ℕ) => n) + 3 = Finsupp.sum ↑↑X fun (x : Gene) (n : ℕ) => n) (htailAfterG_def : tailAfterG = ↑↑X - Finsupp.single g (↑↑X g)) (htailAfterG_g_zero : tailAfterG g = 0) (htailAfterG_pos_X_ne : ∀ (h : Gene), 0 < tailAfterG h → 0 < ↑↑X h ∧ h ≠ g) (htailAfterG_rank_ge_three : ∀ (h : Gene), 0 < tailAfterG h → 3 ≤ h.rank) (htailAfterG_zero_or_min : tailAfterG = 0 ∨ ∃ (gtail : Gene), 0 < tailAfterG gtail ∧ (∀ (h : Gene), 0 < tailAfterG h → gtail.rank ≤ h.rank) ∧ 3 ≤ gtail.rank) : ∃ (Z : ↥(Variety.Mix (2 • Variety.Lambda, Variety.Pi))), Step (↑X) Z ∧ Z ≤ ↑Y

theorem Mix2LambdaPi.rank_one_double_same_gene_extra {m p : ℕ} (X Y : nMix2LambdaPi (m + 2)) (hXY : ↑X < ↑Y) (hcommon : ∀ (g : Gene), 0 < ↑↑X g → ↑↑Y g ≤ 0) (h17_1 : ∀ (k : ℕ), 0 < k → (⇑Chromosome.prime)^[k] ↑↑Y ≠ 0 → Chromosome.rank ((⇑Chromosome.prime)^[k] ↑↑X) < Chromosome.rank ((⇑Chromosome.prime)^[k] ↑↑Y)) (hXpol : (↑↑X).IsPolarized) (hno_pair : ¬∃ (gpos : Gene) (gneg : Gene), gpos.rank = gneg.rank ∧ gpos.type = GeneType.Positive ∧ gneg.type = GeneType.Negative ∧ 0 < ↑↑X gpos ∧ 0 < ↑↑X gneg) (g g₂ : Gene) (hgX : 0 < ↑↑X g) (hgmin : ∀ (g' : Gene), 0 < ↑↑X g' → g.rank ≤ g'.rank) (hg_pol : g.type ≠ GeneType.NonPolarized) (hp : g.rank = 2 * p + 1) (hp0 : p = 0) (hg_rank_one : g.rank = 1) (hXneg_zero : ↑↑X (-g) = 0) (hg_two : 2 ≤ ↑↑X g) (hseed1 : (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑X)).1 < (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑Y)).1 ∧ (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑X)).2 < (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑Y)).2) (hXsig1_eq : (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑X)).1 = (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑X)).2) (hYsig1_eq : (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑Y)).1 = (Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑Y)).2) (hgap1 : (1, 1) + Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑X) ≤ Chromosome.signature ((⇑Chromosome.prime)^[1] ↑↑Y)) (restAfterDouble : Chromosome) (hrestAfterDouble_eq : restAfterDouble = ↑↑X - Finsupp.single g 1 - Finsupp.single g 1) (hrestAfterDouble_ne : restAfterDouble ≠ 0) (hrestAfterDouble_mem : restAfterDouble ∈ Variety.Mix (2 • Variety.Lambda, Variety.Pi)) (hprimeX_eq_restAfterDouble : (⇑Chromosome.prime)^[1] ↑↑X = (⇑Chromosome.prime)^[1] restAfterDouble) (hrestAfterDouble_total : (Finsupp.sum restAfterDouble fun (x : Gene) (n : ℕ) => n) + 2 = Finsupp.sum ↑↑X fun (x : Gene) (n : ℕ) => n) (hg₂_rest : 0 < restAfterDouble g₂) (hg₂min : ∀ (g' : Gene), 0 < restAfterDouble g' → g₂.rank ≤ g'.rank) (hXg₂ : 0 < ↑↑X g₂) (hg₂_pol : g₂.type ≠ GeneType.NonPolarized) (hg₂_odd : Odd g₂.rank) (hX_rank_ge_three_of_ne_g : ∀ (h : Gene), 0 < ↑↑X h → h ≠ g → 3 ≤ h.rank) (hg₂min_X_ne_g : ∀ (h : Gene), 0 < ↑↑X h → h ≠ g → g₂.rank ≤ h.rank) (hg₂_same_extra : g₂ = g → 3 ≤ ↑↑X g) (hg₂_rank_ge_three_of_ne_g : g₂ ≠ g → 3 ≤ g₂.rank) (htype16_boundary : ∀ {q : ℕ} (gsingle : Gene), gsingle.type = -g.type → gsingle.rank = 2 * q + 1 → 1 ≤ ↑↑X gsingle → ↑(Y16 ⋯ hg_pol) + (↑↑X - Finsupp.single g 1 - Finsupp.single g 1 - Finsupp.single gsingle 1) ≤ ↑↑Y → ∃ (Z : ↥(Variety.Mix (2 • Variety.Lambda, Variety.Pi))), Step (↑X) Z ∧ Z ≤ ↑Y) (htype14_boundary : ∀ {q : ℕ} (gopp : Gene), gopp.type = -g.type → gopp.rank = 2 * q + 1 → 2 ≤ ↑↑X gopp → ↑(Y14 ⋯ hg_pol) + (↑↑X - Finsupp.single g 1 - Finsupp.single g 1 - Finsupp.single gopp 1 - Finsupp.single gopp 1) ≤ ↑↑Y → ∃ (Z : ↥(Variety.Mix (2 • Variety.Lambda, Variety.Pi))), Step (↑X) Z ∧ Z ≤ ↑Y) (hsame : g₂ = g) : ∃ (Z : ↥(Variety.Mix (2 • Variety.Lambda, Variety.Pi))), Step (↑X) Z ∧ Z ≤ ↑Y

The same-gene extra-multiplicity frontier in the rank-one-double no-pair branch.

Here the residue-minimal gene after removing two copies of the rank-one source is again the rank-one gene itself, so X has at least three copies of that minimal gene. The large dispatcher reduces to this focused frontier before continuing with the Type14/Type16 alternatives.