Liu: state x-subtraction, quartic boundary and root-order lemmas directly (part 2)

ARCHITECTURE.md

@@ -632,18 +632,15 @@ and its elementary endpoint consequences. The
 root-count transport first, then the finite-gap invariant, then the left/right
 Theorem 2.1 branch predicate. `Theorem21Statements.CommonRootDeletion` owns the
 independent shared-factor reduction, and `Theorem21Statements.Interfaces`
-combines the two branches into the theorem-shaped targets and implication
-wrappers. The historical `Theorem21Statements` path remains a compatibility
+keeps only the refuted published forward direction beside its checked
+negation. The historical `Theorem21Statements` path remains a compatibility
 facade, and consumers needing only the predicate import `NoCommonRoots`
 directly.
 
-`LiuOppositeSigns.FactorReturnAssembly` is a compatibility facade over the
-factor-return theorem route. `LeftDegreeCases` owns the translated and
-x-subtraction realizations of the three left deletion branches;
-`RightDegreeCases` obtains the symmetric right branches and their endpoint
-specializations; `PredicateDegreeCases` combines both orientations under
-lower-endpoint predicates; and `DegreeCaseAssembly` packages the final six-case
-factor-return principle.
+`LiuOppositeSigns.FactorReturnAssembly` proves the reverse direction of
+Theorem 2.1. `FactorReturnLeft` and `FactorReturnTwoDegree` reduce the three
+degree cases of a left deletion branch to the positive-split x-subtraction
+pencils of `XSub.IntervalRootCount`; the right branch follows by symmetry.
 
 `LiuOppositeSigns.XSub.ProperPosition` is a narrow bridge from the ordinary
 positive-leading `StrictInterl` interface to Liu's positive root-count package. It
@@ -668,13 +665,12 @@ families in proof dependency order; and `Endpoints` derives the degree-three
 interface. The facade preserves the previous public import path.
 
 `LiuOppositeSigns.XSub.QuarticCubicBoundary` now exposes the analogous boundary
-dependency graph. `Statements` owns the six proposition-valued package
-interfaces; `RepeatedRight` proves the independent strict-left repeated-right
-branch; `QuarticSubQuadratic` owns the endpoint factor and right-only zero
-package; `RepeatedLeft` builds on that factor; `EndpointZero` combines the two
-completed boundary branches; and `Assembly` derives the normalized terminal.
-The 9-line facade preserves the former import path. The implementation units
-have 88, 434, 1,022, 707, 550, and 200 lines, respectively.
+dependency graph. `RepeatedRight` proves the independent strict-left
+repeated-right branch; `QuarticSubQuadratic` owns the endpoint factor and
+right-only zero case; `RepeatedLeft` builds on that factor; `EndpointZero`
+combines the two endpoint-zero cases; and `Assembly` proves the normalized
+quartic/cubic splitting theorem. The 9-line facade preserves the former import
+path.
 
 The Cayley-transform extraction is entirely Mathlib-shaped:
 

RealRooted.lean

@@ -538,17 +538,11 @@ 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.FactorReturnAssembly.DegreeCaseAssembly
-import RealRooted.LiuOppositeSigns.FactorReturnAssembly.LeftDegreeCases
-import RealRooted.LiuOppositeSigns.FactorReturnAssembly.PredicateDegreeCases
-import RealRooted.LiuOppositeSigns.FactorReturnAssembly.RightDegreeCases
 import RealRooted.LiuOppositeSigns.FactorReturnLeft
-import RealRooted.LiuOppositeSigns.FactorReturnStatements
 import RealRooted.LiuOppositeSigns.FactorReturnTwoDegree
 import RealRooted.LiuOppositeSigns.ForwardCubicLinear
 import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.Average
@@ -571,7 +565,6 @@ import RealRooted.LiuOppositeSigns.RootCount
 import RealRooted.LiuOppositeSigns.RootCountClosure
 import RealRooted.LiuOppositeSigns.RootCountRelStability
 import RealRooted.LiuOppositeSigns.RootDeletion
