refactor: split common-interleaver tactic layers

[PerAlexandersson]

Summary

• split the 3,089-line common-interleaver tactic frontend into a theorem core, four syntax layers, and four matching rule layers behind the existing facade
• preserve all 191 established tactic spellings and their compiled example coverage
• narrow Tactic.OEIS to the basic common-interleaver rules it documents and add exact architecture budgets

Verification

• focused layer, facade, and Tactic.Examples.CommonInterleaver builds
• full lake-workspace build RealRooted (9,410 jobs)
• import architecture self/live, proof-status self/live, and root-import checks
• declaration-stream and tactic-coverage comparison; changed-file width and diff checks
• five representative axiom audits: only propext, Classical.choice, and Quot.sound