Join proved and proof-refuted branch leaves

[kim-em]

Summary

• add package-owned refutation recognizers and handles to the generic proof registry
• add frontend emission from an exact chronology-proved node/version/fact to a RefuteSchema; live callers supply retained engine arrays as untrusted selector data
• run a live output split where the left child closes from .nonnegative and the right child derives .empty from .negative, then closes only by semantic refutation
• join those ordinary child proofs into a kernel-checked theorem; runtime contradiction state selects the path but never enters evidence
• reject ambiguous handles, array-length mismatch, changed fact snapshots, and stale bottom versions
• guard the mixed theorem's dependencies and tactic failure-state restoration

Validation

• lake build HexInterval.Experiment.ProofRegistry HexInterval.Experiment.ProofFrontend HexIntervalMathlib.ProofRegistryConformance HexIntervalMathlib.RefuteConformance HexIntervalMathlib.ExpSignConformance (1969 jobs)
• copyright, line-count, DAG, released trust-surface, Phase 4, factor-sweep freshness, diff, and banned-proof checks

Reconciled onto exact current main 835ef164be760fa0d173c32b895cc8c1568efda4, preserving merged #9221 and #9256 content.

No native_decide, axiom, or sorry is introduced.