Prove Liu cross-owned gaps by bounded continuity

RealRooted.lean

@@ -99,6 +99,8 @@ import RealRooted.DegreeDropDivXPrec
 import RealRooted.DegreeDropReversal
 import RealRooted.DegreeIncreasingLocalLowerCount
 import RealRooted.Derivative
+import RealRooted.DerivativeShiftRootMatching
+import RealRooted.DerivativeShiftSequence
 import RealRooted.DifferentialBlocks
 import RealRooted.ElementaryDifferential
 import RealRooted.EulerOperator
@@ -141,9 +143,12 @@ import RealRooted.LiebSokalPointwise
 import RealRooted.Linear
 import RealRooted.LinearPowerFamily
 import RealRooted.LiuOppositeSigns
+import RealRooted.LiuOppositeSigns.BoundedIntervalContinuity
 import RealRooted.LiuOppositeSigns.CommonInterleaverConsequences
 import RealRooted.LiuOppositeSigns.Corollary22
 import RealRooted.LiuOppositeSigns.DeletionBranches
+import RealRooted.LiuOppositeSigns.DerivativeShiftRegularization
+import RealRooted.LiuOppositeSigns.DerivativeShiftSequenceRegularization
 import RealRooted.LiuOppositeSigns.FactorReturnAssembly
 import RealRooted.LiuOppositeSigns.FactorReturnLeft
 import RealRooted.LiuOppositeSigns.FactorReturnStatements
@@ -162,6 +167,8 @@ import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.RootOrderUpper
 import RealRooted.LiuOppositeSigns.ForwardLowDegree
 import RealRooted.LiuOppositeSigns.NonnegCoeffs
 import RealRooted.LiuOppositeSigns.PositiveSplitPair
+import RealRooted.LiuOppositeSigns.RootCountRelStability
+import RealRooted.LiuOppositeSigns.RootCountClosure
 import RealRooted.LiuOppositeSigns.Theorem21Assembly
 import RealRooted.LiuOppositeSigns.Theorem21Statements
 import RealRooted.LiuOppositeSigns.XSub.CubicCubic
@@ -199,6 +206,8 @@ import RealRooted.Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
 import RealRooted.Mathlib.Combinatorics.Enumerative.OrderedSubsetPairs
 import RealRooted.Mathlib.Data.List.Interleave
 import RealRooted.Mathlib.Data.List.Zip
+import RealRooted.Mathlib.Data.Multiset.Rel
+import RealRooted.RootMatchingSort
 import RealRooted.Mathlib.Data.Nat.Cast.Basic
 import RealRooted.Mathlib.Data.Nat.Choose.Cast
 import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.Basic
@@ -231,6 +240,7 @@ import RealRooted.RectangularConvolutionIdentity
 import RealRooted.RectangularPolarization
 import RealRooted.RectangularPolarizationComplement
 import RealRooted.RecurrenceDiscriminant
+import RealRooted.ReflectedRootCountLocalConstancy
 import RealRooted.RootContinuity
 import RealRooted.RootCountFinite
 import RealRooted.RootCountJump

RealRooted/AllCombo.lean

@@ -87,11 +87,6 @@ lemma allComboRealRooted_iterate_derivative
       exact allComboRealRooted_derivative
         (allComboRealRooted_iterate_derivative hall n)
 
-lemma iterateTDeriv_linear_combo (eps α β : ℝ) (n : ℕ) (f g : ℝ[X]) :
-    iterateTDeriv eps n (C α * f + C β * g) =
-      C α * iterateTDeriv eps n f + C β * iterateTDeriv eps n g := by
-  rw [iterateTDeriv_add, iterateTDeriv_C_mul, iterateTDeriv_C_mul]
-
 lemma TDeriv_eq_zero_iff (eps : ℝ) {p : ℝ[X]} :
     TDeriv eps p = 0 ↔ p = 0 := by
   constructor

RealRooted/CommonInterleaver/RootCountCombinatorics.lean

@@ -462,6 +462,28 @@ theorem succDegreeRootCrossing_of_rootCount
     rw [card_roots_of_splits hg, hdeg]
   exact succRootCrossing_of_count_le_two hMcard hNcard hcount
 
