interval: drive arbitrary policies to a target fact

[kim-em]

Summary

• add a Mathlib-free, target-directed runner over the proof-producing PolicySession
• keep the controller generic in both fact representation and policy-private state
• distinguish target, saturation, contradiction, split, incompleteness, explicit stop, fuel, malformed-state, and resource outcomes
• retain the exact fact/version selected by runtime target subsumption while keeping that runtime test proof-irrelevant
• drive the nested exponential canary through two live policy steps and replay both events into an ordinary kernel theorem

Verification

• lake build HexInterval.Experiment.TargetRun HexIntervalMathlib.ExpSignConformance (1,959 jobs)
• copyright, DAG, trust-surface, phase, factor-freshness, diff, and banned-proof checks pass
• no native_decide, axiom, or sorry
• proof-only Lake exemption matches exact lakefile.lean blob 4c861820dbf8db07758455a01f04156f59ad2439

Base and scope

Restacked onto current main at 9f9a5e1f54c6d29d5eb18e2802f46731dda2cbba. Range-diff equality preserves all three previously approved feature/honesty commits, and patch-ID checks confirm the TargetRun and exponential conformance Lean deltas are unchanged. Current-main content, the #9213 resource-envelope disclosure, and guarded axiom reports are retained.

The SPEC records that session-start failures, non-target run stops, registry failures, and conservative target-probe failures currently collapse at the tactic diagnostic boundary. Strictly stronger retained-fact closure and execution/joining of returned split plans remain follow-up work.