Pith. sign in

REVIEW 24 references

Error extracted from a realization is bounded above by occurrence-sensitive certificates and below by a greatest bound that depends only on observed behavior.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.5

2026-07-30 18:36 UTC pith:F5AG4NGR

load-bearing objection A long but coherent synthesis that packages DPO occurrence transport with behaviorwise lower bounds into a usable sandwich theorem; worth referee time if the AI-assisted proofs get checked.

arxiv 2607.23567 v1 pith:F5AG4NGR submitted 2026-07-26 math.CT

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

SeungJu Lee This is my paper
classification math.CT MSC 18M3518A4018F2043A1568Q42
keywords realization semanticsoccurrence structureDPO rewritingright Kan extensionquotient normcompact-group interpolationAbel meansbehavior-dependent lower bounds
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Distinct proofs, programs, formulas, or rewrite paths can share the same observable result while differing in sharing, interfaces, or history. This paper argues that those distinctions matter for error bounds, so error must be extracted from the chosen realization before collapsing to behavior. The magnitude of that error is then sandwiched: an upper certificate built from guarded local estimates along the realization’s path, and a lower bound forced solely by what is observed. For linear double-pushout rewriting the paper identifies the greatest subobject carried intact through a step or path, so certificates compose only where occurrences survive. For linear observations the lower bound becomes a quotient norm, and via compact-group interpolation and Abel transfer it yields concrete tail lower bounds for Mellin data, generating functions, and normalized point-count errors of curves over finite fields.

Core claim

Under stated guards and soundness hypotheses, every applicable realization r satisfies Q(O(Err(r))) ≤ A(Err(r)) ≤ U(r): the true error magnitude sits between a greatest lower reflection Q determined only by observed error behavior and an occurrence-based upper certificate U attached to the chosen realization.

What carries the argument

Guarded realization semantics: extract structured Err(r) first; compose sound local certificates in an ordered error algebra along intact DPO track domains for U(r); take the behaviorwise lower reflection Q as fiber infimum, right Kan extension Ran_O A, or the quotient/interpolation norm induced by the observation.

Load-bearing premise

Boundary coefficients from a Mellin or generating-function continuation may be used only when that continuation still agrees with the original interior integral or series on the interior side of the boundary; without that agreement the tail lower bounds do not apply to the original error.

What would settle it

Exhibit a guarded realization whose observed Abel or character coefficients force a positive Q, yet whose actual tail amplitude A falls strictly below Q, or a claimed sound path certificate U that is smaller than the realized magnitude A on its stated guard.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

Share X Bluesky LinkedIn Reddit HN

If this is right

  • Intact occurrence transport through linear DPO steps and paths is exactly the greatest subobject below the composite track domain, so pathwise upper certificates compose only on that domain.
  • Continuous or discrete Abel limits at finitely many distinct frequencies lower-bound essential tail amplitude by the compact-orbit interpolation norm, with an exact dual L1 character-polynomial formula.
  • Simple Mellin or generating-function boundary poles, under interior agreement, convert residues into the same tail lower bounds; higher-order poles force unbounded normalized tails.
  • For a smooth projective curve of genus ≥1 over a finite field, the normalized point-count error’s limsup is at least the interpolation norm of the Frobenius multiplicity vector on its orbit group.
  • Behavior-level representable quotation cannot separate nonisomorphic realizations with the same behavior; fiberwise or aggregate codes retain that data without choosing a single representative.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same sandwich suggests a practical audit pattern for approximate programs: keep a path-sensitive upper certificate in the rewriter or compiler, and independently check observed spectral or Abel coefficients against the quotient lower bound.
  • When character relations make the interpolation norm much larger than the Euclidean coefficient norm, dependent frequency observations can certify unboundedness even for square-summable coefficient sequences.
  • Proof assistants and cut-elimination engines could expose residual obligations as Err(r) and report both the intact-transport upper certificate and the behavior-forced lower floor after normalization.
  • Any observer that is not a fibration may make the lower reflection depend on comma reindexings into cheaper realizations, so the design of the observation map itself becomes part of the bound’s meaning.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Circularity Check

0 steps flagged

No significant circularity: the sandwich is a universal-property packaging of independently constructed upper certificates and behaviorwise lower reflections, not a fit or self-citation loop.

full rationale