-import RealRooted.LiuOppositeSigns.Theorem21Assembly
 import RealRooted.LiuOppositeSigns.Theorem21Statements
 import RealRooted.LiuOppositeSigns.Theorem21Statements.CommonRootDeletion
 import RealRooted.LiuOppositeSigns.Theorem21Statements.Interfaces
@@ -611,7 +604,6 @@ import RealRooted.LiuOppositeSigns.XSub.QuarticCubicBoundary.EndpointZero
 import RealRooted.LiuOppositeSigns.XSub.QuarticCubicBoundary.QuarticSubQuadratic
 import RealRooted.LiuOppositeSigns.XSub.QuarticCubicBoundary.RepeatedLeft
 import RealRooted.LiuOppositeSigns.XSub.QuarticCubicBoundary.RepeatedRight
-import RealRooted.LiuOppositeSigns.XSub.QuarticCubicBoundary.Statements
 import RealRooted.LiuOppositeSigns.XSub.QuarticCubicCommonRoot
 import RealRooted.LiuOppositeSigns.XSub.SameDegree
 import RealRooted.LiuOppositeSigns.XSub.SplittingTools

RealRooted/Challenges/LiuOppositeSigns.lean

@@ -132,7 +132,7 @@ theorem compatible_iff_rootCount_of_noCommonRoots {f g : ℝ[X]} (hf : f.Splits)
     (hf_deg : f.natDegree ≠ 0) (hg_deg : g.natDegree ≠ 0) :
     Compatible f g ↔
       ∃ r s, LeftRootCountBranch f g r s ∨ RightRootCountBranch f g r s :=
-  theorem21CompatibleRootCountNoCommonNonconstant f g hf hg hsgn hno hf_deg hg_deg
+  theorem21CompatibleRootCountNoCommonNonconstant hf hg hsgn hno hf_deg hg_deg
 
 /-- Without the common-root branch, the forward direction fails (for `X` and
 `-X ^ 2`). -/
@@ -147,7 +147,7 @@ differing by at most two. -/
 theorem natDegree_diff_le_two {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits)
     (hsgn : OppositeLeadingSigns f g) (hcompat : Compatible f g) :
     |((f.natDegree : ℤ) - (g.natDegree : ℤ))| ≤ 2 :=
-  corollary22DegreeDiff_proof f g hf hg hsgn hcompat
+  corollary22DegreeDiff hf hg hsgn hcompat
 
 end LiuOppositeSigns
 end Challenges

RealRooted/LiuOppositeSigns/CommonInterleaverConsequences.lean

@@ -1,11 +1,11 @@
 import RealRooted.CommonInterleaverTwo
-import RealRooted.LiuOppositeSigns.Corollary22
+import RealRooted.LiuOppositeSigns.ForwardLowDegree
 
 /-!
 # Liu common-interleaver consequences
 
 This module contains the positive-deletion and branch-retaining
-common-interleaver consequences derived from Liu Theorem 2.1 packages.
+common-interleaver consequences of Liu's root-count branches.
 -/
 
 open Polynomial
@@ -59,137 +59,5 @@ theorem theorem21PositiveDeletionCompatibleBranches_of_theorem21RootCountBranche
     hsgn (theorem21DeletionPairCommonInterleaverBranches_of_theorem21RootCountBranches
       hf_splits hg_splits hsgn h)
 
