CommonInterleaver: state the Chudnovsky–Seymour pair chain directly (part 2)

RealRooted.lean

@@ -228,7 +228,6 @@ import RealRooted.Challenges.OperatorPreservers
 import RealRooted.Challenges.VeroneseSections
 import RealRooted.Challenges.Wagner
 import RealRooted.ChudnovskySeymour.Core
-import RealRooted.ClosedSegmentCountEqFromAnalytic
 import RealRooted.CoefficientDominance
 import RealRooted.CoefficientDominance.LogConcavity
 import RealRooted.CoefficientDominance.RootGap
@@ -303,7 +302,6 @@ import RealRooted.CommonInterleaver.RootSlots
 import RealRooted.CommonInterleaver.RootSlots.Basic
 import RealRooted.CommonInterleaver.Sequence
 import RealRooted.CommonInterleaver.SameDegreeRootCount
-import RealRooted.CommonInterleaver.Statements
 import RealRooted.CommonInterleaver.SuccDegreeEndpoint
 import RealRooted.CommonInterleaver.SuccDegreeLowDegree
 import RealRooted.CommonInterleaver.FamilySum

RealRooted/ChudnovskySeymour/Core.lean

@@ -1,4 +1,3 @@
-import RealRooted.ClosedSegmentCountEqFromAnalytic
 import RealRooted.CommonInterleaverTwo
 import RealRooted.InterlacingSequenceBasic
 import RealRooted.SameDegreeCountFromAnalytic
@@ -9,37 +8,42 @@ namespace RealRooted
 
 open Polynomial
 
-/-- Chudnovsky--Seymour for two polynomials: compatible polynomials with positive
-leading coefficients have a common (right) interleaver.  The proof splits into
-the same-degree and successor-degree cases. -/
-theorem chudnovskySeymour_compatiblePairHasCommonInterleaver :
-    CompatiblePairHasCommonInterleaverStatement :=
-  compatiblePairHasCommonInterleaver_of_pairDegreeSplit_via_nonnegShift
-    PosComboNoCommonSameDegreePairHasCommonInterleaverNonneg
-    PosComboNoCommonSuccDegreePairHasCommonInterleaverNonneg
-
-/-- Chudnovsky--Seymour for two polynomials, common-left form: compatible
-polynomials with positive leading coefficients have a common left interleaver. -/
-theorem chudnovskySeymour_compatiblePairHasCommonLeftInterleaver :
-    CompatiblePairHasCommonLeftInterleaverPosStatement :=
-  compatiblePairHasCommonLeftInterleaverPos_of_pairBridge
-    chudnovskySeymour_compatiblePairHasCommonInterleaver
-
-/-- Two compatible polynomials with positive leading coefficients have a common
-interleaver. -/
+/-- Implicit-binder form of `chudnovskySeymour_compatiblePairHasCommonInterleaver`,
+kept for existing callers. -/
 theorem compatiblePairHasCommonInterleaver_chudnovskySeymour
     {f g : ℝ[X]} (hf : HasPosLeadingCoeff f) (hg : HasPosLeadingCoeff g)
     (h : Compatible f g) :
     ∃ k : ℝ[X], StrictInterl f k ∧ StrictInterl g k :=
   chudnovskySeymour_compatiblePairHasCommonInterleaver hf hg h
 
-/-- Two compatible polynomials with positive leading coefficients have a common
-left interleaver. -/
-theorem compatiblePairHasCommonLeftInterleaver_chudnovskySeymour
-    {f g : ℝ[X]} (hf : HasPosLeadingCoeff f) (hg : HasPosLeadingCoeff g)
+/-- **Chudnovsky--Seymour for two polynomials**, common-left form: compatible
+polynomials with positive leading coefficients have a common left interleaver.
+A common right interleaver is converted using degree closeness. -/
+theorem chudnovskySeymour_compatiblePairHasCommonLeftInterleaver
+    ⦃f g : ℝ[X]⦄ (hf : HasPosLeadingCoeff f) (hg : HasPosLeadingCoeff g)
     (h : Compatible f g) :
