CommonInterleaver: delete dead Chudnovsky–Seymour reduction routes (part 1)

[PerAlexandersson]

Follows #1092 (Chudnovsky–Seymour headline restatement).

Chudnovsky–Seymour is fully proved, so most of the CommonInterleaver/Compatibility statement layer is either a dead alternative route or scaffolding of the finished proof. This PR (part 1) deletes the dead routes. The live proof chain (same-degree and successor-degree root-count, root-crossing and slot-data statements) is restated in a follow-up PR.

Deleted

• 38 …Statement defs no proof consumes. These include the refuted orientation and right-pencil shortcuts, the affine-family, boundary-right-pair, degree-close, all-combo-bridge, residual/lead/divX, closed-segment no-gap, endpoint-sign and cubic discriminant/not-splits leaves, the duplicate CompatiblePairHasCommonRightInterleaverStatement and the same/succ-degree compatible-pair statements.
• About 220 theorems conditional on those statements. Theorems whose hypothesis is refuted were vacuous.
• Conditional reductions between proved statements that had no callers. Examples are the _via_nonnegShift/_of_slotData/_of_rootCrossing family and four-way variants, the forward-ASW left-splits wrappers and the CS 3.4 derivative-induction wrappers.
• Statement aliases of proved theorems: Common(Left)InterleaverFamilyUpgradeStatement and its witnesses, which callers now replace with has(Common|CommonLeft)Interleaver_of_pairwise…; also StrictInterlLeftShiftedSlotStatement and CommonLeftInterleaverShiftedSlotStatement.
• 97 tactic syntaxes and macro rules that only dispatched to the deleted theorems, plus 95 tactic examples.

Restated

• rootSlotInterval_succ_inter_nonempty_of_commonLeftInterleaver: this is the old shifted-slot statement, now with explicit binders. pairwise_shiftedSlotIntersections_of_pairwiseHasCommonLeftInterleaver and hasCommonLeftInterleaverSeq_of_pairwiseHasCommonLeftInterleaver no longer take it as a hypothesis.
• Refuted statements: the checked counterexamples are kept as explicit negations in CommonInterleaverExamples:
  • not_forall_posCombo_succDegree_noCommon_strictInterl
  • not_forall_compatible_succDegree_negativeRightFamily_splits
  • not_forall_compatible_succDegree_allComboRealRooted
  • not_forall_posCombo_noCommon_strictInterl_or (re-attached to its existing private counterexample)
  • not_forall_posCombo_succDegree_noCommon_coeff_zero_strictInterl (re-attached to its existing private counterexample)

Kept, and why

• Statements consumed by LiuOppositeSigns, which is another cluster:
  • CompatiblePairHasCommonInterleaverStatement
  • PosComboNoCommonSuccDegreeCommonLeftInterleaverNonnegStatement
  • PosComboNoCommon{Same,Succ}DegreeRootCountAboveNonRootNonnegStatement
  • CompatibleSuccDegreeRootCountAboveNonRootStatement
  • the lemmas Liu calls
• CubicInteriorTwo{Below,Above}Statement, used by Tactic/RootCount. Both follow from cubicSecondRootBound_from_analytic.
• The live same/succ-degree chain statements (…SlotData…, …RootCrossing…, …RootCountAbove…, …ClosedSegmentCountEq…, …LeftSplits…, and the two pair endpoints). Part 2 restates these.

No catalog entries or proofs-repo names change.

🤖 Generated with Claude Code