Add proof-producing contradiction leaves

[kim-em]

Summary

• add a generic package-owned refutation schema for an exact established fact
• eliminate that checked impossible fact into an arbitrary branch target without trusting runtime contradiction state
• add the first Real/exp .empty adapter and ordinary kernel theorem, with reduction rejecting .all
• retain the honest boundary: resolving a contradictory runtime leaf to exact fact evidence in the tree frontend remains future work
• add a guarded axiom report for the ordinary refutation theorem

Validation

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

Reconciled onto exact current main 23c4e006aa7f36e233fd7bffdd1c1d0b522a7dbd, preserving the merged #9220 provenance/state repairs and #9256 SPEC additions.

No native_decide, axiom, or sorry is introduced.