-    ∃ k : ℝ[X], StrictInterl k f ∧ StrictInterl k g :=
-  chudnovskySeymour_compatiblePairHasCommonLeftInterleaver hf hg h
+    ∃ k : ℝ[X], StrictInterl k f ∧ StrictInterl k g := by
+  have hclose : f.natDegree ≤ g.natDegree + 1 ∧ g.natDegree ≤ f.natDegree + 1 :=
+    h.natDegree_close hf hg
+  by_cases hdeg : f.natDegree ≤ g.natDegree
+  · obtain ⟨k, hfk, hgk⟩ := chudnovskySeymour_compatiblePairHasCommonInterleaver hf hg h
+    exact pairHasCommonLeftInterleaver_of_commonInterleaver hfk hgk hdeg hclose.2
+  · obtain ⟨k, hgk, hfk⟩ :=
+      chudnovskySeymour_compatiblePairHasCommonInterleaver hg hf h.comm
+    exact (pairHasCommonLeftInterleaver_of_commonInterleaver
+      hgk hfk (le_of_not_ge hdeg) hclose.1).imp fun _ hk => hk.symm
+
+/-- **Chudnovsky--Seymour**, four-way form: for a finite family of real-rooted
+polynomials with positive leading coefficients, pairwise compatibility,
+pairwise common interleavers, a common interleaver, and family compatibility
+are equivalent. -/
+theorem chudnovskySeymour_fourWay
+    {fs : List ℝ[X]}
+    (hrr : ∀ f ∈ fs, f ≠ 0 ∧ f.Splits)
+    (hpos : ∀ f ∈ fs, HasPosLeadingCoeff f) :
+    ChudnovskySeymourFourWayPackage fs :=
+  chudnovskySeymour_fourWay_of_pairBridgePos hrr hpos
+    chudnovskySeymour_compatiblePairHasCommonInterleaver
 
 /-- **Chudnovsky--Seymour.** A finite family of real-rooted polynomials with
 positive leading coefficients is pairwise compatible if and only if it has a
@@ -49,8 +53,7 @@ theorem chudnovskySeymour_pairwiseCompatible_iff_commonInterleaver
     (hrr : ∀ f ∈ fs, f ≠ 0 ∧ f.Splits)
     (hpos : ∀ f ∈ fs, HasPosLeadingCoeff f) :
     PairwiseCompatible fs ↔ HasCommonInterleaver fs :=
-  pairwiseCompatible_iff_hasCommonInterleaver_of_pairBridgePos hrr hpos
-    (fun _ _ hf hg h => compatiblePairHasCommonInterleaver_chudnovskySeymour hf hg h)
+  pairwiseCompatible_iff_hasCommonInterleaver_of_fourWay (chudnovskySeymour_fourWay hrr hpos)
 
 /-- **Chudnovsky--Seymour**, common-left form: a finite family of real-rooted
 polynomials with positive leading coefficients is pairwise compatible if and
@@ -60,9 +63,13 @@ theorem chudnovskySeymour_pairwiseCompatible_iff_commonLeftInterleaver
     (hrr : ∀ f ∈ fs, f ≠ 0 ∧ f.Splits)
     (hpos : ∀ f ∈ fs, HasPosLeadingCoeff f) :
     PairwiseCompatible fs ↔ HasCommonLeftInterleaver fs :=
-  pairwiseCompatible_iff_commonLeftInterleaver_of_pairwiseLeftBridge_direct
-    chudnovskySeymour_compatiblePairHasCommonLeftInterleaver
-    (fun f hf => (hrr f hf).2) hpos
+  ⟨fun hpair =>
+    hasCommonLeftInterleaver_of_pairwiseHasCommonLeftInterleaver
+      (fun f hf => (hrr f hf).2) hpos fun i j hij =>
+        chudnovskySeymour_compatiblePairHasCommonLeftInterleaver
+          (hpos (fs.get i) (fs.get_mem i)) (hpos (fs.get j) (fs.get_mem j))
+          (hpair i j hij),
+    fun hcommon => pairwiseCompatible_of_commonLeftInterleaver hcommon hpos⟩
 
 /-- **Chudnovsky--Seymour.** A finite family of real-rooted polynomials with
 positive leading coefficients is pairwise compatible if and only if every
@@ -72,8 +79,7 @@ theorem chudnovskySeymour_pairwiseCompatible_iff_familyCompatible
     (hrr : ∀ f ∈ fs, f ≠ 0 ∧ f.Splits)
     (hpos : ∀ f ∈ fs, HasPosLeadingCoeff f) :
     PairwiseCompatible fs ↔ FamilyCompatible fs :=
