When Equality Fails as a Rewrite Principle: Provenance and Definedness for Measurement-Bearing Expressions
This work tackles foundational issues in mathematical rewriting for measurement-based systems, though it appears incremental as it builds on existing semantics to handle specific cases like division and reuse.
The paper addresses the unsoundness of ordinary algebraic equality for measurement-bearing expressions by introducing a unified semantics that tracks provenance and definedness, formalizing all definitions and theorems in Lean 4.
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.