+/-- Converse root-count bridge from successor-degree descending-root crossing
+to the asymmetric lower-threshold formulation. -/
+theorem succDegreeRootCount_of_rootCrossing
+    {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits)
+    (hdeg : g.natDegree = f.natDegree + 1)
+    (hcross :
+      (∀ j, 1 ≤ j → j ≤ f.natDegree →
+          (rootSeqDesc g).getD j 0 ≤
+            (rootSeqDesc f).getD (j - 1) 0) ∧
+      (∀ j, 1 ≤ j → j < f.natDegree →
+          (rootSeqDesc f).getD j 0 ≤
+            (rootSeqDesc g).getD (j - 1) 0)) :
+    ∀ x : ℝ,
+      ((f.roots.filter (· ≤ x)).card : ℤ) -
+          (g.roots.filter (· ≤ x)).card ≤ 0 ∧
+      ((g.roots.filter (· ≤ x)).card : ℤ) -
+          (f.roots.filter (· ≤ x)).card ≤ 2 := by
+  have hMcard : f.roots.card = f.natDegree := card_roots_of_splits hf
+  have hNcard : g.roots.card = f.natDegree + 1 := by
+    rw [card_roots_of_splits hg, hdeg]
+  exact count_le_two_of_succRootCrossing hMcard hNcard hcross
+
 /-- Root-count bridge from the upper-threshold formulation to the succ-degree
 root-crossing target. -/
 theorem succDegreeRootCrossing_of_rootCountAbove

RealRooted/CommonInterleaverSeq.lean

@@ -80,6 +80,20 @@ lemma rootSeqDesc_eq_reverse_of_pairwise
   · grind
   · exact Multiset.coe_eq_coe.mp (by simp [rootSeqDesc, hrs_eq, Multiset.sort_eq])
 
+/-- The canonical descending root sequence is the roots sorted in decreasing order. -/
+lemma rootSeqDesc_eq_sort_ge (f : ℝ[X]) :
+    rootSeqDesc f = f.roots.sort (· ≥ ·) := by
+  have hpair :
+      ((f.roots.sort (· ≥ ·)).reverse).Pairwise (· ≤ ·) := by
+    simpa using
+      (Multiset.pairwise_sort (s := f.roots) (r := (· ≥ ·))).reverse
+  have hroots :
+      (↑((f.roots.sort (· ≥ ·)).reverse) : Multiset ℝ) = f.roots := by
+    simp [Multiset.sort_eq]
+  simpa using
+    (rootSeqDesc_eq_reverse_of_pairwise (f := f)
+      (rs := (f.roots.sort (· ≥ ·)).reverse) hpair hroots)
+
 /-- The `j`th Chudnovsky--Seymour interval attached to a descending root
 sequence `rs = [r₁, ..., r_d]`.
 

RealRooted/Compatibility/Basic.lean

@@ -106,6 +106,22 @@ lemma derivative {f g : ℝ[X]} (h : Compatible f g) :
   · rw [hcomb]
     exact derivative_eq_zero_or_ne_zero_and_splits hrr.2
 
+/-- Compatibility is preserved by the degree-preserving root regularizer
+`iterateTDeriv` at every positive shift. -/
+lemma iterateTDeriv {f g : ℝ[X]} (h : Compatible f g)
+    {eps : ℝ} (heps : 0 < eps) (n : ℕ) :
+    Compatible (RealRooted.iterateTDeriv eps n f)
+      (RealRooted.iterateTDeriv eps n g) := by
+  intro α β hα hβ
+  rcases h α β hα hβ with hzero | hrr
+  · left
+    rw [← RealRooted.iterateTDeriv_linear_combo, hzero]
+    simp
+  · right
+    rw [← RealRooted.iterateTDeriv_linear_combo]
+    exact ⟨RealRooted.iterateTDeriv_ne_zero hrr.1,
+      RealRooted.splits_iterateTDeriv heps hrr.2⟩
+
 lemma isRealRooted_left
     {f g : ℝ[X]} (h : Compatible f g)
     (hf_pos : HasPosLeadingCoeff f) : (f ≠ 0 ∧ f.Splits) := by