-  pairwiseCompatible_iff_familyCompatible_of_pairBridgePos hrr hpos
-    chudnovskySeymour_compatiblePairHasCommonInterleaver
+  pairwiseCompatible_iff_familyCompatible_of_fourWay (chudnovskySeymour_fourWay hrr hpos)
 
 /-- An interlacing sequence with nonnegative coefficients is compatible under
 all nonnegative weighted sums. -/
@@ -103,19 +109,6 @@ theorem IsInterlacingSeqNonneg.weightedSum_isPFPolynomial
   exact IsPFPolynomial.of_nonnegCoeffs_eq_zero_or_splits hnonneg <|
     (hfs.familyCompatible ws hmem hweights).imp_right And.right
 
-/-- The four equivalent Chudnovsky--Seymour conditions for a family with
-nonnegative coefficients: pairwise compatibility, pairwise and common
-interleavers, and family compatibility. -/
-theorem chudnovskySeymour_fourWay_nonnegCoeffs
-    {fs : List ℝ[X]}
-    (hrr : ∀ f ∈ fs, f ≠ 0 ∧ f.Splits)
-    (hpos : ∀ f ∈ fs, HasPosLeadingCoeff f)
-    (hnn : ∀ f ∈ fs, HasNonnegCoeffs f) :
-    ChudnovskySeymourFourWayPackage fs :=
-  chudnovskySeymour_fourWay_of_pairDegreeSplit_and_nonnegCoeffs hrr hpos hnn
-    PosComboNoCommonSameDegreePairHasCommonInterleaverNonneg
-    PosComboNoCommonSuccDegreePairHasCommonInterleaverNonneg
-
 /-- `chudnovskySeymour_pairwiseCompatible_iff_familyCompatible` with an unused
 nonnegativity hypothesis, kept for existing callers. -/
 theorem chudnovskySeymour_pairwiseCompatible_iff_familyCompatible_nonnegCoeffs

RealRooted/CommonInterleaver/AffineBoundary.lean

@@ -6,7 +6,7 @@ They turn the no-common boundary right-pair orientation statement into the
 positive affine-family bridge used by the common-interleaver reductions.
 -/
 import RealRooted.AffineFamily
-import RealRooted.CommonInterleaver.Statements
+import RealRooted.AllCombo
 import RealRooted.PosCombo
 
 open Polynomial
@@ -64,36 +64,4 @@ theorem pairHasCommonInterleaver_of_strictInterl_right_pair_nonneg
   have hf : (f ≠ 0 ∧ f.Splits) := isRealRooted_of_X_mul hstrictInterl.2.1.1 hstrictInterl.2.1.2
   exact ⟨X * f, strictInterl_self_X_mul_of_nonneg hf.1 hf.2 hfnn, hstrictInterl⟩
 
-/-- Orienting each boundary pair `(C t * f + g, X * f)` is already enough to
-recover the full affine-family hypothesis. The no-common condition for the
-boundary pair is automatic from nonnegative coefficients and the original
-no-common hypothesis. -/
-theorem posComboNoCommonAffineFamily_of_boundaryRightPairOrientation
-    (hboundary : PosComboNoCommonBoundaryRightPairOrientationStatement) :
-    PosComboNoCommonAffineFamilyStatement := by
-  intro f g hf_pos hg_pos hfnn hgnn hfg hdeg_lo hdeg_hi hno s t hs ht
-  let p : ℝ[X] := C t * f + g
-  have hp_rr : (p ≠ 0 ∧ p.Splits) := by
-    dsimp [p]
-    simpa using PosComboRealRooted.isRealRooted_add_left hfg ht
-  have hp_nn : HasNonnegCoeffs p := by
-    dsimp [p]
-    exact (nonnegCoeffs_C_mul ht.le hfnn).add hgnn
-  have hp_pos : HasPosLeadingCoeff p := hp_nn.pos_leadingCoeff hp_rr.1
-  have hXf_pos : HasPosLeadingCoeff (X * f) := hf_pos.X_mul
-  have hstrictInterl_or : StrictInterl p (X * f) ∨ StrictInterl (X * f) p := by
-    dsimp [p]
-    exact hboundary hf_pos hg_pos hfnn hgnn hfg hdeg_lo hdeg_hi hno ht
-  have hno_right : ∀ r, p.IsRoot r → ¬ (X * f).IsRoot r := by
-    dsimp [p]
-    exact no_common_boundary_right_pair_of_no_common_nonneg hfnn hgnn hno ht
-  have hstrictInterl : StrictInterl p (X * f) :=
-    strictInterl_right_pair_of_strictInterl_or_reverse_of_no_common_nonneg
-      hstrictInterl_or hp_rr.1 hp_rr.2 hp_nn hno_right
-  have hcombo_rr :
-      ((C (1 : ℝ) * p + C s * (X * f)) ≠ 0 ∧ (C (1 : ℝ) * p + C s * (X * f)).Splits) :=
-    StrictInterl.isRealRooted_nonneg_combo
-      hstrictInterl hp_pos hXf_pos (by simp) hs.le (Or.inl zero_lt_one)
-  grind
-
 end RealRooted

