CommonInterleaver: state the Chudnovsky–Seymour pair chain directly (part 2)

[PerAlexandersson]

Part 2 of the CommonInterleaver cleanup. This PR builds on #1098, so its diff includes that commit until #1098 merges. Review only the last commit.

The live proof chain behind the two-polynomial Chudnovsky–Seymour theorem now uses explicit per-pair theorems and no statement wrappers.

Deleted

• 14 …Statement defs from the live chain:
  • same/succ-degree pair endpoints (PosComboNoCommon{Same,Succ}DegreePairHasCommonInterleaverNonnegStatement)
  • …SlotData…, …RootCrossing… and …RootCountAbove… (same and succ)
  • PosComboSuccDegreeLeftSplitsNonnegStatement
  • PosComboNoCommonSuccDegreeRootCountNonRootNonnegStatement
  • CompatibleSuccDegreeRootCountAboveNoGapTwoStatement
  • CompatibleSuccDegreeClosedSegment{NoGapTwo,CountEq}Statement
  • CompatiblePairHasCommonLeftInterleaverPosStatement
• The modules CommonInterleaver.Statements and ClosedSegmentCountEqFromAnalytic; the latter's proof moved into PairBridge/SuccDegree/ClosedSegment.
• About 60 statement-level reductions between those statements, the nonnegPairBridge scaffolding, chudnovskySeymour_fourWay_of_pairDegreeSplit_and_nonnegCoeffs and the duplicate compatiblePairHasCommonLeftInterleaver_chudnovskySeymour.
• chudnovskySeymour_fourWay_nonnegCoeffs (its nonnegativity hypothesis was unused). It is replaced by chudnovskySeymour_fourWay.
• 18 tactics and examples whose only job was to prove statement-typed goals. One orphan syntax declaration.

Restated or new (explicit binders)

• Same degree:
  • pairHasCommonInterleaver_of_sameDegree_rootCrossing
  • pairHasCommonInterleaver_of_sameDegree_rootCountAbove_nonRoot
  • pairHasCommonInterleaver_of_posCombo_sameDegree
• Successor degree:
  • Compatible.succDegree_card_roots_gt_eq_of_closedSegment
  • Compatible.succDegree_rootCountAbove_sub_ne_two
  • compatibleSuccDegree_rootCountAbove_diff_le_one_of_nonRoot
  • pairHasCommonInterleaver_of_posCombo_succDegree
• Assembly, with no hypotheses left:
  • pairHasCommonInterleaver_of_posCombo_noCommon_of_natDegree_close
  • CommonInterleaver.PairBridge.pairDegreeSplit_ordered
  • posComboPairHasCommonInterleaver_of_nonnegCoeffs
  • posComboPairHasCommonInterleaver_of_splits
  • chudnovskySeymour_compatiblePairHasCommonInterleaver (moved to NonnegativeShift, same name)
• Core:
  • chudnovskySeymour_compatiblePairHasCommonLeftInterleaver
  • chudnovskySeymour_fourWay
  • the family theorems, now proved through the four-way package
• The _of_pairBridgePos family reductions take the pair theorem as an unfolded ∀ hypothesis.

Kept, and why

• Used only by LiuOppositeSigns callers (another cluster). Docstrings say each is proved:
  • CompatiblePairHasCommonInterleaverStatement
  • PosComboNoCommon{Same,Succ}DegreeRootCountAboveNonRootNonnegStatement
  • CompatibleSuccDegreeRootCountAboveNonRootStatement
  • PosComboNoCommonSuccDegreeCommonLeftInterleaverNonnegStatement
• Liu-facing shims with unused hypotheses, kept so Liu still compiles:
  • compatiblePairHasCommonInterleaver_of_pairDegreeSplit_via_nonnegShift
  • compatiblePairHasCommonInterleaver_of_rootCountAboveBothNonRoot
  • posComboNoCommonSameDegreeRootCountAboveNonRootNonneg_from_analytic
  • PosComboSuccDegreeLeftSplitsNonnegStatement_of_rootContinuity: name kept and binders kept in the same order, because Liu calls it.
• Genuine reductions kept: chudnovskySeymour_fourWay_of_pairBridgePos (pair theorem to family, via the finite Helly upgrade; also used by Liu); the common-root peeling and nonnegative-shift reductions (…_of_natDegree_le_reduction…); the low-degree endpoints.
• CubicSecondRootBoundStatement and CubicInteriorTwo{Below,Above}Statement are consumed by Tactic/RootCount (another cluster). The interior ones follow trivially from cubicSecondRootBound_from_analytic.
• compatiblePairHasCommonInterleaver_chudnovskySeymour: the proofs repo uses it.

Import budgets go up by 6–7 modules for 9 PairBridge modules, because the closed-segment count proof now lives in ClosedSegment.

🤖 Generated with Claude Code