interval: join checked solver splits

[kim-em]

Summary

• add a function-agnostic, cut-type-polymorphic semantic coverage schema for solver splits
• add a transparent kernel join from the parent proof and two child-conditional target proofs
• add a Mathlib-free conformance theorem which consumes both child cases and rejects swapped quoted children
• specify branch-root provenance, child-local program extension, contradiction evidence, resources, and open scheduling/storage choices

A prepared policy split remains untrusted search data. It can enable proof emission only after the domain package proves exact child coverage and both child branches supply ordinary kernel evidence.

Verification

• lake build HexInterval.ProofEmitterConformance
• copyright, line-count, DAG, published trust-surface, factor-freshness, and diff checks
• no added native_decide, axiom, sorry, admit, unsafe, or implemented_by

Stack

Depends on #9215.