DataSource
plain-language theorem explainer
Enumerates the five allowed origins of empirical numbers inside the measurement quarantine: hand entry, computation, external APIs, dataset mining, and calibration. Anyone building a provenance record or a data-derived hypothesis cites it as the source tag. The declaration is a plain inductive with decidable equality and a printer; no proof content.
Claim. There is a finite type of data origins with five constructors: manual (researcher-entered), computation (machine-generated), external (database or API), mining (extracted from datasets), and calibration (tuning or optimization output). Equality of origins is decidable.
background
The module builds quarantine infrastructure so that certified, theorem-level claims never import raw empirical numbers. Every measurement, calibration constant, or mined dataset must sit behind a provenance record before it can touch a hypothesis bridge.
DataSource is the first piece of that record: a closed tag for where the artifact came from. Downstream, the provenance structure pairs this tag with a human description, a SHA-256 hash of the artifact, and generator metadata. Measurement wrappers and data-derived hypotheses then carry that full record.
Quarantine rules are strict: modules under Verification/Measurement/* may hold these records; the certified surface may not import them. Only preregistered test suites may see both sides.
proof idea
No proof. The declaration is an inductive type with five nullary constructors, deriving decidable equality and a representation instance. There is no tactic block and no lemma application.
why it matters
Without a closed source vocabulary, provenance records cannot force every quarantined value to declare its origin. This type is the source field of the provenance structure and is threaded into data-derived hypotheses, the bridge from empirical numbers to claims that may later be certified.
It does not itself touch the forcing chain (T0–T8), the Recognition Composition Law, or mass/ladder formulae. Its role is verification hygiene: keep empirical inputs out of the theorem surface until they are tagged, hashed, and explicitly hypothesized. Downstream structures (DataProvenance, DataHypothesis) depend on it as the mandatory origin tag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.