feat(interval): prove a mixed sine-exp tactic path

[kim-em]

Summary

• add independently registered Mathlib-free source, sine, and exponential runtime packages over one shared fact domain
• add package-owned Real semantics and replay schemas for sine range and exponential upper-bound propagation
• reify Real.exp (Real.sin x) recursively through the generic goal registry and kernel-replay sine then exp through the generic proof frontend
• prove the ordinary theorem Real.exp (Real.sin x) ≤ 3 with an exact guarded axiom report

Non-vacuity

The exponential runtime rule is inapplicable until sine installs the exact [-1,1] fact. Its replay theorem consumes that exact fact, while mutations reject wrong schema, source node, or dependency chronology. Generic scheduler, reifier, quotation, ProofFrontend, and GoalClosure remain function-agnostic.

Scope

This demonstrates recursive structural discovery, not dynamic auxiliary-expression instantiation. Packages in one run currently share a fact representation and aligned operation/meaning/proof-package slots; the SPEC records these limitations.

Validation

• focused mixed-function, sine/exp frontend, policy/controller, exact-branch, subtraction, nested-branch, and complete LogTables conformance build
• trust surface, factor freshness, PNT source inventory, diff, and banned-proof checks