interval: run search on reified goals

[kim-em]

Summary

• remove the fixed two-node exponential search fixture from the modeled-goal tactic
• start PolicySession from the actual reified CheckerInput
• select the exponential rule at the actual target node, quote that session, and replay it through the generic proof frontend with the dynamic program and caller facts
• cover both a graph extended by an unrelated supported hypothesis and the distinct three-node target exp (exp x) with ordinary theorem canaries
• keep model construction, scheduling, quotation, and replay free of graph-shape cases
• document the current resource mismatch honestly: goal reification permits 16 nodes/depth 8, while the ExpSign session currently permits 5 nodes/depth 4

Validation

• focused HexIntervalMathlib.ExpSignConformance build (1,958 jobs)
• copyright, line-count, DAG, trust-surface, Phase 4, factor-freshness, and diff checks
• fresh isolated exact-head review: approve, no blockers
• exact-head CI required before merge

No native_decide, axioms, or sorries are introduced.