IndisputableMonolith.Verification.Measurement.DataProvenance

   1import Mathlib
   2
   3/-!
   4# Data Provenance Infrastructure
   5
   6This module defines the **quarantine infrastructure** for empirical data.
   7All measurement results, calibration constants, and mined datasets must
   8be wrapped in provenance records.
   9
  10## Purpose
  11
  12The certified surface (theorem-level claims) must not depend on raw
  13empirical data. This module provides:
  14
  151. **DataProvenance**: Record tracking data source, hash, generator
  162. **MeasurementResult**: Wrapper for empirical values with provenance
  173. **HypothesisFromData**: Bridge between data and certified claims
  18
  19## Quarantine Rules
  20
  21- Modules in `Verification/Measurement/*` are **quarantined**
  22- The certified surface may NOT import quarantined modules
  23- Test suites (in `Verification/Preregistered/*`) may import both
  24
  25-/
  26
  27namespace IndisputableMonolith
  28namespace Verification
  29namespace Measurement
  30
  31/-! ## Provenance Records -/
  32
  33/-- Source type for empirical data. -/
  34inductive DataSource
  35  | manual         -- Hand-entered by researcher
  36  | computation    -- Generated by computation
  37  | external       -- From external database/API
  38  | mining         -- Extracted from datasets
  39  | calibration    -- Tuning/optimization result
  40  deriving DecidableEq, Repr
  41
  42/-- Provenance record for empirical data.
  43    Every piece of data in the quarantine zone must have this. -/
  44structure DataProvenance where
  45  /-- Human-readable description -/
  46  description : String
  47  /-- Source type -/
  48  source : DataSource
  49  /-- SHA-256 hash of the data artifact (hex string) -/
  50  dataHash : String
  51  /-- Path to generator script (if computation/mining) -/
  52  generatorScript : Option String
  53  /-- Timestamp of data generation (ISO 8601) -/
  54  timestamp : String
  55  /-- Version identifier -/
  56  version : String
  57  /-- Additional metadata (key-value pairs) -/
  58  metadata : List (String × String)
  59  deriving Repr
  60
  61/-- Create a provenance record for manual data. -/
  62def DataProvenance.manual (desc : String) (timestamp : String) : DataProvenance :=
  63  { description := desc
  64  , source := .manual
  65  , dataHash := ""  -- No hash for manual entry
  66  , generatorScript := none
  67  , timestamp := timestamp
  68  , version := "1.0"
  69  , metadata := []
  70  }
  71
  72/-- Create a provenance record for computed data. -/
  73def DataProvenance.computed (desc : String) (hash : String)
  74    (script : String) (timestamp : String) : DataProvenance :=
  75  { description := desc
  76  , source := .computation
  77  , dataHash := hash
  78  , generatorScript := some script
  79  , timestamp := timestamp
  80  , version := "1.0"
  81  , metadata := []
  82  }
  83
  84/-- Create a provenance record for calibration. -/
  85def DataProvenance.calibrated (desc : String) (timestamp : String)
  86    (method : String) : DataProvenance :=
  87  { description := desc
  88  , source := .calibration
  89  , dataHash := ""
  90  , generatorScript := none
  91  , timestamp := timestamp
  92  , version := "1.0"
  93  , metadata := [("method", method)]
  94  }
  95
  96/-! ## Measurement Results -/
  97
  98/-- A measurement result with provenance tracking. -/
  99structure MeasurementResult (α : Type*) where
 100  /-- The measured value -/
 101  value : α
 102  /-- Uncertainty/error bound (if applicable) -/
 103  uncertainty : Option ℝ
 104  /-- Provenance record -/
 105  provenance : DataProvenance
 106
 107/-- Extract just the value, discarding provenance. -/
 108def MeasurementResult.unwrap {α : Type*} (m : MeasurementResult α) : α := m.value
 109
 110/-- Map over a measurement result, preserving provenance. -/
 111def MeasurementResult.map {α β : Type*} (f : α → β)
 112    (m : MeasurementResult α) : MeasurementResult β :=
 113  { value := f m.value
 114  , uncertainty := m.uncertainty
 115  , provenance := m.provenance
 116  }
 117
 118/-! ## Hypothesis Bridge -/
 119
 120/-- Status of a hypothesis derived from data. -/
 121inductive HypothesisStatus
 122  | unverified    -- Data exists but not validated
 123  | validated     -- Data validated by independent check
 124  | preregistered -- Used in preregistered test suite
 125  | deprecated    -- Superseded by newer data
 126  deriving DecidableEq, Repr
 127
 128/-- A hypothesis derived from empirical data.
 129    This is the bridge between quarantined data and certified claims. -/
 130structure DataHypothesis (α : Type*) where
 131  /-- Name of the hypothesis -/
 132  name : String
 133  /-- The claimed value -/
 134  claim : α
 135  /-- Underlying measurement -/
 136  measurement : MeasurementResult α
 137  /-- Current status -/
 138  status : HypothesisStatus
 139  /-- Falsification condition (what would disprove this) -/
 140  falsifier : String
 141  /-- Removal plan (how to make this a theorem) -/
 142  removalPlan : String
 143
 144/-- Create a hypothesis from a measurement. -/
 145def DataHypothesis.fromMeasurement {α : Type*}
 146    (name : String) (m : MeasurementResult α)
 147    (falsifier : String) (plan : String) : DataHypothesis α :=
 148  { name := name
 149  , claim := m.value
 150  , measurement := m
 151  , status := .unverified
 152  , falsifier := falsifier
 153  , removalPlan := plan
 154  }
 155
 156/-! ## Calibration Constants (Quarantined) -/
 157
 158/-- Classification threshold for the audited classification interface.
 159    This is a **calibration constant**, not a derived value. -/
 160def classifyThreshold_raw : MeasurementResult ℝ :=
 161  { value := 0.9
 162  , uncertainty := some 0.05
 163  , provenance := DataProvenance.calibrated
 164      "Classification threshold for exact token match"
 165      "2026-01-06"
 166      "Manual tuning on canonical bases"
 167  }
 168
 169/-- Stability threshold for perturbation bounds.
 170    Derived from overlap perturbation analysis. -/
 171def stabilityThreshold_raw : MeasurementResult ℝ :=
 172  { value := 0.01
 173  , uncertainty := some 0.005
 174  , provenance := DataProvenance.computed
 175      "Stability threshold from Cauchy-Schwarz bound"
 176      ""  -- No hash yet
 177      "private calibration assumption ledger"
 178      "2026-01-06"
 179  }
 180
 181/-- Net constant for CPM coercivity. -/
 182def C_net_raw : MeasurementResult ℝ :=
 183  { value := 1.0
 184  , uncertainty := none
 185  , provenance := DataProvenance.calibrated
 186      "Optimized for intrinsic neutrality preservation"
 187      "2026-01-06"
 188      "Coercivity optimization"
 189  }
 190
 191/-- Projection constant for CPM. -/
 192def C_proj_raw : MeasurementResult ℝ :=
 193  { value := 2.0
 194  , uncertainty := none
 195  , provenance := DataProvenance.manual
 196      "Rank-one Hermitian bound"
 197      "2026-01-06"
 198  }
 199
 200/-- Energy control constant for CPM. -/
 201def C_eng_raw : MeasurementResult ℝ :=
 202  { value := 2.5
 203  , uncertainty := some 0.2
 204  , provenance := DataProvenance.calibrated
 205      "Empirical from diagnostic runs"
 206      "2026-01-06"
 207      "Energy diagnostic analysis"
 208  }
 209
 210/-! ## Hypotheses from Calibration -/
 211
 212/-- Hypothesis: classification threshold 0.9 is optimal. -/
 213def classifyThreshold_hypothesis : DataHypothesis ℝ :=
 214  DataHypothesis.fromMeasurement
 215    "classifyThreshold"
 216    classifyThreshold_raw
 217    "Different threshold achieves better accuracy"
 218    "Derive from stability analysis + information theory"
 219
 220/-- Hypothesis: stability threshold 0.01 is sufficient. -/
 221def stabilityThreshold_hypothesis : DataHypothesis ℝ :=
 222  DataHypothesis.fromMeasurement
 223    "stabilityThreshold"
 224    stabilityThreshold_raw
 225    "Perturbation changes classification within threshold"
 226    "Prove tight bound from overlap_perturbation_bound"
 227
 228/-! ## Provenance Validation -/
 229
 230/-- Check if provenance has all required fields. -/
 231def DataProvenance.isComplete (p : DataProvenance) : Bool :=
 232  p.description.length > 0 &&
 233  p.timestamp.length > 0 &&
 234  p.version.length > 0 &&
 235  (p.source ≠ .computation || p.generatorScript.isSome) &&
 236  (p.source ≠ .computation || p.dataHash.length > 0)
 237
 238/-- Check if a hypothesis is ready for preregistration. -/
 239def DataHypothesis.isPreregisterable {α : Type*} (h : DataHypothesis α) : Bool :=
 240  h.measurement.provenance.isComplete &&
 241  h.falsifier.length > 0 &&
 242  h.removalPlan.length > 0
 243
 244/-! ## Summary Report -/
 245
 246/-- Convert DataSource to string. -/
 247def DataSource.toString : DataSource → String
 248  | .manual => "manual"
 249  | .computation => "computation"
 250  | .external => "external"
 251  | .mining => "mining"
 252  | .calibration => "calibration"
 253
 254/-- List all calibration constants with their provenance. -/
 255def calibrationSummary : List (String × String × String) :=
 256  [ ("classifyThreshold", "0.9", classifyThreshold_raw.provenance.source.toString)
 257  , ("stabilityThreshold", "0.01", stabilityThreshold_raw.provenance.source.toString)
 258  , ("C_net", "1.0", C_net_raw.provenance.source.toString)
 259  , ("C_proj", "2.0", C_proj_raw.provenance.source.toString)
 260  , ("C_eng", "2.5", C_eng_raw.provenance.source.toString)
 261  ]
 262
 263-- #eval calibrationSummary  -- Disabled: ℝ not computable
 264
 265end Measurement
 266end Verification
 267end IndisputableMonolith
 268