Token-Sensitive Enclosure Semantics for Measurement-Bearing Expressions

TL;DR

This paper introduces a formal semantics for measurement-bearing expressions that incorporates token identity to distinguish between observation events, enabling precise reasoning about enclosure and interchangeability.

Contribution

It presents a novel semantics that models measurement tokens and their enclosures, formalizing how observation identities affect expression equivalence and rewrite rules.

Findings

Reusing a token implies interchangeability with simplified expressions.

Using distinct tokens results in only one-way enclosure containment.

Mechanized formal proofs in Lean 4 validate the semantics and results.

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.