The central comparison Q(O(Err(r))) ≤ A(Err(r)) ≤ U(r) does not reduce inputs to outputs by construction in the sense flagged by this pass. U(r) is built compositionally from guarded local certificates in an ordered error algebra (Thm 25.2, Prop 25.4) under explicit soundness hypotheses (S1)–(S3)/(I3); that is ordinary monoid induction, not a fitted parameter renamed as a prediction. Q is defined as the greatest behavior-level lower bound (fiber infimum, Thm 28.2; or Ran_O A, with the fibration reduction in Thm 28.4) and is further identified with quotient norms (Thm 29.1) and compact-group interpolation duals (Thm 32.3) via standard duality, then transferred to tail amplitudes by Abel/Kronecker–Weyl arguments (Thms 33.2, 34.2) under stated interior-agreement guards. The left inequality is the counit/universal property of that reflection—true once Q is so defined—but the paper states this openly rather than smuggling a data fit. The finite-field application explicitly separates the coefficient-constrained lower bound from the exact limsup of the trigonometric realization (Thm 36.1, Rmk 36.2), which is anti-circular. References are to external standard sources (Mac Lane–Moerdijk, Lack–Sobociński, Rudin, Weil, Deligne, etc.); there is no load-bearing self-citation, uniqueness import from the same authors, or ansatz smuggled via prior own work. No steps meet the quote-and-reduce standard for circularity.

Axiom & Free-Parameter Ledger

0 free parameters · 8 axioms · 3 invented entities

The central sandwich rests on standard categorical and analytic machinery plus domain guards the paper is explicit about. No numerical free parameters are fitted. Invented structure is organizational (realization–error datum, certificate soundness predicate, transport bicategory of occurrences) rather than new physical entities. Load-bearing non-standard inputs are the soundness axioms (S1)–(S3), cartesian/isomorphism-invariant error extraction, actual-domain guards for partial rules and boundary transfers, and existence of the relevant right Kan extension or quotient presentation.

axioms (8)
  • standard math Linear DPO steps in an adhesive topos (typed presheaf slice) have monic matches/context legs; pushouts along monos are pullbacks, yielding maximal intact transported subobject D.
    Invoked in Thm 5.3–6.3 and 7.1; cites Lack–Sobociński adhesive rewriting.
  • domain assumption Soundness predicate on ordered error algebra: identity sound, generators sound on guards, soundness closed under ordered composition on composite guards (S1)–(S3).
    Thm 25.2; without this, pathwise U(r) is not a valid upper certificate.
  • domain assumption Error extractor Err is cartesian or isomorphism-invariant; realizations fibered in groupoids with occurrence transport along cartesian arrows.
    Hypotheses (I1)–(I2) of Thm 37.1; needed so A(Err(r)) and Q(O(Err(r))) descend appropriately.
  • domain assumption When used, O is a Grothendieck fibration (or categories are discrete) so Ran_O A reduces to strict-fiber infimum; otherwise comma-category infimum applies.
    Thm 28.4 and §38 item 3; changes the meaning of the lower endpoint.
  • standard math Continuous linear surjection T:X↠B onto finite-dimensional normed B induces quotient norm with dual formula via T*; compact-group coefficient maps are such surjections.
    Thm 29.1, 32.3; standard quotient duality.
  • domain assumption Boundary Abel/Mellin/generating-function coefficients equal limits from the original interior representation (agreement guard), not from continuation alone.
    Remark 33.6, Cor 33.4, Cor 34.3; required for Thm 33.2, 34.2, 38.1.
  • standard math Weil point-count formula and Deligne |\alpha_j|=q^{1/2} for smooth projective geometrically connected curves of genus ≥1.
    §36 application only; cited [22,23].
  • standard math Sion minimax on compact convex uncertainty in finite dimensions; weak-star compactness of dual balls for simultaneous linear constraints.
    Thm 29.5 and 30.5.
invented entities (3)
  • Realization–error datum (R,E,B_err,S with Err, O, A) no independent evidence
    purpose: Organize extraction of structured error before behavior observation so upper and lower bounds use different information.
    Definition 2.1; definitional packaging of the framework, not an external object.
  • Guarded realization semantics / occurrence-based upper certificate U paired with behaviorwise reflection Q no independent evidence
    purpose: State the sandwich Q(O(Err(r))) ≤ A(Err(r)) ≤ U(r) with compositional path certificates and observer-forced lowers.
    Defs 2.4–2.5, Thm 28.2, 37.1; the paper’s central organizing proposal.
  • Transport bicategory of occurrences Occ_R and track pseudofunctor Trk no independent evidence
    purpose: Identify intact residuals and coherence/monodromy of occurrence transport along rewrite paths.
    Defs 7.3–7.4, Thm 7.1; built from standard spans but named as part of the contribution.

pith-pipeline@v1.2.0-grok45-kimik3 · 38845 in / 4233 out tokens · 88803 ms · 2026-07-30T18:36:53.567469+00:00 · methodology

0 comments
Cite this review

