Documentation

YoungDiagram.Theorem6.MixCase4

Case 4 (§15.10) for Mix (Lambda, Pi). #

This file factors the Case-4 obligation for Mix (Lambda, Pi) into:

This mirrors Pi.exists_mutation_le_fifteen_ten in YoungDiagram/Theorem6/Pi.lean. The Case-B branch is fully proved via the negation lemmas; the Case-A core is delegated to MixLambdaPi.exists_mutation_le_caseA / MixPiLambda.exists_mutation_le_caseA (files MixLambdaPi/CaseA.lean, MixPiLambda/CaseA.lean), which dispatch on the minimal-rank gene's polarization (§16 Branch A / Branch B); the two branch leaves per variety are the remaining sorrys.

source
theorem MixVarietyJoint.exists_mutation_le_fifteen_ten_LP_caseA (m : ℕ) :
(∀ k < m + 2, ∀ (X Y : nMixLambdaPi k), ↑X < ↑Y → ∃ (Z : ↥(Variety.Mix (Variety.Lambda, Variety.Pi))), MixLambdaPi.Step (↑X) Z ∧ Z ≤ ↑Y) → (∀ k < m + 2, ∀ (X Y : nMixPiLambda k), ↑X < ↑Y → ∃ (Z : ↥(Variety.Mix (Variety.Pi, Variety.Lambda))), MixPiLambda.Step (↑X) Z ∧ Z ≤ ↑Y) → ∀ (X Y : nMixLambdaPi (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) (hXpn : ¬∃ (g : Gene) (h : Gene), g.rank = h.rank ∧ g.type = GeneType.Positive ∧ h.type = GeneType.Negative ∧ 0 < ↑↑X g ∧ 0 < ↑↑X h) (ha : (Sigma.sigma (↑↑X) 1).1 < (Sigma.sigma (↑↑Y) 1).1), ∃ (Z : ↥(Variety.Mix (Variety.Lambda, Variety.Pi))), MixLambdaPi.Step (↑X) Z ∧ Z ≤ ↑Y

Case A of §15.10 for Mix (Lambda, Pi): the additional hypothesis is (sigma X 1).1 < (sigma Y 1).1. This is the sorried core.

source
theorem MixVarietyJoint.exists_mutation_le_fifteen_ten_LP (m : ℕ) (ihLP : ∀ k < m + 2, ∀ (X Y : nMixLambdaPi k), ↑X < ↑Y → ∃ (Z : ↥(Variety.Mix (Variety.Lambda, Variety.Pi))), MixLambdaPi.Step (↑X) Z ∧ Z ≤ ↑Y) (ihPL : ∀ k < m + 2, ∀ (X Y : nMixPiLambda k), ↑X < ↑Y → ∃ (Z : ↥(Variety.Mix (Variety.Pi, Variety.Lambda))), MixPiLambda.Step (↑X) Z ∧ Z ≤ ↑Y) (X Y : nMixLambdaPi (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) (hXpn : ¬∃ (g : Gene) (h : Gene), g.rank = h.rank ∧ g.type = GeneType.Positive ∧ h.type = GeneType.Negative ∧ 0 < ↑↑X g ∧ 0 < ↑↑X h) :
∃ (Z : ↥(Variety.Mix (Variety.Lambda, Variety.Pi))), MixLambdaPi.Step (↑X) Z ∧ Z ≤ ↑Y

Case 4 (§15.10) for Mix (Lambda, Pi). Dispatches to Case A on the branch (sigma X 1).1 < (sigma Y 1).1; on the other branch builds the sign-dual and reduces to Case A applied to -X, -Y.

source
theorem MixVarietyJoint.exists_mutation_le_fifteen_ten_PL_caseA (m : ℕ) :
(∀ k < m + 2, ∀ (X Y : nMixLambdaPi k), ↑X < ↑Y → ∃ (Z : ↥(Variety.Mix (Variety.Lambda, Variety.Pi))), MixLambdaPi.Step (↑X) Z ∧ Z ≤ ↑Y) → (∀ k < m + 2, ∀ (X Y : nMixPiLambda k), ↑X < ↑Y → ∃ (Z : ↥(Variety.Mix (Variety.Pi, Variety.Lambda))), MixPiLambda.Step (↑X) Z ∧ Z ≤ ↑Y) → ∀ (X Y : nMixPiLambda (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) (hXpn : ¬∃ (g : Gene) (h : Gene), g.rank = h.rank ∧ g.type = GeneType.Positive ∧ h.type = GeneType.Negative ∧ 0 < ↑↑X g ∧ 0 < ↑↑X h) (ha : (Sigma.sigma (↑↑X) 1).1 < (Sigma.sigma (↑↑Y) 1).1), ∃ (Z : ↥(Variety.Mix (Variety.Pi, Variety.Lambda))), MixPiLambda.Step (↑X) Z ∧ Z ≤ ↑Y

Case A of §15.10 for Mix (Pi, Lambda): the additional hypothesis is (sigma X 1).1 < (sigma Y 1).1. This is the sorried core.

source
theorem MixVarietyJoint.exists_mutation_le_fifteen_ten_PL (m : ℕ) (ihLP : ∀ k < m + 2, ∀ (X Y : nMixLambdaPi k), ↑X < ↑Y → ∃ (Z : ↥(Variety.Mix (Variety.Lambda, Variety.Pi))), MixLambdaPi.Step (↑X) Z ∧ Z ≤ ↑Y) (ihPL : ∀ k < m + 2, ∀ (X Y : nMixPiLambda k), ↑X < ↑Y → ∃ (Z : ↥(Variety.Mix (Variety.Pi, Variety.Lambda))), MixPiLambda.Step (↑X) Z ∧ Z ≤ ↑Y) (X Y : nMixPiLambda (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) (hXpn : ¬∃ (g : Gene) (h : Gene), g.rank = h.rank ∧ g.type = GeneType.Positive ∧ h.type = GeneType.Negative ∧ 0 < ↑↑X g ∧ 0 < ↑↑X h) :
∃ (Z : ↥(Variety.Mix (Variety.Pi, Variety.Lambda))), MixPiLambda.Step (↑X) Z ∧ Z ≤ ↑Y

Case 4 (§15.10) for Mix (Pi, Lambda). Dispatches to Case A on the branch (sigma X 1).1 < (sigma Y 1).1; on the other branch builds the sign-dual and reduces to Case A applied to -X, -Y.