RealRooted/DegreeDropReversal.lean

@@ -296,6 +296,15 @@ theorem splits_reflect_iff {p : K[X]} {N : ℕ} (hN : p.natDegree ≤ N) :
     Polynomial.natDegree_reflect_le.trans <| by simp_all
   simpa using splits_reflect_of_splits h hreflect_deg
 
+/-- Reflection sends a nonzero root to its inverse at any valid degree bound. -/
+theorem isRoot_reflect_inv_iff {p : K[X]} {b : K} (hb : b ≠ 0)
+    {N : ℕ} (hN : p.natDegree ≤ N) :
+    (reflect N p).IsRoot b⁻¹ ↔ p.IsRoot b := by
+  letI : Invertible b := invertibleOfNonzero hb
+  change eval b⁻¹ (reflect N p) = 0 ↔ eval b p = 0
+  simpa [Polynomial.eval₂_id, invOf_eq_inv] using
+    (Polynomial.eval₂_reflect_eq_zero_iff (RingHom.id K) b N p hN)
+
 /-- Reversal preserves and reflects splitting over a field. -/
 theorem splits_reverse_iff {p : K[X]} :
     p.reverse.Splits ↔ p.Splits := by
@@ -526,6 +535,26 @@ theorem card_roots_reverse_Ioi {p : K[X]} (hp : p.Splits) (h0 : p.coeff 0 ≠ 0)
     congrArg Multiset.card
     (Multiset.filter_congr (fun r _ => mem_Ioi_inv_iff ha))
 
+/-- Half-line root-count transport under reflection at a degree bound. -/
+theorem card_roots_reflect_Ioi {p : K[X]} (hp : p.Splits) (h0 : p.coeff 0 ≠ 0)
+    {N : ℕ} (hN : p.natDegree ≤ N) {a : K} (ha : 0 < a) :
+    ((reflect N p).roots.filter (fun x => a < x)).card =
+      (p.roots.filter (fun r => 0 < r ∧ r < a⁻¹)).card := by
+  have hpad :
+      Multiset.filter (fun x => a < x)
+        ((N - p.natDegree) • ({0} : Multiset K)) = 0 := by
+    rw [Multiset.filter_eq_nil]
+    intro x hx
+    rw [Multiset.mem_nsmul, Multiset.mem_singleton] at hx
+    grind
+  rw [reflect_eq_X_pow_mul_reverse p hN,
+    Polynomial.roots_mul
+      (mul_ne_zero (pow_ne_zero _ Polynomial.X_ne_zero)
+        (reverse_ne_zero_of_coeff_zero_ne h0)),
+    Multiset.filter_add, Multiset.card_add, Polynomial.roots_pow,
+    Polynomial.roots_X, card_roots_reverse_Ioi hp h0 ha, hpad,
+    Multiset.card_zero, zero_add]
+
 /-- No-gap emptiness on a positive interval under reversal. -/
 theorem card_roots_reverse_Ioo_eq_zero_iff {p : K[X]} (hp : p.Splits)
     (h0 : p.coeff 0 ≠ 0) {a b : K} (ha : 0 < a) (hb : 0 < b) :

RealRooted/Derivative.lean

@@ -638,6 +638,69 @@ lemma mkInterleaving_sub_multiset (f : ℝ[X])
       · -- a ≠ s, a ≠ r₁
         grind
 