RealRooted/CommonInterleaver/FamilyUpgrade.lean

@@ -168,21 +168,6 @@ theorem hasCommonInterleaver_of_pairwiseHasCommonInterleaver
         hasCommonInterleaver_of_pairwiseHasCommonInterleaver_ge_two
           (f := f) (g := g) (fs := fs) hrr hpos hpair
 
-/-- Global finite-family right upgrade: pairwise common interleavers imply a
-single common interleaver under the usual split and positive-leading
-hypotheses. -/
-def CommonInterleaverFamilyUpgradeStatement : Prop :=
-  ∀ {fs : List ℝ[X]},
-    (∀ f ∈ fs, f.Splits) →
-    (∀ f ∈ fs, HasPosLeadingCoeff f) →
-    PairwiseHasCommonInterleaver fs →
-    HasCommonInterleaver fs
-
-/-- The proved global finite-family right upgrade, packaged as a statement alias. -/
-theorem commonInterleaverFamilyUpgrade :
-    CommonInterleaverFamilyUpgradeStatement :=
-  hasCommonInterleaver_of_pairwiseHasCommonInterleaver
-
 /-- Chudnovsky--Seymour `2 ⇒ 3`, left-oriented version: pairwise common left
 interleavers can be upgraded to a single common left interleaver. -/
 private theorem hasCommonLeftInterleaver_of_pairwiseHasCommonLeftInterleaver_ge_two
@@ -253,21 +238,6 @@ theorem hasCommonLeftInterleaver_of_pairwiseHasCommonLeftInterleaver
         hasCommonLeftInterleaver_of_pairwiseHasCommonLeftInterleaver_ge_two
           (f := f) (g := g) (fs := fs) hrr hpos hpair
 
-/-- Global finite-family left upgrade: pairwise common left interleavers imply a
-single common left interleaver under the usual split and positive-leading
-hypotheses. -/
-def CommonLeftInterleaverFamilyUpgradeStatement : Prop :=
-  ∀ {fs : List ℝ[X]},
-    (∀ f ∈ fs, f.Splits) →
-    (∀ f ∈ fs, HasPosLeadingCoeff f) →
-    PairwiseHasCommonLeftInterleaver fs →
-    HasCommonLeftInterleaver fs
-
-/-- The proved global finite-family left upgrade, packaged as a statement alias. -/
-theorem commonLeftInterleaverFamilyUpgrade :
-    CommonLeftInterleaverFamilyUpgradeStatement :=
-  hasCommonLeftInterleaver_of_pairwiseHasCommonLeftInterleaver
-
 /-- A common interleaver immediately implies real-rootedness of the full sum,
 by Wagner's finite-sum theorem on the right. -/
 theorem isRealRooted_sum_of_commonInterleaver

RealRooted/CommonInterleaver/PairBridge.lean

@@ -3,7 +3,7 @@ import RealRooted.CommonInterleaver.PairBridge.Compatibility.NonnegativeShift
 /-!
 # Pair bridge assembly for two-polynomial common interleavers
 
-Compatibility facade for the layered two-polynomial common-interleaver bridge.
-The forward, succ-degree, common-root reduction, endpoint, and nonnegative-shift
-layers live in dedicated children.
+Facade for the two-polynomial common-interleaver theorem.  The forward,
+succ-degree, common-root reduction, and nonnegative-shift layers live in
+dedicated children.
 -/