feat(interval): replay a backward function contractor

[kim-em]

Summary

• prove the centered function inverse-image rule [3/16,1/4] -> [1/4,3/4]
• attach a backward propagator from a separate package to the existing opaque operation
• check the live event and replay it through the same generic fact transition
• reject a quote whose watched output premise is weakened, and pin the ordinary theorem axiom report
• reconcile the feature directly onto current upstream main, preserving the public interval and PNT registrations

Validation

• lake build HexInterval.Conformance HexIntervalMathlib.PntBKLNWPowConformance HexIntervalMathlib.MixedInstantiationConformance HexIntervalMathlib.ExactBranchConformance (2256 jobs, green on the reconciled lineage)
• trust-surface, PNT inventory, factor freshness, diff, and banned-proof checks are retained for exact CI

Base: upstream main at 505a91875c3409781d34999d023d04b1a8833b1b.