Validate split plans into exact child sessions

[kim-em]

Summary

• add a Mathlib-free, function-independent branch-start transition
• authenticate each plan against its exact engine-retained suggestion, action, scope, cut, reason, and proposal-time fact version
• repeat endpoint-cost and current program/fact/version checks, then require two distinct strict domain narrowings
• seal branch-tree scope/depth accounting and allocate exact child scopes under depth and total-scope budgets
• bind completed child runs back to their prepared program, initial facts, scopes, retained target fact, and version
• connect the selected exponential zero-landmark plan to the existing two-child live proof canary while preserving its exact trace/side/seed guards
• reject stale, forged, missing-suggestion, wrong-state/scope, duplicate, exhausted, wrong-input, contradictory, and unfinished cases

Trust boundary

This layer validates runtime search state and constructs child sessions; it is not proof evidence. BranchSeed, the package-owned coverage theorem, chronological replay, target closure, and the kernel-checked split join remain the proof boundary. Runtime contradiction is deliberately not accepted as proof closure. The exponential target is still unconditional, so this canary is not claimed as useful branch-dependent closure.

Verification

• lake build HexInterval.Experiment.BranchStart HexInterval.ProofEmitterConformance HexIntervalMathlib.SineTacticConformance HexIntervalMathlib.ExpSignConformance (1971 jobs)
• git diff --check 7b25e51ea28a6783835e3bd81758941894a4b2cf
• copyright-header and DAG checks
• trust-surface, Phase 4, factor-freshness, and banned-proof-mechanism checks

Restacked directly on merged #9219 / exact main 7b25e51ea28a6783835e3bd81758941894a4b2cf and includes retained-suggestion/state repair d9f686d6598ecd6126a00c7bed50a87ec06ef56f.