interval: replay a live split through exp

[kim-em]

Summary

• extend the Mathlib-free exponential domain to the four facts needed for a strict source-sign split
• add a real zero-split coverage schema and exact left/right BranchSeeds
• run actual left and right child sessions through the arbitrary exponential propagator
• pin each child's exact reached state and one-rule quoted trace before replay
• replay both nonempty child traces through emitBranch, close their targets, and join them with replaySplit
• reject mismatched child inputs and branch seeds, and guard the joined tactic theorem's axiom report

The canary deliberately does not claim useful branch-dependent closure: real exponential nonnegativity is unconditional, so neither child target proof needs its split assumption. Connecting an executable SplitPlan to child construction remains branch-manager work.

Verification

• lake build HexInterval.ProofEmitterConformance HexIntervalMathlib.SineTacticConformance HexIntervalMathlib.ExpSignConformance (1970 jobs)
• git diff --check 3967aa77e2855522d560b5b83ef0efb594d8d604
• copyright-header and DAG checks
• trust-surface, Phase 4, factor-freshness, and banned-proof-mechanism checks

Restacked directly on merged #9218 / exact main 3967aa77e2855522d560b5b83ef0efb594d8d604.