feat(interval): emit proofs from retained branch trees

[kim-em]

Summary

• add a function-independent bottom-up proof emitter for settled retained branch trees
• replay the two side-specific max x 0 child traces and join them with the package-owned split theorem
• reject incomplete, shared, cyclic, dangling, and unreachable tree shapes before returning a proof term
• split the ReLU client into its own conformance module while preserving exact parent/child/session/trace fidelity

Exact reconciliation

• base: b083ed96f8ad05fa38d97f0f47d32981c1c5910a (post-feat(interval): replay pinned PNT+ nested logarithm #9260 main)
• head: 8c1633850c240531944958a32fd7181d324a6ce2
• preserves the nested PNT-log experiment and conformance registrations introduced on the final base
• proof-only Lake freshness exemption is pinned to the exact resolved lakefile.lean blob 7b6aaa8aa8a5af86fb3de13fc11606499863c170

Verification

• lake build HexInterval.Experiment.BranchProof HexIntervalMathlib.ExpSignConformance HexIntervalMathlib.ReluConformance HexIntervalMathlib.PntLogTableConformance HexIntervalMathlib.PntNestedLogConformance HexInterval.SinTenIntervalConformance HexIntervalMathlib.SinTenConformance HexIntervalMathlib.SinTenIntervalConformance (2250 jobs)
• copyright, file-line, DAG, trust-surface, Phase 4, factor-freshness, PNT-inventory, and diff checks
• no added native_decide, axiom, sorry, admit, unsafe, or implemented_by
• fresh exact-head Opus review and exact-head CI are required before merge readiness