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.

翻译：令牌身份是测量承载表达式的语义信息。区间、维度标签和令牌擦除语法可以说明测量叶子可能取的值，但无法说明两个出现次是指同一观测还是两个新的观测。我们给出一个小型形式语义，其中每个测量叶子携带一个可能精确值的区间和一个不透明的观测事件令牌。此处的"令牌"指测量事件的身份，而非源语法的词法令牌。表达式的指称是其有保证的封闭集：由隐藏值环境证明的精确值集合，该环境为每个观测令牌分配一个值并遵守声明的区间。在此语义下，e -> e' 是声明收紧判断，等价于封闭集包含关系 Encl(e') 含于 Encl(e)，而可互换性则是封闭集相等。这种区别在消去、背景减除和自除法中可见：重复使用同一令牌可得到与预期简化表达式的可互换性，而使用不同令牌则仅得到单向包含关系。我们证明，此类保留区间、维度标签和令牌擦除语法的来源无关摘要不足以恢复正确的重写类别。形式化结果已在 Lean 4 中机械化验证，不含任何 sorry 或 admit 占位符。