HypothesisStatus
plain-language theorem explainer
Four-valued status tag for any hypothesis built from empirical data: unverified, validated, preregistered, or deprecated. Downstream provenance records and the DataHypothesis bridge cite it to keep raw measurements out of the certified surface. The declaration is a plain inductive with DecidableEq and Repr; there is no proof obligation.
Claim. There is a finite status type for data-derived hypotheses with exactly four constructors: $\mathsf{unverified}$ (data present but not independently checked), $\mathsf{validated}$ (passed an independent check), $\mathsf{preregistered}$ (admitted into a preregistered test suite), and $\mathsf{deprecated}$ (superseded by newer data). Equality of statuses is decidable.
background
The enclosing module is the quarantine layer for empirical input. Certified theorem-level claims must not import raw measurements, calibration constants, or mined datasets. Instead every such value is wrapped in a provenance record (source, hash, generator) and, when promoted toward a claim, in a measurement or hypothesis structure.
HypothesisStatus is the discrete label that records how far a data-derived hypothesis has progressed through that pipeline. Sibling definitions supply the rest of the stack: data source and provenance records, measurement wrappers, and the DataHypothesis structure that carries a named claim together with its underlying measurement and this status.
Quarantine rules are strict: modules under Verification/Measurement/* stay quarantined; only preregistered test suites may import both the certified surface and the quarantine layer.
proof idea
No proof. The declaration is an inductive type with four nullary constructors, deriving DecidableEq and Repr. Classification is by construction; there are no lemmas to apply and no tactic script.
why it matters
It is the status field inside DataHypothesis, the explicit bridge between quarantined empirical data and anything that might later be cited as a certified claim. Without a status tag, the provenance layer could not distinguish an unchecked number from a preregistered or deprecated one, and the certified surface would have no mechanical way to refuse raw imports.
In the broader Recognition Science verification story this sits entirely on the measurement side of the wall: it does not touch the forcing chain (T0–T8), the Recognition Composition Law, or the mass ladder. Its job is institutional hygiene so that later claims about constants, thresholds, or PTA-style structural hypotheses can point at audited data rather than free-floating floats.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.