[PerAlexandersson]

Moves the core onto Mathlib's API and onto general lemmas, as the core-cleanup audit asked:
core modules should be Mathlib-clean, without duplicate lemmas, and should prefer general
arguments to special cases.

Mathlib API

• About 370 calls in 125 files now use Mathlib's own lemmas instead of local helpers:
  splits_iff_card_roots, Splits.eval_eq_prod_roots, Splits.mul/pow/derivative/
  iterate_derivative, Splits.of_dvd, IsRoot.dvd, Splits.exists_eval_eq_zero and
  Splits.mem_range_of_isRoot.
• natDegree_add_eq_{left,right}_of_natDegree_lt comes from Mathlib directly, so the
  positive-leading-coefficient hypothesis is gone.
• New shims in RealRooted/Mathlib/Algebra/Polynomial/Reverse.lean: Polynomial.Splits.reverse,
  .reflect, .X_pow_mul_reverse and .of_reverse, plus splits_reverse_iff and
  splits_reflect_iff.

General lemmas instead of special cases

• The StrictInterl.mul_X* variants follow from StrictInterl.mul_X_sub_C_both, which moved
  earlier in the import order.
• New hypothesis-free lemmas: StrictInterl.mul_X_sub_C_both_iff, Interl.mul_X_sub_C_both,
  Interl.of_mul_X_sub_C_both, Interl.mul_X_both, Interl.of_mul_X_both, Interl.theta,
  Interl.thetaPlusOne and Interl.iterateThetaPlusOne. Their predecessors carried
  nonnegativity or PF hypotheses that the proofs did not use.
• The quadratic splitting forms are derived from one discriminant criterion.
• Duplicates merged: pairwise_le_of_listInterlaces, hasNonnegCoeffs_C_mul (115 calls),
  Interl.toStrictInterl_of_ne, and the divX splitting lemma.
• 42 file-local helpers are now private.

Compatibility

• Names still used in oeis-proofs remain as @[deprecated … (since := "2026-10-21")] with
  their old signatures. Names with no downstream use were deleted.
• Tactics accept new certificate-minimal forms such as
  rr_strict_interl_mul_X_both using proper := h. The old forms still parse and are
  registered as @[tactic_alt].
• Fixes a bracketing bug in the product branch of rr_zero_or_splits.

Checks (local)

• Full default build passes, Tactic.Examples included.
• runLinter passes against the committed nolints.json, with the baseline unchanged.
• lake exe lint-style passes, along with all guards and the shim registry check.
• OEIS_COVERAGE.md is regenerated and passes --check.
• Catalog tests and the catalog axiom audit pass.

🤖 Generated with Claude Code