IndisputableMonolith.Measurement.RSNative.Core

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# RS-Native Measurement Framework (Core)
   6
   7This module defines a **Lean-first** measurement scaffold for Recognition Science (RS).
   8
   9Design goals:
  10- **Core theory is RS-native**: ticks/voxels/coh/act + ledger observables, with \(τ₀ = 1\).
  11- **SI/CODATA is optional calibration**: lives outside core (`Constants.RSNativeUnits.ExternalCalibration`).
  12- **Protocols are explicit**: every measurement carries a protocol + falsifiers, so “arbitrary choices”
  13  (windowing, coarse-graining, basis choices) cannot be hidden.
  14
  15This file is intentionally small and dependency-light. Concrete observables live in
  16`IndisputableMonolith.Measurement.RSNative.Catalog.*`.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace Measurement
  21namespace RSNative
  22
  23/-! ## Protocol metadata -/
  24
  25inductive Status
  26  | spec
  27  | derived
  28  | hypothesis
  29  | scaffold
  30  deriving DecidableEq, Repr
  31
  32/-- A measurement protocol: how an RS observable is extracted from a state/trace. -/
  33structure Protocol where
  34  /-- Short protocol identifier (stable, machine-friendly). -/
  35  name : String
  36  /-- Human-readable summary. -/
  37  summary : String := ""
  38  /-- Claim hygiene for the extraction step. -/
  39  status : Status := .spec
  40  /-- Explicit assumptions (kept small and testable). -/
  41  assumptions : List String := []
  42  /-- Falsifiers: what would prove this protocol wrong. -/
  43  falsifiers : List String := []
  44
  45namespace Protocol
  46
  47/-- Protocol hygiene predicate (v1/v2).
  48
  49Rules:
  50- `name` must be non-empty
  51- if `status` is `.hypothesis` or `.scaffold`, both `assumptions` and `falsifiers` must be non-empty -/
  52def hygienic (p : Protocol) : Prop :=
  53  p.name ≠ "" ∧
  54    match p.status with
  55    | .hypothesis | .scaffold => p.assumptions ≠ [] ∧ p.falsifiers ≠ []
  56    | _ => True
  57
  58/-- Boolean check version of `Protocol.hygienic` (useful for audits). -/
  59def hygienicBool (p : Protocol) : Bool :=
  60  (!p.name.isEmpty) &&
  61    match p.status with
  62    | .hypothesis | .scaffold => (!p.assumptions.isEmpty) && (!p.falsifiers.isEmpty)
  63    | _ => true
  64
  65end Protocol
  66
  67/-! ## Time windows (ticks) -/
  68
  69/-- A discrete measurement window, expressed in ticks. -/
  70structure Window where
  71  /-- Start tick. -/
  72  t0 : Nat
  73  /-- Window length in ticks (0 = instantaneous). -/
  74  len : Nat
  75  deriving DecidableEq
  76
  77namespace Window
  78
  79@[simp] def instant (t : Nat) : Window := ⟨t, 0⟩
  80
  81@[simp] def stop (w : Window) : Nat := w.t0 + w.len
  82
  83end Window
  84
  85/-! ## Uncertainty and measurement record -/
  86
  87/-- Uncertainty semantics for scalar (real-valued) measurements.
  88
  89v1 used only `sigma`. v2 adds:
  90- interval bounds
  91- a finite discrete distribution scaffold
  92
  93This is intentionally lightweight: it is a *reporting seam* for measurement,
  94not a full probability theory. -/
  95inductive Uncertainty where
  96  /-- Symmetric 1σ uncertainty (standard deviation), in the same units as the value. -/
  97  | sigma (σ : ℝ) (hσ : 0 ≤ σ)
  98  /-- Interval uncertainty: the true value lies in `[lo, hi]`. -/
  99  | interval (lo hi : ℝ) (hlohi : lo ≤ hi)
 100  /-- Finite discrete distribution scaffold: list of `(value, weight)` pairs.
 101      We do not require proof obligations (nonneg/sum=1) in v2; protocols must state hygiene. -/
 102  | discrete (support : List (ℝ × ℝ))
 103
 104namespace Uncertainty
 105
 106@[simp] def sigmaVal : Uncertainty → Option ℝ
 107  | sigma σ _ => some σ
 108  | _ => none
 109
 110@[simp] def intervalBounds : Uncertainty → Option (ℝ × ℝ)
 111  | interval lo hi _ => some (lo, hi)
 112  | _ => none
 113
 114end Uncertainty
 115
 116/-- A measurement value with protocol + (optional) time window + (optional) uncertainty. -/
 117structure Measurement (α : Type) where
 118  value : α
 119  window : Option Window := none
 120  protocol : Protocol
 121  uncertainty : Option Uncertainty := none
 122  notes : List String := []
 123
 124namespace Measurement
 125
 126/-- Map the value of a measurement, preserving window/protocol/uncertainty/notes. -/
 127def map {α β : Type} (f : α → β) (m : Measurement α) : Measurement β :=
 128  { value := f m.value
 129    window := m.window
 130    protocol := m.protocol
 131    uncertainty := m.uncertainty
 132    notes := m.notes
 133  }
 134
 135/-- Map the value and replace protocol (e.g., when you derive a new observable). -/
 136def mapWithProtocol {α β : Type} (f : α → β) (p : Protocol) (m : Measurement α) : Measurement β :=
 137  { value := f m.value
 138    window := m.window
 139    protocol := p
 140    uncertainty := m.uncertainty
 141    notes := m.notes
 142  }
 143
 144/-- Transform the uncertainty record (when present). -/
 145def mapUncertainty {α : Type} (uMap : Uncertainty → Uncertainty) (m : Measurement α) : Measurement α :=
 146  { value := m.value
 147    window := m.window
 148    protocol := m.protocol
 149    uncertainty := m.uncertainty.map uMap
 150    notes := m.notes
 151  }
 152
 153def addNote {α : Type} (note : String) (m : Measurement α) : Measurement α :=
 154  { m with notes := m.notes ++ [note] }
 155
 156def addNotes {α : Type} (notes : List String) (m : Measurement α) : Measurement α :=
 157  { m with notes := m.notes ++ notes }
 158
 159end Measurement
 160
 161/-- An observable extracts a `Measurement α` from some state type `S`. -/
 162abbrev Observable (S α : Type) : Type := S → Measurement α
 163
 164/-! ## Tagged quantities (type-safe units) -/
 165
 166/-- A real-valued quantity tagged with a unit/semantic label. -/
 167structure Quantity (U : Type) where
 168  val : ℝ
 169
 170instance (U : Type) : CoeTC (Quantity U) ℝ := ⟨Quantity.val⟩
 171
 172namespace Quantity
 173
 174instance (U : Type) : Zero (Quantity U) := ⟨⟨0⟩⟩
 175instance (U : Type) : Add (Quantity U) := ⟨fun a b => ⟨a.val + b.val⟩⟩
 176instance (U : Type) : Sub (Quantity U) := ⟨fun a b => ⟨a.val - b.val⟩⟩
 177instance (U : Type) : Neg (Quantity U) := ⟨fun a => ⟨-a.val⟩⟩
 178instance (U : Type) : SMul ℝ (Quantity U) := ⟨fun r a => ⟨r * a.val⟩⟩
 179
 180@[simp] theorem val_zero (U : Type) : (0 : Quantity U).val = 0 := rfl
 181@[simp] theorem val_add {U : Type} (a b : Quantity U) : (a + b).val = a.val + b.val := rfl
 182@[simp] theorem val_sub {U : Type} (a b : Quantity U) : (a - b).val = a.val - b.val := rfl
 183@[simp] theorem val_neg {U : Type} (a : Quantity U) : (-a).val = -a.val := rfl
 184@[simp] theorem val_smul {U : Type} (r : ℝ) (a : Quantity U) : (r • a).val = r * a.val := rfl
 185
 186end Quantity
 187
 188/-! ### Unit/semantic tags (empty types) -/
 189
 190inductive TickUnit : Type
 191inductive VoxelUnit : Type
 192inductive CohUnit : Type
 193inductive ActUnit : Type
 194inductive CostUnit : Type
 195inductive SkewUnit : Type
 196inductive MeaningUnit : Type
 197inductive QualiaUnit : Type
 198inductive ZUnit : Type
 199
 200abbrev Tick := Quantity TickUnit
 201abbrev Voxel := Quantity VoxelUnit
 202abbrev Coh := Quantity CohUnit
 203abbrev Act := Quantity ActUnit
 204abbrev Cost := Quantity CostUnit
 205abbrev Skew := Quantity SkewUnit
 206abbrev Meaning := Quantity MeaningUnit
 207abbrev Qualia := Quantity QualiaUnit
 208abbrev ZCharge := Quantity ZUnit
 209
 210end RSNative
 211end Measurement
 212end IndisputableMonolith
 213