AI 中文总结
研究不同证明等虽行为相同但结构有别时的错误界定，开发受保护实现语义，通过确定重写中传输的子对象等方法，给出错误幅度上下界，应用于多种情况并得出相关结论，满足特定不等式。
AI 中文摘要
不同的证明、程序、公式或重写路径可能具有相同的可观察行为，但在出现结构、共享、接口或转换历史方面存在差异。我们开发了一种受保护实现语义，在提取错误时保留这些差异。产生的错误幅度上限由附加到所选实现的证书界定，下限由仅由观察到的行为确定的最大下界界定。对于类型化预层设置中的线性双推出重写，我们确定在重写步骤和有限重写路径中完整传输的最大子对象。受保护的局部估计组合起来给出路径式上证书。在集合层面，互补下界是行为纤维中幅度的下确界。对于非离散范畴，当该扩展存在时，它由逐点右 Kan 扩展给出，并且在格罗滕迪克纤维化假设下它简化为严格纤维下确界。对于到有限维赋范空间的连续满射线性观察，下反射是诱导商范数。应用于紧可度量化阿贝尔群上的有限多个不同特征，这产生了一个具有精确对偶公式的插值范数。连续和离散的阿贝尔转移定理然后将观察到的系数转换为尾部幅度的下界，对梅林变换、生成函数和有限域上曲线的归一化点数误差有影响。在所述保护和健全性假设下，每个实现都满足$Q(O(\mathrm{Err}(r))) \leq A(\mathrm{Err}(r)) \leq U(r)$。
英文摘要
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)$.
Comments36 pages; no figures. Reclassified 21 results (16 propositions, 4 corollaries, and 1 lemma); mathematical statements and proofs are unchanged