+/-- The recursively selected witness is the penultimate entry of `ss`.
+The product statement permits repeated entries and endpoint equality. -/
+private lemma exists_penultimate_listInterlaces_prod_nonneg :
+    ∀ {ss rs : List ℝ},
+      ss.Pairwise (· ≤ ·) →
+      ListInterlaces ss rs →
+      2 ≤ ss.length →
+      ∃ c ∈ ss, 0 ≤ (rs.map (c - ·)).prod := by
+  intro ss
+  induction ss with
+  | nil =>
+      intro rs _ _ hlen
+      simp at hlen
+  | cons s ss ih =>
+      cases ss with
+      | nil =>
+          intro rs _ _ hlen
+          simp at hlen
+      | cons t ts =>
+          intro rs hss hint _
+          cases rs with
+          | nil =>
+              simp [ListInterlaces] at hint
+          | cons r₁ rs =>
+              cases rs with
+              | nil =>
+                  simp [ListInterlaces] at hint
+              | cons r₂ rest =>
+                  obtain ⟨hr₁s, hsr₂, htail⟩ := hint
+                  by_cases hts : ts = []
+                  · subst ts
+                    have hrest_len : rest.length = 1 := by
+                      simpa using
+                        (listInterlaces_cons_length_eq htail).symm
+                    obtain ⟨r₃, rfl⟩ :=
+                      List.length_eq_one_iff.mp hrest_len
+                    change r₂ ≤ t ∧ t ≤ r₃ ∧ True at htail
+                    obtain ⟨hr₂t, htr₃, _⟩ := htail
+                    refine ⟨s, by simp, ?_⟩
+                    have h₁ : 0 ≤ s - r₁ :=
+                      sub_nonneg.mpr hr₁s
+                    have h₂ : s - r₂ ≤ 0 :=
+                      sub_nonpos.mpr hsr₂
+                    have h₃ : s - r₃ ≤ 0 :=
+                      sub_nonpos.mpr
+                        (hsr₂.trans (hr₂t.trans htr₃))
+                    simpa [mul_assoc] using
+                      mul_nonneg h₁
+                        (mul_nonneg_of_nonpos_of_nonpos h₂ h₃)
+                  · have htail_len : 2 ≤ (t :: ts).length := by
+                      grind
+                    have hss_cons := List.pairwise_cons.mp hss
+                    obtain ⟨c, hc, hcprod⟩ :=
+                      ih hss_cons.2 htail htail_len
+                    have hsc : s ≤ c :=
+                      hss_cons.1 c hc
+                    have hr₁c : r₁ ≤ c :=
+                      hr₁s.trans hsc
+                    refine
+                      ⟨c, List.mem_cons_of_mem s hc, ?_⟩
+                    simpa [List.map, List.prod_cons] using
+                      mul_nonneg (sub_nonneg.mpr hr₁c) hcprod
+
 /-! ## Main theorem -/
 
 /-- **Derivative interlacing**: if `f` is real-rooted of degree ≥ 2,