Pith. "Pith review of Guarded Realization Semantics: Occurrence-Sensitive Certificates and Behavior-Dependent Lower Bounds." pith.science (2026). https://pith.science/paper/F5AG4NGR

@misc{pith2026260723567,
  author       = {Pith},
  title        = {Pith review of: Guarded Realization Semantics: Occurrence-Sensitive Certificates and Behavior-Dependent Lower Bounds},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/F5AG4NGR}},
  note         = {Machine review of arXiv:2607.23567}
}
Share X Bluesky LinkedIn Reddit HN
read the original 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)$.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

24 extracted references · 2 canonical work pages

  1. [1]

    Whole-grain Petri nets and processes.Journal of the ACM, 70(1):1–58, 2022

    Joachim Kock. Whole-grain Petri nets and processes.Journal of the ACM, 70(1):1–58, 2022. doi: 10.1145/3559103. URLhttps://arxiv.org/pdf/2005.05108

    Pith/arXiv arXiv 2022

  2. [2]

    Springer, 1992

    Saunders Mac Lane and Ieke Moerdijk.Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer, 1992. doi: 10.1007/978-1-4612-0927-0. URL https://openlibrary.org/works/OL2739892W/ Sheaves_in_geometry_and_logic

    doi:10.1007/978-1-4612-0927-0 1992

  3. [3]

    Adhesive and quasiadhesive categories.RAIRO – Theoretical Informatics and Applications, 39(3):511–545, 2005

    Stephen Lack and Paweł Sobociński. Adhesive and quasiadhesive categories.RAIRO – Theoretical Informatics and Applications, 39(3):511–545, 2005. doi: 10.1051/ita:2005028. URLhttps://www.numdam.org/item/10.1051/ ita:2005028.pdf

    doi:10.1051/ita:2005028 2005

  4. [4]

    Fundamentals of compositional rewriting theory.Journal of Logical and Algebraic Methods in Programming, 135:100893, 2023

    Nicolas Behr, Russ Harmer, and Jean Krivine. Fundamentals of compositional rewriting theory.Journal of Logical and Algebraic Methods in Programming, 135:100893, 2023. doi: 10.1016/j.jlamp.2023.100893. URL https://arxiv.org/pdf/2204.07175

    arXiv 2023

  5. [5]

    Rewriting in free hypergraph categories

    Fabio Zanasi. Rewriting in free hypergraph categories. InProceedings Third Workshop on Graphs as Models (GaM 2017), volume 263 ofElectronic Proceedings in Theoretical Computer Science, pages 16–30, 2017. doi: 10.4204/EPTCS.263.2. URLhttps://arxiv.org/pdf/1712.09495

    Pith/arXiv arXiv 2017

  6. [6]

    Rewriting with Frobenius

    Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Paweł Sobociński, and Fabio Zanasi. Rewriting with Frobenius. InProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), pages 165–174. ACM, 2018. doi: 10.1145/3209108.3209137. URLhttps://discovery.ucl.ac.uk/10053250/1/ paperLICS18.pdf. 36 Guarded Realization Semantics

    arXiv 2018

  7. [7]

    Proof-nets: The parallel syntax for proof-theory

    Jean-Yves Girard. Proof-nets: The parallel syntax for proof-theory. In Aldo Ursini and Paolo Aglianò, editors,Logic and Algebra, volume 180 ofLecture Notes in Pure and Applied Mathematics, pages 97–124. Marcel Dekker, 1996. URLhttps://girard.perso.math.cnrs.fr/Proofnets.pdf

    1996

  8. [8]

    Proof nets and the identity of proofs, 2006

    Lutz Straßburger. Proof nets and the identity of proofs, 2006. URLhttps://arxiv.org/pdf/cs/0610123. arXiv:cs/0610123

    Pith/arXiv arXiv 2006

  9. [9]

    PhD thesis, University of Edinburgh, 1997

    Masahito Hasegawa.Models of Sharing Graphs: A Categorical Semantics of let and letrec. PhD thesis, University of Edinburgh, 1997. URLhttps://www.kurims.kyoto-u.ac.jp/~hassei/papers/ECS-LFCS-97-360.pdf

    1997

  10. [10]

    Intensionality, extensionality, and proof irrelevance in modal type theory

    Frank Pfenning. Intensionality, extensionality, and proof irrelevance in modal type theory. InProceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS 2001), pages 221–230. IEEE, 2001. doi: 10.1109/LICS.2001.932499. URLhttps://www.cs.cmu.edu/~fp/papers/lics01.pdf

    arXiv 2001

  11. [11]

    Jason Z. S. Hu and Brigitte Pientka. Layered modal type theory: Where meta-programming meets intensional analysis. InProgramming Languages and Systems (ESOP 2024), volume 14576 ofLecture Notes in Computer Science, pages 52–82. Springer, 2024. doi: 10.1007/978-3-031-57262-3_3. URLhttps://www.cs.mcgill.ca/ ~bpientka/papers/esop24.pdf

    work page doi:10.1007/978-3-031-57262-3_3 2024

  12. [12]

    Springer, 2 edition, 1998

    Saunders Mac Lane.Categories for the Working Mathematician, volume 5 ofGraduate Texts in Mathemat- ics. Springer, 2 edition, 1998. doi: 10.1007/978-1-4757-4721-8. URL https://archive.org/details/ categoriesforwor0000macl

    doi:10.1007/978-1-4757-4721-8 1998

  13. [13]

    Fibered categories à la Jean Bénabou, 2023

    Thomas Streicher. Fibered categories à la Jean Bénabou, 2023. URLhttps://arxiv.org/pdf/1801.02927. arXiv:1801.02927, version 20, 13 September 2023

    Pith/arXiv arXiv 2023

  14. [14]

    Stack semantics of type theory

    Thierry Coquand, Bassel Mannaa, and Fabian Ruch. Stack semantics of type theory. In32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017), pages 1–11. IEEE, 2017. doi: 10.1109/LICS.2017.8005130. URLhttps://arxiv.org/pdf/1701.02571

    arXiv 2017

  15. [15]

    Conway.A Course in Functional Analysis, volume 96 ofGraduate Texts in Mathematics

    John B. Conway.A Course in Functional Analysis, volume 96 ofGraduate Texts in Mathematics. Springer, 2 edition,

  16. [16]

    Folland.Real Analysis: Modern Techniques and Their Applications

    Gerald B. Folland.Real Analysis: Modern Techniques and Their Applications. Wiley, 2 edition, 1999. URL https://archive.org/details/realanalysismode0000foll_q2y3

    1999

  17. [17]

    On general minimax theorems.Pacific Journal of Mathematics, 8(1):171–176, 1958

    Maurice Sion. On general minimax theorems.Pacific Journal of Mathematics, 8(1):171–176, 1958. doi: 10.2140/pjm.1958.8.171. URLhttps://msp.org/pjm/1958/8-1/pjm-v8-n1-p14-p.pdf

    doi:10.2140/pjm.1958.8.171 1958

  18. [18]

    Explicit Kronecker–Weyl theorems and applications to prime number races.Research in Number Theory, 8(3):43, 2022

    Alexandre Bailleul. Explicit Kronecker–Weyl theorems and applications to prime number races.Research in Number Theory, 8(3):43, 2022. doi: 10.1007/s40993-022-00349-2. URLhttps://arxiv.org/pdf/2007.05763

    Pith/arXiv arXiv 2022

  19. [19]

    Interscience, 1962

    Walter Rudin.Fourier Analysis on Groups, volume 12 ofInterscience Tracts in Pure and Applied Mathematics. Interscience, 1962. URLhttps://archive.org/details/fourieranalysiso0000rudi

    1962

  20. [20]

    Cambridge University Press, 3 edition, 2004

    Yitzhak Katznelson.An Introduction to Harmonic Analysis. Cambridge University Press, 3 edition, 2004. doi: 10.1017/CBO9781139165372. URLhttps://books.google.com/books?id=gkpUE_m5vvsC

    doi:10.1017/cbo9781139165372 2004

  21. [21]

    The Mellin transform and other useful analytic techniques

    Don Zagier. The Mellin transform and other useful analytic techniques. InQuantum Field Theory I: Basics in Mathematics and Physics, pages 305–323. Springer, 2006. URLhttps://people.mpim-bonn.mpg.de/zagier/ files/tex/MellinTransform/fulltext.pdf. Appendix to Eberhard Zeidler’sQuantum Field Theory I

    2006

  22. [22]

    Hermann, 1948

    André Weil.Sur les courbes algébriques et les variétés qui s’en déduisent, volume 1041 ofActualités Scientifiques et Industrielles. Hermann, 1948. URLhttps://gallica.bnf.fr/ark:/12148/bpt6k3372566b.texteImage

    1948

  23. [23]

    La conjecture de Weil

    Pierre Deligne. La conjecture de Weil. I.Publications Mathématiques de l’IHÉS, 43:273–307, 1974. doi: 10.1007/BF02684373. URLhttps://www.numdam.org/item/PMIHES_1974__43__273_0.pdf

    work page doi:10.1007/bf02684373 1974

  24. [1990]

    URLhttps://archive.org/details/courseinfunction0000conw

    doi: 10.1007/978-1-4757-4383-8. URLhttps://archive.org/details/courseinfunction0000conw

    doi:10.1007/978-1-4757-4383-8