feat(interval): replay an arbitrary centered function

[kim-em]

Summary

• give the opaque centered operation an exact real semantics over the dyadic interval domain
• prove and replay the package-owned [0,1] -> [0,1/4] forward contractor through the generic rule frontend
• pin the live retained event and ordinary theorem, with a negative premise mutation and guarded axiom report
• document the minimal arbitrary-function vertical in the SPEC

Validation

• focused 2,252-job build covering centered, dyadic, nested-branch, ReLU, and PNT targets
• copyright, line-count, DAG, trust-surface, Phase 4, factor-freshness, and PNT-inventory checks
• exact resolved Lake proof-only exemption; no native_decide, axiom, or sorry

Reconciled directly onto current upstream main after #9227 merged.