Liu: state Theorem 2.1 directly, drop statement scaffolding (part 1)

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

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

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,82 +59,6 @@ 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