Split root-count tactic into theorem and frontend layers

[PerAlexandersson]

Summary

• replace the 3,226-line Tactic.RootCount mixed module with a compatibility
  facade over six theorem, syntax, and macro-rule layers
• expose parser-free SequenceCore and LowDegree theorem APIs while
  preserving all 191 established theorem/syntax declarations and all 124
  tactic spellings
• simplify the degree-at-most-three endpoint with
  Nat.le_or_eq_of_le_succ, removing the negated case split and lia
• document the boundary and guard every new layer's import closure

Dependency effect

• SequenceCore: 83 modules / 30,789 local lines
• old facade baseline: 138 modules / 62,863 local lines
• parser-free LowDegree: 136 modules / 59,977 local lines
• the compatibility facade remains available to all existing tactic users

Verification

• focused builds of all six layers, the facade, Tactic, Tactic.OEIS, and
  Tactic.Examples.RootCount
• full lake-workspace build RealRooted: 9,401 jobs passed
• all 124 tactic spellings occur in the compiled root-count example suite
• import-architecture self-test and live check
• root-import completeness: all 842 source modules imported
• proof-status self-test and live check
• exact 191-declaration stream comparison against the pre-split source
• five representative axiom audits: only propext, Classical.choice, and
  Quot.sound
• changed-file width and git diff --check

Aristotle

Owner-labeled advisory project a081360c-f706-4531-b949-b6b47fb79f66, task
84b3da16-38b1-4220-b56c-3b897e957855, is independently proof-golfing the
low-degree endpoint against public merge 5d2ad085. It is intentionally not a
merge gate; any worthwhile result will require a separate local replay and
follow-up checkpoint.