CommonInterleaver: delete dead Chudnovsky–Seymour reduction routes (part 1)

RealRooted/CommonInterleaver/AffineBoundary.lean

@@ -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/Compatibility.lean

@@ -13,98 +13,6 @@ noncomputable section
 
 namespace RealRooted
 
-/-- Reduction of no-common orientation to the all-combinations bridge plus
-Obreschkoff converse (`strictInterl_of_allComboRealRooted`). -/
-theorem posComboNoCommonOrientation_of_allComboBridge
-    (hallBridge : PosComboNoCommonToAllComboBridgeStatement) :
-    PosComboNoCommonOrientationStatement := by
-  intro f g hfg hf_pos hg_pos hdeg_lo hdeg_hi hno
-  have hall : AllComboRealRooted f g :=
-    hallBridge hf_pos hg_pos hfg hdeg_lo hdeg_hi hno
-  exact
-    CommonInterleaver.PairBridge.strictInterl_or_reverse_of_allComboRealRooted_ordered
-      hf_pos hg_pos hall hdeg_lo hdeg_hi
-
-/-- Converse reduction: the no-common orientation core immediately yields the
-all-combinations bridge by passing through `allComboRealRooted_of_strictInterl`. -/
-theorem posComboAllComboBridge_of_noCommonOrientation
-    (hstep : PosComboNoCommonOrientationStatement) :
-    PosComboNoCommonToAllComboBridgeStatement :=
-  fun _ _ hf_pos hg_pos hfg hdeg_lo hdeg_hi hno =>
-    allComboRealRooted_of_strictInterl_or_reverse <|
-    hstep hfg hf_pos hg_pos hdeg_lo hdeg_hi hno
-
-/-- The two no-common bridge formulations are equivalent:
-orientation (`StrictInterl f g ∨ StrictInterl g f`) and all-combinations real-rootedness. -/
-theorem posComboNoCommonBridge_iff_orientation :
-    PosComboNoCommonToAllComboBridgeStatement ↔
-      PosComboNoCommonOrientationStatement :=
-  ⟨posComboNoCommonOrientation_of_allComboBridge,
-    posComboAllComboBridge_of_noCommonOrientation⟩
-
-/-- Reduction of the two-polynomial bridge to an orientation theorem for the
-positive-combination cone. If one can show `StrictInterl f g ∨ StrictInterl g f` for every
-positive-leading `PosComboRealRooted` pair, then compatibility gives a common
-right interleaver immediately. -/
-theorem compatiblePairHasCommonInterleaver_of_posComboOrientation
-    (horient :
-      ∀ ⦃f g : ℝ[X]⦄,
-        HasPosLeadingCoeff f →
-        HasPosLeadingCoeff g →
-        PosComboRealRooted f g →
-        StrictInterl f g ∨ StrictInterl g f) :
-    CompatiblePairHasCommonInterleaverStatement :=
-  fun {_ _} hf_pos hg_pos hfg =>
-    pairHasCommonInterleaver_of_strictInterl_or_reverse <|
-      horient hf_pos hg_pos (hfg.toPosComboRealRooted hf_pos hg_pos)
-
-/-- Compatibility-to-common-interleaver reduction through the positive-combo
-bridge. -/
-theorem compatiblePairHasCommonInterleaver_of_posComboPair
-    (hposCombo : PosComboPairHasCommonInterleaverStatement) :
-    CompatiblePairHasCommonInterleaverStatement :=
-  fun {_ _} hf_pos hg_pos hfg =>
-    hposCombo hf_pos hg_pos
-      (hfg.toPosComboRealRooted hf_pos hg_pos)
-
-/-- If one has both the no-common-roots orientation core and degree closeness
-for the current `PosComboRealRooted` pair, then the pair has a common right
-interleaver. -/
-theorem posComboPairHasCommonInterleaver_of_noCommonOrientation_and_degreeBounds
-    (hstep : PosComboNoCommonOrientationStatement)
-    {f g : ℝ[X]}
-    (hf_pos : HasPosLeadingCoeff f) (hg_pos : HasPosLeadingCoeff g)
-    (hfg : PosComboRealRooted f g)
-    (hclose :
-      f.natDegree ≤ g.natDegree + 1 ∧
-        g.natDegree ≤ f.natDegree + 1) :
-    ∃ h : ℝ[X], StrictInterl f h ∧ StrictInterl g h := by
-  by_cases hfg_deg : f.natDegree ≤ g.natDegree
-  · have hstrictInterl_or : StrictInterl f g ∨ StrictInterl g f :=
-      PosComboRealRooted.strictInterl_or_reverse_of_posComboRealRooted_of_no_common
-        (hstep := fun hfg hf_pos hg_pos hdeg_lo hdeg_hi hno =>
-          hstep hfg hf_pos hg_pos hdeg_lo hdeg_hi hno)
-        hfg hf_pos hg_pos hfg_deg hclose.2
-    exact pairHasCommonInterleaver_of_strictInterl_or_reverse hstrictInterl_or
-  · have hgf_deg : g.natDegree ≤ f.natDegree := le_of_not_ge hfg_deg
-    have hstrictInterl_or : StrictInterl g f ∨ StrictInterl f g :=
-      PosComboRealRooted.strictInterl_or_reverse_of_posComboRealRooted_of_no_common
-        (hstep := fun hfg hf_pos hg_pos hdeg_lo hdeg_hi hno =>
-          hstep hfg hf_pos hg_pos hdeg_lo hdeg_hi hno)
-        (PosComboRealRooted.comm hfg) hg_pos hf_pos hgf_deg hclose.1
-    exact pairHasCommonInterleaver_of_strictInterl_or_reverse (Or.symm hstrictInterl_or)
-
-/-- If one has both the no-common-roots orientation core and degree closeness
-for `PosComboRealRooted` pairs, then every positive-leading `PosComboRealRooted`
-pair has a common right interleaver. -/
-theorem posComboPairHasCommonInterleaver_of_noCommonOrientation_and_degreeClose
-    (hstep : PosComboNoCommonOrientationStatement)
-    (hdegClose : PosComboNatDegreeCloseStatement) :
-    PosComboPairHasCommonInterleaverStatement :=
-  fun _ _ hf_pos hg_pos hfg =>
-    posComboPairHasCommonInterleaver_of_noCommonOrientation_and_degreeBounds
-      hstep hf_pos hg_pos hfg (hdegClose hfg)
-
 /-- Degree-closeness specialization with nonnegative coefficients. -/
 theorem posComboNatDegreeClose_of_nonnegCoeffs
     {f g : ℝ[X]}
