Verification Measurement Data Provenance

The quarantine wall

Verification measurement data provenance is the bookkeeping system that keeps empirical facts from leaking into proved ones. In the Recognition Science framework, a machine-checked library of formal theorems separates what is proved from what is merely measured. The quarantine rule (an enforced separation between raw data and certified claims) wraps every measurement result, calibration constant, and mined dataset in a provenance record that tracks where the number came from, when it was recorded, and how it was generated.

The core object is a provenance record (a structured note attached to a number that says its source, timestamp, and version). Each record also carries a data source tag: manual entry, computation, external database, mining, or calibration. A measurement result bundles the value itself with an optional uncertainty bound and its provenance record. A completeness check requires that any computational result include both a generator script and a data hash, so a number produced by code cannot claim completeness without saying which code produced it and what input it digested.

The framework also defines a bridge from data to hypotheses. A data hypothesis takes a measured value, pairs it with a named falsifier (a concrete condition that would refute it) and a removal plan (how it would be withdrawn if that condition appeared), and marks its status as unverified, validated, preregistered, or deprecated. This turns a bare empirical number into a claim that knows how it could die. The quarantine rule is strict: modules in the verification measurement folder may not be imported by the certified surface, the layer of theorem-level claims. Test suites, however, may import both sides, which lets preregistered tests check the data without letting the data become a theorem.

In plain language, the framework establishes that a measured number is a citizen with a passport, not a vagrant. The library can point at a calibration constant and say exactly where it came from, what uncertainty it carries, and what would make it leave. That discipline matters because the framework's headline results, such as the forced cost function and the golden ratio scaling, are only as trustworthy as the wall that keeps them from depending on any particular empirical input. The wall is what lets the library claim that its theorems do not rest on the raw numbers that calibrate its models.

/-- Provenance record for empirical data.
    Every piece of data in the quarantine zone must have this. -/
structure DataProvenance where
  /-- Human-readable description -/
  description : String
  /-- Source type -/
  source : DataSource
  /-- SHA-256 hash of the data artifact (hex string) -/
  dataHash : String
  /-- Path to generator script (if computation/mining) -/
  generatorScript : Option String
  /-- Timestamp of data generation (ISO 8601) -/
  timestamp : String
  /-- Version identifier -/
  version : String
  /-- Additional metadata (key-value pairs) -/
  metadata : List (String × String)
  deriving Repr

/-- A hypothesis derived from empirical data.
    This is the bridge between quarantined data and certified claims. -/
structure DataHypothesis (α : Type*) where
  /-- Name of the hypothesis -/
  name : String
  /-- The claimed value -/
  claim : α
  /-- Underlying measurement -/
  measurement : MeasurementResult α
  /-- Current status -/
  status : HypothesisStatus
  /-- Falsification condition (what would disprove this) -/
  falsifier : String
  /-- Removal plan (how to make this a theorem) -/
  removalPlan : String

/-- Provenance record for empirical data.
    Every piece of data in the quarantine zone must have this. -/
structure DataProvenance where
  /-- Human-readable description -/
  description : String
  /-- Source type -/
  source : DataSource
  /-- SHA-256 hash of the data artifact (hex string) -/
  dataHash : String
  /-- Path to generator script (if computation/mining) -/
  generatorScript : Option String
  /-- Timestamp of data generation (ISO 8601) -/
  timestamp : String
  /-- Version identifier -/
  version : String
  /-- Additional metadata (key-value pairs) -/
  metadata : List (String × String)
  deriving Repr

What this page does not claim

The module does not prove any physical theorem; it only structures how empirical data is recorded and quarantined. No claim is made that the example constants (0.9, 0.01, 1.0, 2.0, 2.5) are physically meaningful; they are illustrative calibration values.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/Measurement/DataProvenance.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: