We study certificate-based verification of straight-line intervalprograms built over a fixed primitive core$\Sprim=\{+,-,\times,\operatorname{inv},\operatorname{sqrt},\relu\}$with polynomial specification constraints expressed over$\{+,-,\times\}$.Our main result is a \emph{verifier-closure theorem}: for this fixedcore, every obligation the verifier must discharge is aquantifier-free ground integer formula, each non-trivial primitive ruleis witnessed by explicit Euclidean data, and acceptance is decided bydeterministic replay of a finite ledger without search.The contribution is not a new interval semantics, not a decisionprocedure for non-linear real arithmetic in general, and not averification of deployed floating-point code; it is a closure resultfor a concrete verifier architecture over a fixed primitive set.The architecture rests on a strict Galois insertion between realintervals and an encoded fixed-point integer domain, a totalnormalisation homomorphism~$\tau$ mapping certificate-side expressionsinto a ground integer signature $\Sint$, closed-form witness-bearingrules for each primitive, and a specification-side ledger replayed bythe same machinery.Verifier acceptance implies the existence of a unique concrete realtrajectory and enclosure of every certified specification constraint;structural replay cost is $O(n+s)$ in the ledger size.Transfer from certified mathematical semantics to a deployedimplementation is isolated as an explicit implementation-inclusioncontract, kept outside the verifier's trusted computing base.Core definitions and soundness theorems are mechanically verified inLean~4 using Mathlib.▽Lean Proofhttps://github.com/GhostDriftTheory/adic-lean-proof-replay