@@ -687,6 +750,40 @@ theorem derivative_interlaces {f : ℝ[X]} (hf : f.Splits) (hdeg : 2 ≤ f.natDe
   exact ⟨⟨by rintro rfl; simp at hf'_ne, hf⟩, hf'_rr, by rw [f.natDegree_derivative]; lia,
     rs, ss, hrs_sorted, hss_sorted, hrs_multiset, hss_eq, hss_interlaces⟩
 
+/-- A positive-leading splitting polynomial of degree at least four is
+nonnegative at the penultimate derivative-root occurrence.
+
+Repeated roots are retained: if the selected derivative root is also a root
+of `p`, the conclusion is equality. -/
+theorem exists_derivative_root_eval_nonneg_of_four_le_natDegree
+    {p : ℝ[X]} (hp : p.Splits) (hp_pos : HasPosLeadingCoeff p)
+    (hdeg : 4 ≤ p.natDegree) :
+    ∃ c ∈ p.derivative.roots, 0 ≤ p.eval c := by
+  obtain
+      ⟨_, hpd, _, rs, ss, _, hss_sorted, hrs_eq, hss_eq, hint⟩ :=
+    derivative_interlaces hp (by lia)
+  have hss_length : ss.length = p.derivative.natDegree := by
+    calc
+      ss.length = (↑ss : Multiset ℝ).card := by simp
+      _ = p.derivative.roots.card := congrArg Multiset.card hss_eq
+      _ = p.derivative.natDegree := card_roots_of_splits hpd.2
+  have hss_two : 2 ≤ ss.length := by
+    rw [hss_length, p.natDegree_derivative]
+    lia
+  obtain ⟨c, hc, hcprod⟩ :=
+    exists_penultimate_listInterlaces_prod_nonneg
+      hss_sorted hint hss_two
+  have hc_roots : c ∈ p.derivative.roots := by
+    rw [← hss_eq]
+    exact Multiset.mem_coe.mpr hc
+  refine ⟨c, hc_roots, ?_⟩
+  have heval :
+      p.eval c = p.leadingCoeff * (rs.map (c - ·)).prod := by
+    rw [hp.eval_eq_prod_roots c, ← hrs_eq]
+    rfl
+  rw [heval]
+  exact mul_nonneg hp_pos.le hcprod
+
 /-- A nonzero degree-zero real-rooted polynomial precedes a nonzero
 degree-one real-rooted polynomial. -/
 lemma prec_degree_zero_right_of_degree_one

RealRooted/DerivativeShiftRootMatching.lean

@@ -0,0 +1,60 @@
+import RealRooted.IteratedDerivativeShift
+import RealRooted.RootMultiplicityMatching
+import RealRooted.SameDegreeMultiplicityLowerCount
+
+/-!
+# Root matching for derivative shifts
+
+This module combines coefficient continuity of `TDeriv` with the
+multiplicity-aware finite matching API. It provides the root transport needed
+when derivative shifts are used to regularize a compatible polynomial pair.
+-/
+
+open Polynomial
+
+noncomputable section
+
+namespace RealRooted
+
+/-- For every positive radius, all roots of a sufficiently small positive
+`TDeriv` shift can be matched, with multiplicity, to roots of the original
+splitting polynomial within that radius. -/
+theorem exists_delta_roots_rel_TDeriv
+    {p : ℝ[X]} (hp : p.Splits) {ρ : ℝ} (hρ : 0 < ρ) :
+    ∃ δ > 0, ∀ ⦃eps : ℝ⦄, 0 < eps → eps < δ →
+      Multiset.Rel (fun r q ↦ |q - r| < ρ) p.roots (TDeriv eps p).roots := by
+  obtain ⟨η, hη_pos, hηρ, hsep⟩ :=
+    Multiset.exists_pos_lt_and_two_mul_le_abs_sub_toFinset p.roots hρ
+  have hshift (nu : ℝ) :
+      p + C nu * (-p.derivative) = TDeriv nu p := by
+    simp only [TDeriv, sub_eq_add_neg, mul_neg]
+  have hp0 : (p + C (0 : ℝ) * (-p.derivative)).Splits := by
+    simpa using hp
+  obtain ⟨δ, hδ_pos, hlocal⟩ :=
+    exists_eps_forall_root_count_le_card_filter_near
+      (f := p) (g := -p.derivative) (μ0 := 0) hp0 η hη_pos
+  refine ⟨δ, hδ_pos, ?_⟩
+  intro eps heps_pos hepsδ
+  have heps_abs : |eps - 0| < δ := by
+    simpa [abs_of_pos heps_pos] using hepsδ
+  have hsplit : (p + C eps * (-p.derivative)).Splits := by
+    rw [hshift]
+    exact splits_tderiv heps_pos hp
+  have hdeg :
+      (p + C eps * (-p.derivative)).natDegree =
+        (p + C (0 : ℝ) * (-p.derivative)).natDegree := by
+    rw [hshift eps, hshift 0, natDegree_TDeriv, natDegree_TDeriv]
+  have hcount := hlocal eps heps_abs hsplit hdeg
+  rw [hshift eps, hshift 0] at hcount
+  have hcount' : ∀ a ∈ p.roots.toFinset,
+      p.roots.count a ≤
+        ((TDeriv eps p).roots.filter (fun q ↦ |q - a| < η)).card := by
+    simpa [TDeriv] using hcount
+  have hcard : (TDeriv eps p).roots.card = p.roots.card := by
+    rw [card_roots_of_splits (splits_tderiv heps_pos hp), natDegree_TDeriv,
+      card_roots_of_splits hp]
+  have hrel :=
+    Multiset.rel_of_forall_le_count_of_card_eq hsep hcount' hcard
+  exact hrel.mono fun _ _ _ _ hclose ↦ lt_trans hclose hηρ
+
+end RealRooted