Guarded Realization Semantics: Occurrence-Sensitive Certificates and Behavior-Dependent Lower Bounds

Abstract

Distinct proofs, programs, formulas, or rewrite paths may have the same observable behavior while differing in occurrence structure, sharing, interfaces, or transformation history. We develop a guarded realization semantics that retains these distinctions when an error is extracted. The resulting error magnitude is bounded above by a certificate attached to the chosen realization and below by the greatest lower bound determined solely by the observed behavior. For linear double-pushout rewriting in a typed presheaf setting, we identify the greatest subobject transported intact through a rewrite step and through a finite rewrite path. Guarded local estimates compose to give pathwise upper certificates. At the set level, the complementary lower bound is the infimum of magnitudes in a behavior fiber. For non-discrete categories, it is given by a pointwise right Kan extension when that extension exists, and it reduces to the strict-fiber infimum under a Grothendieck fibration hypothesis. For continuous surjective linear observations onto finite-dimensional normed spaces, the lower reflection is the induced quotient norm. Applied to finitely many distinct characters on a compact metrizable abelian group, this yields an interpolation norm with an exact dual formula. Continuous and discrete Abel transfer theorems then convert observed coefficients into lower bounds for tail amplitudes, with consequences for Mellin transforms, generating functions, and normalized point-count errors of curves over finite fields. Under the stated guards and soundness hypotheses, every realization satisfies $Q(O(\mathrm{Err}(r))) \leq A(\mathrm{Err}(r)) \leq U(r)$.