@@ -117,32 +25,6 @@ theorem posComboNatDegreeClose_of_nonnegCoeffs
     hfg (hf_pos.ne_zero)
     (hg_pos.ne_zero) hfnn hgnn
 
-/-- In the nonnegative-coefficient regime, the no-common-roots orientation
-core already implies the full positive-combo pair bridge. -/
-theorem posComboPairHasCommonInterleaver_of_noCommonOrientation_and_nonnegCoeffs
-    (hstep : PosComboNoCommonOrientationStatement)
-    {f g : ℝ[X]}
-    (hf_pos : HasPosLeadingCoeff f) (hg_pos : HasPosLeadingCoeff g)
-    (hfnn : HasNonnegCoeffs f) (hgnn : HasNonnegCoeffs g)
-    (hfg : PosComboRealRooted f g) :
-    ∃ h : ℝ[X], StrictInterl f h ∧ StrictInterl g h :=
-  posComboPairHasCommonInterleaver_of_noCommonOrientation_and_degreeBounds
-    hstep hf_pos hg_pos hfg
-    (posComboNatDegreeClose_of_nonnegCoeffs hf_pos hg_pos hfnn hgnn hfg)
-
-/-- In the nonnegative-coefficient regime, the affine-family bridge already
-implies the full positive-combo pair bridge. -/
-theorem posComboPairHasCommonInterleaver_of_affineFamilyBridge_and_nonnegCoeffs
-    (haffBridge : PosComboNoCommonAffineFamilyStatement)
-    {f g : ℝ[X]}
-    (hf_pos : HasPosLeadingCoeff f) (hg_pos : HasPosLeadingCoeff g)
-    (hfnn : HasNonnegCoeffs f) (hgnn : HasNonnegCoeffs g)
-    (hfg : PosComboRealRooted f g) :
-    ∃ h : ℝ[X], StrictInterl f h ∧ StrictInterl g h :=
-  pairHasCommonInterleaver_of_strictInterl_or_reverse <|
-    posComboOrientation_of_affineFamilyBridge_and_nonnegCoeffs
-      haffBridge hf_pos hg_pos hfnn hgnn hfg
-
 /-- An ordered positive-combo pair bridge plus the nonnegative degree-closeness
 theorem gives the unordered pair bridge. -/
 theorem posComboPairHasCommonInterleaver_of_orderedBridge_and_nonnegCoeffs