-/-- Projection form of the isolated branch-retaining deletion-pair
-common-interleaver forward direction. -/
-theorem theorem21DeletionPairCommonInterleaverBranches_of_compatible_of_commonForward
-    (hforward : theorem21CompatibleToDeletionPairCommonInterleaverBranchesStatement)
-    {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits)
-    (hsgn : OppositeLeadingSigns f g) (hcompat : Compatible f g) :
-    theorem21DeletionPairCommonInterleaverBranches f g :=
-  hforward hf hg hsgn hcompat
-
-/-- The isolated branch-retaining deletion-pair common-interleaver forward
-direction supplies normalized deletion compatibility branches. -/
-theorem theorem21PositiveDeletionCompatibleBranches_of_compatible_of_commonForward
-    (hforward : theorem21CompatibleToDeletionPairCommonInterleaverBranchesStatement)
-    {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits)
-    (hsgn : OppositeLeadingSigns f g) (hcompat : Compatible f g) :
-    theorem21PositiveDeletionCompatibleBranches f g :=
-  theorem21PositiveDeletionCompatibleBranches_of_deletionPairCommonInterleaverBranches
-    hsgn
-    (theorem21DeletionPairCommonInterleaverBranches_of_compatible_of_commonForward
-      hforward hf hg hsgn hcompat)
-
-/-- The isolated forward direction of Liu Theorem 2.1 supplies normalized
-deletion compatibility branches. -/
-theorem theorem21PositiveDeletionCompatibleBranches_of_compatible_of_forward
-    (hforward : theorem21CompatibleToRootCountBranchesStatement)
-    {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits)
-    (hsgn : OppositeLeadingSigns f g) (hcompat : Compatible f g) :
-    theorem21PositiveDeletionCompatibleBranches f g :=
-  theorem21PositiveDeletionCompatibleBranches_of_compatible_of_commonForward
-    (theorem21CompatibleToDeletionPairCommonInterleaverBranches_of_forward
-      hforward)
-    hf hg hsgn hcompat
-
-/-- The forward direction of Liu Theorem 2.1 supplies normalized deletion
-compatibility branches. -/
-theorem theorem21PositiveDeletionCompatibleBranches_of_compatible
-    (h : theorem21CompatibleRootCountStatement) {f g : ℝ[X]}
-    (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g)
-    (hcompat : Compatible f g) :
-    theorem21PositiveDeletionCompatibleBranches f g :=
-  theorem21PositiveDeletionCompatibleBranches_of_compatible_of_forward
-    (theorem21CompatibleToRootCountBranches_of_theorem21CompatibleRootCount h)
-    hf hg hsgn hcompat
-
-/-- The isolated forward direction of Liu Theorem 2.1 supplies
-branch-retaining common interleaver witnesses for the actual deletion pair. -/
-theorem theorem21DeletionPairCommonInterleaverBranches_of_compatible_of_forward
-    (hforward : theorem21CompatibleToRootCountBranchesStatement)
-    {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits)
-    (hsgn : OppositeLeadingSigns f g) (hcompat : Compatible f g) :
-    theorem21DeletionPairCommonInterleaverBranches f g :=
-  theorem21DeletionPairCommonInterleaverBranches_of_compatible_of_commonForward
-    (theorem21CompatibleToDeletionPairCommonInterleaverBranches_of_forward
-      hforward)
-    hf hg hsgn hcompat
-
-/-- The forward direction of Liu Theorem 2.1 supplies branch-retaining common
-interleaver witnesses for the actual deletion pair. -/
-theorem theorem21DeletionPairCommonInterleaverBranches_of_compatible
-    (h : theorem21CompatibleRootCountStatement) {f g : ℝ[X]}
-    (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g)
-    (hcompat : Compatible f g) :
-    theorem21DeletionPairCommonInterleaverBranches f g :=
-  theorem21DeletionPairCommonInterleaverBranches_of_compatible_of_forward
-    (theorem21CompatibleToRootCountBranches_of_theorem21CompatibleRootCount h)
-    hf hg hsgn hcompat
-
-/-- Liu Theorem 2.1, restated with branch-retaining deletion-pair
-common-interleaver witnesses. -/
-theorem compatible_iff_theorem21DeletionPairCommonInterleaverBranches
-    (h : theorem21CompatibleRootCountStatement) {f g : ℝ[X]}
-    (hf : f.Splits) (hg : g.Splits) (hsgn : OppositeLeadingSigns f g) :
-    Compatible f g ↔ theorem21DeletionPairCommonInterleaverBranches f g :=
-  (theorem21DeletionPairCommonInterleaverIff_of_theorem21CompatibleRootCount
-    h) f g hf hg hsgn
-
-/-- The two positive-split root-count leaves supply the existing
-positive-leading compatibility-to-common-interleaver bridge. -/
-theorem
-    compatiblePairHasCommonInterleaver_of_positiveSplitRootCountAboveNonRoot
-    (hsame : positiveSplitSameDegreeRootCountAboveNonRootStatement)
-    (hsucc : positiveSplitSuccDegreeRootCountAboveNonRootStatement) :
-    CompatiblePairHasCommonInterleaverStatement := by
-  refine compatiblePairHasCommonInterleaver_of_pairDegreeSplit_via_nonnegShift
-    ?hsame ?hsucc
-  · intro f g hf_pos hg_pos hfnn hgnn hfg hdeg hno
-    exact (hsame hf_pos hg_pos hfnn hgnn hfg hdeg hno)
-      |>.pairHasCommonInterleaver_of_sameDegree hdeg
-  · intro f g hf_pos hg_pos hfnn hgnn hfg hdeg hno
-    have hf_split : f.Splits :=
-      PosComboSuccDegreeLeftSplitsNonnegStatement_of_rootContinuity
-        hf_pos hg_pos hfnn hgnn hfg hdeg
-    exact (hsucc hf_pos hg_pos hfnn hgnn hfg hdeg hno hf_split)
-      |>.pairHasCommonInterleaver_of_succDegree hdeg
-
-/-- The checked same-degree analytic count spine and the succ-degree
-common-left-interleaver reduction supply the compatible-pair endpoint. -/
-theorem
-    compatiblePairHasCommonInterleaver_of_sameDegreeAnalytic_and_succCommonLeftInterleaver
-    (hsucc : PosComboNoCommonSuccDegreeCommonLeftInterleaverNonnegStatement) :
-    CompatiblePairHasCommonInterleaverStatement :=
-  compatiblePairHasCommonInterleaver_of_rootCountAboveBothNonRoot
-    _root_.RealRooted.posComboNoCommonSameDegreeRootCountAboveNonRootNonneg_from_analytic
-    (posComboNoCommonSuccDegreeRootCountAboveNonRoot_of_commonLeftInterleaver
-      hsucc)
-
-/-- Finite-family Chudnovsky--Seymour package from the Liu-side
-positive-split root-count leaves. -/
-theorem chudnovskySeymour_fourWay_of_positiveSplitRootCountAboveNonRoot
-    {fs : List ℝ[X]}
-    (hrr : ∀ f ∈ fs, (f ≠ 0 ∧ f.Splits))
-    (hpos : ∀ f ∈ fs, HasPosLeadingCoeff f)
-    (hsame : positiveSplitSameDegreeRootCountAboveNonRootStatement)
-    (hsucc : positiveSplitSuccDegreeRootCountAboveNonRootStatement) :
-    ChudnovskySeymourFourWayPackage fs :=
-  chudnovskySeymour_fourWay_of_pairBridgePos (fs := fs) hrr hpos
-    (compatiblePairHasCommonInterleaver_of_positiveSplitRootCountAboveNonRoot
-      hsame hsucc)
-
-/-- Finite-family Chudnovsky--Seymour package from the checked same-degree
-analytic spine and the succ-degree common-left-interleaver reduction. -/
-theorem
-    chudnovskySeymour_fourWay_of_sameDegreeAnalytic_and_succCommonLeftInterleaver
-    {fs : List ℝ[X]}
-    (hrr : ∀ f ∈ fs, (f ≠ 0 ∧ f.Splits))
-    (hpos : ∀ f ∈ fs, HasPosLeadingCoeff f)
-    (hsucc : PosComboNoCommonSuccDegreeCommonLeftInterleaverNonnegStatement) :
-    ChudnovskySeymourFourWayPackage fs :=
-  chudnovskySeymour_fourWay_of_pairBridgePos (fs := fs) hrr hpos
-    (compatiblePairHasCommonInterleaver_of_sameDegreeAnalytic_and_succCommonLeftInterleaver
-      hsucc)
-
 end LiuOppositeSigns
 end RealRooted