DataProvenance
plain-language theorem explainer
A provenance record that tags every empirical datum in the measurement quarantine with source type, optional SHA-256 hash, generator script, timestamp, version, and free-form metadata. Anyone wiring calibration constants or mined values into MeasurementResult cites it. The declaration is a plain structure with three smart constructors (manual, computed, calibrated).
Claim. A provenance record is a tuple $(d, s, h, g, t, v, m)$ where $d$ is a human-readable description, $s$ is a data source (manual, computation, external, mining, or calibration), $h$ is a SHA-256 hex hash of the artifact, $g$ is an optional path to a generator script, $t$ is an ISO-8601 timestamp, $v$ is a version string, and $m$ is a list of string key-value metadata pairs. Every empirical value in the quarantine zone must carry such a record.
background
The module builds quarantine infrastructure so that theorem-level claims never import raw empirical numbers. Measurement modules under Verification/Measurement/* are quarantined: the certified surface may not import them, while preregistered test suites may import both sides.
DataSource is the inductive tag for origin: hand entry, computation, external API, dataset mining, or calibration. The provenance structure sits on top of that tag and adds integrity fields (hash, script path, timestamp, version, metadata).
Downstream, MeasurementResult wraps a value of any type together with an optional uncertainty and exactly one provenance record. Raw calibration constants (classification threshold, stability threshold, CPM net/projection/energy controls) are all built as such wrapped results.
proof idea
No proof: this is a structure definition with deriving Repr. Three factory defs fill the fields for the common cases. manual sets source to manual, empty hash, no script, version "1.0", empty metadata. computed sets source to computation, stores the supplied hash and script path. calibrated sets source to calibration, empty hash, and records the method string in metadata. All three take a description and timestamp.
why it matters
Without this record, empirical constants would leak unlabeled into the certified surface. It is the mandatory wrapper for every datum in the quarantine zone, and it is the provenance field of MeasurementResult. Downstream raw constants (classifyThreshold_raw, stabilityThreshold_raw, C_net_raw, C_proj_raw, C_eng_raw) all construct instances via the manual/computed/calibrated factories, so audit trails for CPM coercivity bounds and classification thresholds bottom out here. The structure itself is not a physics claim; it is the bookkeeping layer that keeps Recognition Science's theorem surface free of untracked numbers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.