@@ -211,32 +93,6 @@ private theorem compatiblePairHasCommonInterleaver_of_nonnegPosComboPairBridge
   hbridge hf_pos hg_pos hfnn hgnn
     (hfg.toPosComboRealRooted hf_pos hg_pos)
 
-private theorem nonnegPosComboPairBridge_of_noCommonOrientation
-    (hstep : PosComboNoCommonOrientationStatement) :
-    ∀ ⦃f g : ℝ[X]⦄,
-      HasPosLeadingCoeff f →
-      HasPosLeadingCoeff g →
-      HasNonnegCoeffs f →
-      HasNonnegCoeffs g →
-      PosComboRealRooted f g →
-      ∃ h : ℝ[X], StrictInterl f h ∧ StrictInterl g h :=
-  fun {_ _} hf_pos hg_pos hfnn hgnn hfg =>
-    posComboPairHasCommonInterleaver_of_noCommonOrientation_and_nonnegCoeffs
-      hstep hf_pos hg_pos hfnn hgnn hfg
-
-private theorem nonnegPosComboPairBridge_of_affineFamilyBridge
-    (haffBridge : PosComboNoCommonAffineFamilyStatement) :
-    ∀ ⦃f g : ℝ[X]⦄,
-      HasPosLeadingCoeff f →
-      HasPosLeadingCoeff g →
-      HasNonnegCoeffs f →
-      HasNonnegCoeffs g →
-      PosComboRealRooted f g →
-      ∃ h : ℝ[X], StrictInterl f h ∧ StrictInterl g h :=
-  fun {_ _} hf_pos hg_pos hfnn hgnn hfg =>
-    posComboPairHasCommonInterleaver_of_affineFamilyBridge_and_nonnegCoeffs
-      haffBridge hf_pos hg_pos hfnn hgnn hfg
-
 private theorem nonnegPosComboPairBridge_of_pairDegreeSplit
     (hsame : PosComboNoCommonSameDegreePairHasCommonInterleaverNonnegStatement)
     (hsucc : PosComboNoCommonSuccDegreePairHasCommonInterleaverNonnegStatement) :
@@ -251,32 +107,6 @@ private theorem nonnegPosComboPairBridge_of_pairDegreeSplit
     posComboPairHasCommonInterleaver_of_pairDegreeSplit_and_nonnegCoeffs
       hsame hsucc hf_pos hg_pos hfnn hgnn hfg
 
-/-- Compatibility-to-common-interleaver bridge under no-common orientation and
-nonnegative coefficients. -/
-theorem compatiblePairHasCommonInterleaver_of_noCommonOrientation_and_nonnegCoeffs
-    (hstep : PosComboNoCommonOrientationStatement)
-    {f g : ℝ[X]}
-    (hf_pos : HasPosLeadingCoeff f) (hg_pos : HasPosLeadingCoeff g)
-    (hfnn : HasNonnegCoeffs f) (hgnn : HasNonnegCoeffs g)
-    (hfg : Compatible f g) :
-    ∃ h : ℝ[X], StrictInterl f h ∧ StrictInterl g h :=
-  compatiblePairHasCommonInterleaver_of_nonnegPosComboPairBridge
-    (nonnegPosComboPairBridge_of_noCommonOrientation hstep)
-    hf_pos hg_pos hfnn hgnn hfg
-
-/-- Compatibility bridge under nonnegative coefficients, reduced to the
-affine-family bridge. -/
-theorem compatiblePairHasCommonInterleaver_of_affineFamilyBridge_and_nonnegCoeffs
-    (haffBridge : PosComboNoCommonAffineFamilyStatement)
-    {f g : ℝ[X]}
-    (hf_pos : HasPosLeadingCoeff f) (hg_pos : HasPosLeadingCoeff g)
-    (hfnn : HasNonnegCoeffs f) (hgnn : HasNonnegCoeffs g)
-    (hfg : Compatible f g) :
-    ∃ h : ℝ[X], StrictInterl f h ∧ StrictInterl g h :=
-  compatiblePairHasCommonInterleaver_of_nonnegPosComboPairBridge
-    (nonnegPosComboPairBridge_of_affineFamilyBridge haffBridge)
-    hf_pos hg_pos hfnn hgnn hfg
-
 /-- Compatibility bridge under nonnegative coefficients, reduced to the
 repaired degree-split package with common-interleaver conclusions in both
 branches. -/

