interval: seed proof branches safely

[kim-em]

Summary

• weaken inherited parent consequences into the exact child assumption context
• expose the one split-side fact as the sole new branch assumption
• bind every version-zero child fact and the full initial-array length in a transparent BranchSeed
• exercise all three seed entries in Mathlib-free conformance: the child side, a derived inherited consequence, and an unrelated top fact
• prove explicitly that the inherited .enabled seed is not a literal member of the parent base, while deriving it from the parent .yes theorem

This prevents restarting a child solver from silently reclassifying parent-derived facts as caller assumptions. The public BranchSeed shape is unchanged by the strengthened canary.

Verification

• restacked on exact post-interval: join checked solver splits #9216 main 816b3da83788c12385e71b9c66ee0f78786c7cdc; its second parent is reviewed interval: join checked solver splits #9216 head ce9e9143f9d5f5d43a3d0cbba31f70dca8d74868, and the trees are identical
• preserves interval: join checked solver splits #9216's direct swapped-child rejection, genuine noncoverage theorem, guarded axiom report, and final split-proof SPEC closure
• lake build HexInterval.Experiment.ProofEmitter HexInterval.ProofEmitterConformance (13 focused jobs)
• copyright, dependency-DAG, published trust-surface, Phase 4, factor-freshness, diff-whitespace, and added-line banned-mechanism checks pass
• no added native_decide, axiom, sorry, admit, unsafe, or implemented_by

Stack

#9216 is merged; this PR now targets main directly.