pith. machine review for the scientific record. sign in

arxiv: 2604.07626 · v2 · submitted 2026-04-08 · 💻 cs.LO · cs.PL

Recognition: unknown

Token-Sensitive Enclosure Semantics for Measurement-Bearing Expressions

David B. Hulak , Arthur F. Ramos , Ruy J. G. B. de Queiroz
Authors on Pith no claims yet

Pith reviewed 2026-05-10 16:48 UTC · model grok-4.3

classification 💻 cs.LO cs.PL
keywords measurement semanticsobservation tokenswarranted enclosurerewrite classificationinterval arithmeticprovenance trackingformal semanticsLean mechanization
0
0 comments X

The pith

Token identities in measurement expressions distinguish interchangeable rewrites from mere claim-tightening, since provenance-blind summaries cannot recover the correct classes.

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

The paper establishes that measurement expressions carry semantic information through the identity of each observation event, beyond what intervals and dimensions alone provide. It defines the meaning of an expression as the warranted enclosure consisting of all exact values consistent with hidden environments that assign one fixed value per token while staying inside the declared intervals. This distinction matters for operations such as cancellation, background subtraction, and self-division, where reusing a token produces full equivalence to the simplified form but distinct tokens produce only one-way containment. A sympathetic reader cares because standard interval or dimension-only representations lose the information needed to classify which rewrites are safe.

Core claim

The denotation of an expression is its warranted enclosure: the set of exact values still justified by hidden-value environments that assign one value to each observation token and respect the declared intervals. Over this semantics, e -> e' is a claim-tightening judgment equivalently enclosure containment Encl(e')subseteq Encl(e), while interchangeability is equality of enclosures. The distinction is visible in cancellation, background subtraction, and self-division: reusing one token gives interchangeability with the expected simplified expression, while using distinct tokens gives only one-way containment. The authors prove that provenance-blind summaries preserving intervals, dimension 1

What carries the argument

Warranted enclosure: the set of exact values justified by hidden-value environments that assign one consistent value to each observation token while respecting declared intervals.

Load-bearing premise

Observation tokens act as opaque primitives whose only role is to enforce that the same unknown exact value is assigned to every occurrence of the same token, and that such assignments exist inside the stated intervals.

What would settle it

Two expressions with identical intervals, dimension tags, and token-erased syntax but unequal warranted enclosures under the token semantics, which would be exhibited by a Lean-checked case where reuse versus distinct tokens changes enclosure equality.

read the original abstract

Token identity is semantic information for measurement-bearing expressions. Intervals, dimension tags, and token-erased syntax can say what values a measured leaf may take, but they cannot say whether two occurrences name the same observation or two fresh observations. We give a small formal semantics in which each measured leaf carries an interval of possible exact values and an opaque observation-event token. Here "token" means an identity for a measurement event, not a lexical token of the source syntax. The denotation of an expression is its warranted enclosure: the set of exact values still justified by hidden-value environments that assign one value to each observation token and respect the declared intervals. Over this semantics, e -> e' is a claim-tightening judgment, equivalently enclosure containment Encl(e') subseteq Encl(e), while interchangeability is equality of enclosures. The distinction is visible in cancellation, background subtraction, and self-division: reusing one token gives interchangeability with the expected simplified expression, while using distinct tokens gives only one-way containment. We prove that provenance-blind summaries of the kind studied here, preserving intervals, dimension tags, and token-erased syntax, are insufficient to recover the correct rewrite class. The formal results are mechanized in Lean 4 with no sorry or admit placeholders.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper claims that token identity is semantic information for measurement-bearing expressions: intervals, dimension tags, and token-erased syntax are insufficient to determine whether two measured leaves refer to the same observation event. It defines a formal semantics in which each measured leaf carries an interval and an opaque observation-event token; the denotation of an expression is its warranted enclosure (the set of exact values justified by hidden-value environments that assign one value per token while respecting the intervals). Over this semantics, e -> e' is enclosure containment while interchangeability is equality of enclosures. The distinction appears in cancellation, background subtraction, and self-division. The paper proves that provenance-blind summaries cannot recover the correct rewrite class and mechanizes the definitions, theorems, and insufficiency result in Lean 4 with no sorry or admit placeholders.

