MeasurementResult
plain-language theorem explainer
A typed wrapper for any empirical measurement: the value, an optional real uncertainty, and a mandatory provenance record. Anyone packaging calibration constants or mined datasets in the quarantine zone cites it. Pure structure definition with companion unwrap and map; no proof content.
Claim. A measurement result over a type $\alpha$ is a triple $(v, u, p)$ where $v \in \alpha$ is the measured value, $u \in \mathbb{R} \cup \{\bot\}$ is an optional uncertainty bound, and $p$ is a data-provenance record (source, hash, generator, timestamp).
background
This module is the quarantine layer for empirical inputs. Certified theorem-level claims must not import raw data; every measurement, calibration constant, or mined dataset lives behind a provenance record and may only reach the certified surface through an explicit hypothesis bridge.
A provenance record carries a human-readable description, a source tag (manual, calibrated, computed, mined, etc.), a SHA-256 hash of the artifact, an optional generator-script path, and an ISO-8601 timestamp. The measurement-result structure simply attaches that record to a typed value and an optional real error bar.
Local companions include unwrap (drop provenance, keep the value) and map (apply a pure function to the value while copying uncertainty and provenance unchanged).
proof idea
No proof: this is a structure declaration. Fields are value, optional uncertainty, and provenance. The file also defines unwrap as projection onto value, and map as the functorial action that transforms the value and leaves uncertainty and provenance fixed.
why it matters
This is the standard carrier for every quarantined empirical constant in the measurement layer. Downstream raw constants (classification threshold 0.9, stability threshold, net/projection/energy CPM constants) are all instances of it. The DataHypothesis bridge then lifts a measurement result into a named claim that test suites may consume without letting the certified surface import the quarantine zone.
It enforces the module's quarantine rule: Verification/Measurement/* stays sealed off from theorem-level imports, while preregistered tests may touch both sides. No forcing-chain landmark (T0–T8, RCL, phi) is at stake; the object is infrastructure hygiene for empirical inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.