Ordinary algebraic equality is not a sound rewrite principle for measurement-bearing expressions. Reuse of the same observation matters, and division can make algebraically equal forms differ on where they are defined. We present a unified semantics that tracks both provenance and definedness. Token-sensitive enclosure semantics yields judgments for one-way rewriting and interchangeability. An admissible-domain refinement yields a domain-safe rewrite judgment, and support-relative variants connect local and global admissibility. Reduction theorems recover the enclosure-based theory on universally admissible supports. Recovery theorems internalize cancellation, background subtraction, and positive-interval self-division. Strictness theorems show that reachable singularities make simplification one-way and make common-domain equality too weak for licensed replacement. An insufficiency theorem shows that erasing token identity collapses distinctions that definedness alone cannot recover. All definitions and theorems are formalized in sorry-free Lean 4.

翻译：普通代数等式对于测量承载表达式而言并非有效的重写原则。同一观测的重用至关重要，而除法可能导致代数上相等的形式在定义性上存在差异。我们提出了一种统一语义，同时追踪来源与定义性。令牌敏感闭包语义为一向重写和可互换性提供了判断依据。可容许域精炼产生了域安全重写判断，而支撑相关变体则连接了局部与全局可容许性。归约定理在全可容许支撑上恢复了基于闭包的理论。恢复定理内化了消去、背景减除与正区间自除。严格性定理表明，可达奇异性使简化变为单向，并使公共域等式对于许可替换而言过于弱化。不足性定理显示，抹除令牌标识会抹平定义性本身无法恢复的区分。所有定义与定理均在无漏洞的 Lean 4 中形式化。