RealRooted/CommonInterleaver/PairBridge/Compatibility/NonnegativeShift.lean

@@ -206,16 +206,6 @@ theorem compatiblePairHasCommonInterleaver_of_pairDegreeSplit_via_nonnegShift
       posComboPairHasCommonInterleaver_of_pairDegreeSplit_via_nonnegShift
         hsame hsucc hf_ne hf_splits hg_ne hg_splits hf_pos hg_pos hfg)
 
-/-- Shifted compatibility bridge from the concrete slot-data endpoints for the
-same-degree and succ-degree nonnegative branches. -/
-theorem compatiblePairHasCommonInterleaver_of_slotData_via_nonnegShift
-    (hsame : PosComboNoCommonSameDegreeSlotDataNonnegStatement)
-    (hsucc : PosComboNoCommonSuccDegreeSlotDataNonnegStatement) :
-    CompatiblePairHasCommonInterleaverStatement :=
-  compatiblePairHasCommonInterleaver_of_pairDegreeSplit_via_nonnegShift
-    (sameDegreePairHasCommonInterleaver_nonneg_of_slotData hsame)
-    (succDegreePairHasCommonInterleaver_nonneg_of_slotData hsucc)
-
 /-- Shifted compatibility bridge from the root-crossing formulations of the
 nonnegative same-degree and succ-degree branches.  The succ-degree branch also
 needs the left-splitting input that is part of its slot-data decomposition. -/
@@ -238,37 +228,6 @@ theorem compatiblePairHasCommonInterleaver_of_rootCrossing
   compatiblePairHasCommonInterleaver_of_rootCrossing_via_nonnegShift
     hsame PosComboSuccDegreeLeftSplitsNonnegStatement_of_rootContinuity hsucc
 
-/-- Shifted compatibility bridge from lower-threshold root-count
-formulations.  The succ-degree left endpoint is supplied by the
-root-continuity theorem before shifting. -/
-theorem compatiblePairHasCommonInterleaver_of_rootCount
-    (hsame : PosComboNoCommonSameDegreeRootCountNonnegStatement)
-    (hsucc : PosComboNoCommonSuccDegreeRootCountNonnegStatement) :
-    CompatiblePairHasCommonInterleaverStatement :=
-  compatiblePairHasCommonInterleaver_of_rootCrossing
-    (posComboNoCommonSameDegreeRootCrossing_of_rootCount hsame)
-    (posComboNoCommonSuccDegreeRootCrossing_of_rootCount hsucc)
-
-/-- Shifted compatibility bridge from upper-threshold root-count formulations
-in both the same-degree and succ-degree branches. -/
-theorem compatiblePairHasCommonInterleaver_of_rootCountAboveBoth
-    (hsame : PosComboNoCommonSameDegreeRootCountAboveNonnegStatement)
-    (hsucc : PosComboNoCommonSuccDegreeRootCountAboveNonnegStatement) :
-    CompatiblePairHasCommonInterleaverStatement :=
-  compatiblePairHasCommonInterleaver_of_rootCrossing
-    (posComboNoCommonSameDegreeRootCrossing_of_rootCountAbove hsame)
-    (posComboNoCommonSuccDegreeRootCrossing_of_rootCountAbove hsucc)
-
-/-- Shifted compatibility bridge from common-non-root lower-threshold root-count
-formulations in both branches. -/
-theorem compatiblePairHasCommonInterleaver_of_rootCountNonRoot
-    (hsame : PosComboNoCommonSameDegreeRootCountNonRootNonnegStatement)
-    (hsucc : PosComboNoCommonSuccDegreeRootCountNonRootNonnegStatement) :
-    CompatiblePairHasCommonInterleaverStatement :=
-  compatiblePairHasCommonInterleaver_of_rootCrossing
-    (posComboNoCommonSameDegreeRootCrossing_of_rootCountNonRoot hsame)
-    (posComboNoCommonSuccDegreeRootCrossing_of_rootCountNonRoot hsucc)
-
 /-- Shifted compatibility bridge from common-non-root upper-threshold root-count
 formulations in both branches. -/
 theorem compatiblePairHasCommonInterleaver_of_rootCountAboveBothNonRoot