interval: validate the frontend with Real.exp

[kim-em]

Summary

• extract one shared Mathlib-free encoder for structural program and trace data
• add an independent exponential package with a distinct fact lattice
• contribute real exponential semantics and a package-owned replay theorem
• run the live rule through policy, joint registry, generic quotation, and generic proof emission
• prove the ordinary theorem 0 ≤ Real.exp x with the emitted evidence

Verification

• lake build HexInterval.Experiment.FrontendEncoder HexInterval.Experiment.ExpSign HexIntervalMathlib.Experiment.ExpSign HexIntervalMathlib.ExpSignConformance HexIntervalMathlib.SineTacticConformance
• copyright, line-count, DAG, release-manifest, trust-surface, Phase 4, conformance-target, diff, banned-proof, and factor-freshness checks

Stacked on #9208.