DataHypothesis
plain-language theorem explainer
Packages an empirical measurement as a named, status-tracked hypothesis with an explicit falsifier and a plan to promote it to a theorem. Verification authors cite it when quarantining calibration constants or mined thresholds before they touch the certified surface. The companion constructor is a pure record fill that copies the measured value and marks status unverified.
Claim. A data hypothesis over a type $\alpha$ is a record $(n, c, m, s, f, p)$ where $n$ is a name, $c \in \alpha$ is the claimed value, $m$ is a measurement result carrying $c$ with provenance and optional uncertainty, $s$ is a hypothesis status (unverified, validated, preregistered, or deprecated), $f$ is a textual falsification condition, and $p$ is a textual plan to discharge the hypothesis into a theorem. From a measurement $m$, one builds such a record by taking claim $= m.\mathrm{value}$ and status $=$ unverified.
background
The module is the quarantine layer for empirical inputs in Recognition Science verification. Certified theorem surfaces must not import raw measurements; everything empirical is wrapped so provenance, status, and a removal path stay explicit. Quarantined modules live under Verification/Measurement/*; only preregistered test suites may mix them with the certified surface.
A measurement result pairs a value in $\alpha$ with optional uncertainty and a provenance record (source, hash, generator). Hypothesis status is a four-way tag: unverified (data present, not checked), validated, preregistered (used in a locked test suite), or deprecated. The data-hypothesis record is the bridge named in the module doc as the link from quarantined data to claims that may later be certified.
Upstream status strings and constant bundles (RS-native units, CPM constants, BIT kernel names) illustrate the same pattern elsewhere: named empirical or calibration objects stay outside pure derivation until a theorem retires them.
proof idea
Not a proof: a structure definition plus a one-line record constructor. fromMeasurement sets name and the supplied falsifier/plan strings, copies claim from the measurement's value field, stores the full measurement, and hard-wires status to unverified. No lemmas are applied.
why it matters
Keeps calibration and mined thresholds out of the certified surface until they earn a theorem. Downstream, the classification threshold $0.9$ and stability threshold $0.01$ are registered exactly this way: each is a data hypothesis built from a raw measurement, with falsifiers such as "a different threshold achieves better accuracy" or "perturbation changes classification within threshold," and removal plans pointing at stability analysis, information theory, or a tight overlap-perturbation bound.
That matches the module purpose: bridge quarantined data to certified claims without smuggling floats into forcing-chain or RCL results (T5 J-uniqueness, phi, eight-tick structure). Open work is discharging those removal plans so the thresholds stop being hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.