Significance. If the results hold, the work supplies a rigorous, mechanized account of why provenance matters for expressions involving uncertain measurements, with direct relevance to scientific computing, data analysis, and metrology. The complete Lean 4 mechanization (no placeholders) is a clear strength: it directly supports the enclosure-containment and interchangeability claims, the distinction between containment and equality, and the insufficiency theorem for provenance-blind summaries.

minor comments (2)
  1. [Abstract] The abstract introduces 'warranted enclosure' without a one-sentence gloss; adding a brief parenthetical definition would help readers who encounter the term first in the abstract.
  2. [Mechanization section] In the description of the Lean development, it would be useful to state explicitly which files contain the definitions of tokens, environments, and the enclosure operator (e.g., 'see Enclosure.lean, lines 45-67').

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive and accurate summary of the manuscript. The report correctly captures the central claim that token identity is semantic information for measurement-bearing expressions, the definition of warranted enclosures, the distinction between enclosure containment and interchangeability, and the insufficiency result for provenance-blind summaries, all supported by the complete Lean 4 mechanization.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper defines a new token-sensitive enclosure semantics directly from standard set-theoretic notions of intervals, hidden-value environments, and opaque observation tokens. The central claim (insufficiency of provenance-blind summaries for recovering rewrite classes) is established by explicit definitions of warranted enclosure, containment, and equality, followed by a complete Lean 4 mechanization containing no admits or sorrys. No load-bearing step reduces to a fitted parameter, self-citation chain, or renaming of prior results by the same authors; all derivations rest on the stated token-assignment rules and are independently verifiable in the formalization.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claim rests on introducing observation tokens as new primitives and assuming standard mathematical structures for sets and intervals; no free parameters are fitted to data.

axioms (2)
  • standard math Standard set theory and interval arithmetic
    Used to define enclosures as sets of justified exact values and environments that assign values within intervals.
  • domain assumption Existence of assignment functions from opaque tokens to exact values
    Invoked when defining warranted enclosures as those consistent with some hidden-value environment.
invented entities (1)
  • observation-event token no independent evidence
    purpose: To serve as an opaque identity distinguishing whether two measurement occurrences refer to the same event or independent events.
    New primitive added to the syntax and semantics to capture provenance beyond intervals and dimension tags.

pith-pipeline@v0.9.0 · 5534 in / 1409 out tokens · 60993 ms · 2026-05-10T16:48:56.787404+00:00 · methodology

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

