interval: close stronger target facts in the kernel

[kim-em]

Summary

• add a transparent generic proof combinator for closing a requested fact from a stronger retained fact
• require the independent fact-domain proveMeet theorem; runtime target subsumption remains proof-irrelevant
• resolve the exact retained (node, version, fact) in ProofFrontend and fail closed before emitting the kernel-checked closure step
• route dynamic exponential target closure through the new bridge
• add an ordinary strict-subsumption theorem and a negative converse guard
• state precisely that strict .nonnegative → .all is exercised directly through closeFact, while the current live closeTarget canaries close exact retained facts

Verification

• restacked on exact post-interval: drive arbitrary policies to a target fact #9214 main 433806f976f5586e6e4c053710e6d5f24314e768; its tree matches reviewed interval: drive arbitrary policies to a target fact #9214 head 3cd78d02bcc17a063e8d9f6e94b294ccf6fb1243, and stable patch IDs for the three Lean feature files match the pre-restack feature
• lake build HexInterval.Experiment.ProofEmitter HexInterval.Experiment.ProofFrontend HexIntervalMathlib.ExpSignConformance (1952 jobs)
• copyright, dependency-DAG, trust-surface, Phase 4, factor-freshness, diff-whitespace, and added-line banned-proof checks pass
• no native_decide, axiom, or sorry

Stack

#9214 is merged. Subdivision branch ownership and joining remain later proof-layer work.