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

[PerAlexandersson]

Part 2 of the Liu cluster wrapper cleanup. It is stacked on #1096; retarget to main once that merges. After this PR, the only …Statement left in RealRooted/LiuOppositeSigns/** is the refuted published forward direction, kept beside its negation.

Deleted (63 declarations)

• 20 …Statement defs: xSub{CubicCubic,CubicQuadratic,QuadraticCubic,QuadraticQuadratic,QuarticCubic,LinearQuadratic}Splits, the two discriminant certificates, quarticSubQuadraticSplits, the seven quartic/cubic boundary packages (and the now-empty module XSub/QuarticCubicBoundary/Statements), CompatibleCubic{Linear,Pair}RootOrder, and positiveSplit{Same,Succ}DegreeRootCountAboveNonRoot.
• 37 conditional lemmas:
  • 30 …_of_monic / …_of_cubicDiscrim / …_of_cubicLinearRootOrder / …_of_cubicPairRootOrder / …_of_packages lemmas. Each body was merged into the existing unconditional lemma of the same name without the suffix, so signatures and call sites are unchanged.
  • The redundant alternative quartic assembly routes.
  • The (3,2)∨(2,3) composition package.
• Conditional routes to results that are already proved unconditionally. They took the open CommonInterleaver succ-degree statements:
  • compatiblePairHasCommonInterleaver_of_{positiveSplitRootCountAboveNonRoot,sameDegreeAnalytic_and_succCommonLeftInterleaver} and chudnovskySeymour_fourWay_of_…, superseded by chudnovskySeymour_compatiblePairHasCommonInterleaver;
  • RootCountCompatible.of_compatible_of_succDegreeRootCountAboveNonRoot and its helper, superseded by RootCountCompatible.of_compatible;
  • positiveSplitSuccDegreeRootCountAboveNonRoot_of_rootCountAboveNonRoot.

Restated with explicit binders (binder order and implicitness follow the old statement, so applied call sites are unchanged)

• xSubCubicCubicSplits, xSubCubicQuadraticSplits, xSubQuadraticCubicSplits, xSubQuadraticQuadraticSplits, xSubQuarticCubicSplits, xSubLinearQuadraticSplits (merged with its discriminant reduction), xSubLinearQuadraticDiscrimNonneg, xSubQuadraticLinearCubicDiscrimNonneg, quarticSubQuadraticSplits.
• xSubQuarticCubic{StrictLeftRepeatedRight,RepeatedLeft,RepeatedRight,LeftOnlyEndpointZero,RightOnlyEndpointZero,EndpointZero,SideBoundary}BoundaryCases.
• compatibleCubicLinearRootOrder and compatibleCubicPairRootOrder. The (3,2)/(2,3) forward cases move next to the latter as theorem21RootCountBranches_of_compatible_natDegree_{three_two,two_three}.
• positiveSplitSameDegreeRootCountAboveNonRoot, instantiated with the proved analytic same-degree count.
• Renamed: splits_X_mul_sub_C_mul_of_positiveSplit_natDegree_two_one_of_cubicDiscrim is now …_two_one. Its hypothesis is proved.

Kept

• theorem21CompatibleToRootCountBranchesNonconstantStatement, with its checked negation (see PROOF_STATUS.md).
• No proofs-repo, tactic or catalog names were touched.

🤖 Generated with Claude Code