Measurement Provenance Semantics

Lean formalization of token-sensitive semantics for measurement-bearing expressions and provenance-aware rewrite classification.

This repository studies when repeated use of the same measurement justifies genuine interchangeability and when lookalike expressions support only one-way tightening. The formal development is mechanized in Lean 4 under the MeasurementProvenanceSemantics namespace and currently supports both:

• a denotational core for token-sensitive enclosure semantics; and
• a rewrite-facing layer distinguishing RewritesTo from Interchangeable.

Current research artifacts

• WPTE 2026 manuscript: papers/wpte-2026/manuscript.tex
• Denotational-core manuscript through M3: papers/denotational-core-m3/manuscript.md
• WPTE positioning memo: docs/project/31-wpte-positioning-memo.md
• Rewrite-theory summary: docs/project/37-rewrite-theory-layer.md

For citation metadata, see CITATION.cff.

Quick start

The repository uses a repo-local Lean toolchain under .tooling/elan.

./scripts/with-local-toolchain.sh lake build
bash scripts/check-token-cancellation.sh
bash scripts/check-background-subtraction.sh
bash scripts/check-blind-comparator.sh

To build the WPTE paper source locally:

cd papers/wpte-2026
pdflatex manuscript.tex

Repository layout

• MeasurementProvenanceSemantics/ — Lean source files for the formal development
• papers/ — manuscript sources and submission assets
• docs/project/ — project notes, theorem planning, and research memos
• docs/brainstorming/ — exploratory/archive material
• scripts/ — verification helpers and local automation scripts
• setup/ — environment-specific setup notes

Lean library

The formal development lives under the MeasurementProvenanceSemantics namespace, with the main entry module at MeasurementProvenanceSemantics.lean.