interval: extract the generic proof frontend

[kim-em]

Summary

• quote arbitrary engine chronology in a Mathlib-free fact-polymorphic module
• fold instance, rule, and transport events through a generic versioned evidence table
• parameterize proof emission by semantics/domain constants and a plain-data encoder
• route the live Real.sin tactic and repeated-instantiation tests through the extracted fold
• reject stale rule versions and remove a duplicate transport mutation

Verification

• Build completed successfully (1960 jobs).
• copyright, line-count, DAG, release-manifest, trust-surface, Phase 4, conformance-target, diff, and factor-freshness checks

Stacked on #9207.