18 extracted references · 15 canonical work pages

  1. [1]

    Baader and T

    F. Baader and T. Nipkow.Term Rewriting and All That. Cambridge University Press, 1998. DOI: 10.1017/CBO9781139172752

    work page doi:10.1017/cbo9781139172752 1998

  2. [2]

    R. E. Moore.Interval Analysis. Prentice-Hall, Englewood Cliffs, NJ, 1966

    1966

  3. [3]

    R. E. Moore, R. B. Kearfott, and M. J. Cloud.Introduction to Interval Analysis. Society for Industrial and Applied Mathematics, 2009. DOI: 10.1137/1.9780898717716

    work page doi:10.1137/1.9780898717716 2009

  4. [4]

    L. H. de Figueiredo and J. Stolfi. Affine arithmetic: concepts and applications.Numerical Algorithms, 37:147–158, 2004. DOI: 10.1023/B:NUMA.0000049462.70970.b6

    work page doi:10.1023/b:numa.0000049462.70970.b6 2004

  5. [5]

    Neumaier.Interval Methods for Systems of Equations

    A. Neumaier.Interval Methods for Systems of Equations. Cambridge University Press, 1990. DOI: 10.1017/CBO9780511526477

    work page doi:10.1017/cbo9780511526477 1990

  6. [6]

    Hickey, Q

    T. Hickey, Q. Ju, and M. H. van Emden. Interval arithmetic: from princi- ples to implementation.Journal of the ACM, 48(5):1038–1068, 2001. DOI: 10.1145/502027.502028

    work page doi:10.1145/502027.502028 2001

  7. [7]

    JCGM 100:2008, 2008

    Joint Committee for Guides in Metrology.Evaluation of measurement data – Guide to the expression of uncertainty in measurement. JCGM 100:2008, 2008. DOI: 10.59161/JCGM100-2008E.https://www.bipm. org/documents/20126/2071204/JCGM_100_2008_E.pdf

    work page doi:10.59161/jcgm100-2008e.https://www.bipm 2008

  8. [8]

    Guide to the expression of uncertainty in measurement

    Joint Committee for Guides in Metrology.Evaluation of measurement data – Supplement 1 to the “Guide to the expression of uncertainty in measurement” – Propagation of distributions using a Monte Carlo method. JCGM 101:2008, 2008. DOI: 10.59161/JCGM101-2008.https://www. bipm.org/documents/20126/2071204/JCGM_101_2008_E.pdf

    work page doi:10.59161/jcgm101-2008.https://www 2008

  9. [9]

    In: Graham, 24 Mitchell and Wang R.M., Harrison, M.A., Sethi, R

    P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approxima- tion of fixpoints. InProc. POPL, pp. 238–252. ACM, 1977. DOI: 10.1145/512950.512973. Token-Sensitive Enclosure Semantics17

    work page doi:10.1145/512950.512973 1977

  10. [10]

    A. Kennedy. Relational parametricity and units of measure. InProc. POPL, pp. 442–455. ACM, 1997. DOI: 10.1145/263699.263761

    work page doi:10.1145/263699.263761 1997

  11. [11]

    Buneman, S

    P. Buneman, S. Khanna, and W.-C. Tan. Why and where: a characteriza- tion of data provenance. InDatabase Theory – ICDT 2001, LNCS 1973, pp. 316–330. Springer, 2001. DOI: 10.1007/3-540-44503-X_20

    work page doi:10.1007/3-540-44503-x_20 2001

  12. [12]

    T. J. Green, G. Karvounarakis, and V. Tannen. Provenance semirings. In Proc. PODS 2007, pp. 31–40. ACM, 2007. DOI: 10.1145/1265530.1265535

    work page doi:10.1145/1265530.1265535 2007

  13. [13]

    Cheney, L

    J. Cheney, L. Chiticariu, and W.-C. Tan. Provenance in databases: why, how, and where.Foundations and Trends in Databases, 1(4):379–474,

  14. [14]

    DOI: 10.1561/1900000006

    work page doi:10.1561/1900000006

  15. [15]

    Herschel, R

    M. Herschel, R. Diestelkämper, and H. Ben Lamine. A survey on prove- nance: what for? what form? what from?The VLDB Journal, 26(6):881– 906, 2017. DOI: 10.1007/s00778-017-0486-1

    work page doi:10.1007/s00778-017-0486-1 2017

  16. [16]

    Moreau, P

    L. Moreau, P. Groth, J. Cheney, T. Lebo, and S. Miles. The PROV data model.ACM Transactions on Internet Technology, 15(1):3:1–3:31, 2015. DOI: 10.1145/2866565. W3C Recommendation:https://www.w3.org/ TR/prov-dm/

    work page doi:10.1145/2866565 2015

  17. [17]

    In: Au- tomated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings

    L. de Moura and S. Ullrich. The Lean 4 theorem prover and programming language. InAutomated Deduction – CADE 28, LNCS 12699, pp. 625–635. Springer, 2021. DOI: 10.1007/978-3-030-79876-5_37

    work page doi:10.1007/978-3-030-79876-5_37 2021

  18. [18]

    D. B. Hulak and A. F. Ramos.measurement-provenance- semantics. Lean 4 formalization, GitHub repository, com- miteede9350e14b9e0d9bb392d0b5b54873587f01d5, 2026. https://github.com/d0d1/measurement-provenance-semantics. David B. Hulak Independent Researcher E-mail:dbhulak@gmail.com Arthur F. Ramos Microsoft E-mail:arfreita@microsoft.com Ruy J. G. B. de Quei...

    2026