IndisputableMonolith.Foundation.OptionAEmpiricalProtocol

   1import Mathlib
   2import IndisputableMonolith.Foundation.OptionAFalsifierRegistry
   3
   4/-!
   5# Option A Empirical Protocol
   6
   7This module turns the falsifier registry into a Lean proposition:
   8every implemented C1-C9 combination has a dataset class, predicted observable,
   9and failure mode.
  10
  11The data mappings remain empirical metadata. The formal content here is total
  12coverage: no implemented Option A theorem is left without a falsifier protocol.
  13
  14Lean status: 0 sorry, 0 axiom.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Foundation
  19namespace OptionAEmpiricalProtocol
  20
  21open OptionAFalsifierRegistry
  22
  23/-- Complete empirical protocol record for one combination. -/
  24structure ProtocolSpec where
  25  dataset : DatasetClass
  26  observable : PredictedObservable
  27  failure : FailureMode
  28  deriving DecidableEq, Repr
  29
  30/-- The empirical protocol associated to a combination. -/
  31def protocolSpec (c : CombinationID) : ProtocolSpec where
  32  dataset := datasetClass c
  33  observable := predictedObservable c
  34  failure := failureMode c
  35
  36/-- A combination is protocol-falsifiable when it has a dataset class, a
  37predicted observable, and a failure mode in the registry. -/
  38def ProtocolFalsifiable (c : CombinationID) : Prop :=
  39  ∃ d : DatasetClass, ∃ o : PredictedObservable, ∃ f : FailureMode,
  40    datasetClass c = d ∧ predictedObservable c = o ∧ failureMode c = f
  41
  42theorem protocolFalsifiable_all (c : CombinationID) :
  43    ProtocolFalsifiable c := by
  44  unfold ProtocolFalsifiable
  45  exact ⟨datasetClass c, predictedObservable c, failureMode c, rfl, rfl, rfl⟩
  46
  47/-- A concrete protocol record matches a combination when all three fields agree. -/
  48def ProtocolMatches (c : CombinationID) (p : ProtocolSpec) : Prop :=
  49  p.dataset = datasetClass c ∧
  50    p.observable = predictedObservable c ∧
  51    p.failure = failureMode c
  52
  53theorem protocolSpec_matches (c : CombinationID) :
  54    ProtocolMatches c (protocolSpec c) := by
  55  simp [ProtocolMatches, protocolSpec]
  56
  57/-- Each implemented combination has a unique empirical protocol record. -/
  58theorem uniqueProtocolSpec (c : CombinationID) :
  59    ∃! p : ProtocolSpec, ProtocolMatches c p := by
  60  refine ⟨protocolSpec c, protocolSpec_matches c, ?_⟩
  61  intro p hp
  62  rcases p with ⟨d, o, f⟩
  63  rcases hp with ⟨hd, ho, hf⟩
  64  simp [protocolSpec] at hd ho hf ⊢
  65  exact ⟨hd, ho, hf⟩
  66
  67/-- Distinct combinations have distinct protocol records. -/
  68theorem protocolSpec_injective : Function.Injective protocolSpec := by
  69  intro a b h
  70  apply datasetClass_injective
  71  exact congrArg ProtocolSpec.dataset h
  72
  73/-- Equality of empirical protocols is exactly equality of combinations. -/
  74theorem protocolSpec_eq_iff (a b : CombinationID) :
  75    protocolSpec a = protocolSpec b ↔ a = b := by
  76  constructor
  77  · intro h
  78    exact protocolSpec_injective h
  79  · intro h
  80    rw [h]
  81
  82/-- Distinct combinations have distinct complete empirical protocols. -/
  83theorem protocolSpec_ne_of_ne {a b : CombinationID} (h : a ≠ b) :
  84    protocolSpec a ≠ protocolSpec b := by
  85  intro hp
  86  exact h (protocolSpec_injective hp)
  87
  88theorem c1_c3_protocol_distinct :
  89    protocolSpec .c1CognitiveTensor ≠ protocolSpec .c3OncologyTensor := by
  90  exact protocolSpec_ne_of_ne (by decide)
  91
  92theorem c3_c5_protocol_distinct :
  93    protocolSpec .c3OncologyTensor ≠ protocolSpec .c5AttentionTensor := by
  94  exact protocolSpec_ne_of_ne (by decide)
  95
  96theorem c5_c8_protocol_distinct :
  97    protocolSpec .c5AttentionTensor ≠ protocolSpec .c8MillerSpan := by
  98  exact protocolSpec_ne_of_ne (by decide)
  99
 100/-- A theorem bundle is empirically covered if every combination has a falsifier
 101protocol. -/
 102def EmpiricallyCovered : Prop :=
 103  ∀ c : CombinationID, ProtocolFalsifiable c
 104
 105theorem empiricallyCovered : EmpiricallyCovered :=
 106  protocolFalsifiable_all
 107
 108theorem c1_protocol :
 109    ProtocolFalsifiable .c1CognitiveTensor :=
 110  protocolFalsifiable_all .c1CognitiveTensor
 111
 112theorem c3_protocol :
 113    ProtocolFalsifiable .c3OncologyTensor :=
 114  protocolFalsifiable_all .c3OncologyTensor
 115
 116theorem c5_protocol :
 117    ProtocolFalsifiable .c5AttentionTensor :=
 118  protocolFalsifiable_all .c5AttentionTensor
 119
 120theorem c8_protocol :
 121    ProtocolFalsifiable .c8MillerSpan :=
 122  protocolFalsifiable_all .c8MillerSpan
 123
 124theorem c3_uniqueProtocol :
 125    ∃! p : ProtocolSpec, ProtocolMatches .c3OncologyTensor p :=
 126  uniqueProtocolSpec .c3OncologyTensor
 127
 128structure EmpiricalProtocolCert where
 129  all_covered : EmpiricallyCovered
 130  c1_covered : ProtocolFalsifiable .c1CognitiveTensor
 131  c3_covered : ProtocolFalsifiable .c3OncologyTensor
 132  c5_covered : ProtocolFalsifiable .c5AttentionTensor
 133  c8_covered : ProtocolFalsifiable .c8MillerSpan
 134  unique_protocol : ∀ c : CombinationID, ∃! p : ProtocolSpec, ProtocolMatches c p
 135  protocol_injective : Function.Injective protocolSpec
 136  c3_unique_protocol : ∃! p : ProtocolSpec, ProtocolMatches .c3OncologyTensor p
 137  protocol_eq_iff : ∀ a b : CombinationID, protocolSpec a = protocolSpec b ↔ a = b
 138  c1_c3_distinct : protocolSpec .c1CognitiveTensor ≠ protocolSpec .c3OncologyTensor
 139  c3_c5_distinct : protocolSpec .c3OncologyTensor ≠ protocolSpec .c5AttentionTensor
 140  c5_c8_distinct : protocolSpec .c5AttentionTensor ≠ protocolSpec .c8MillerSpan
 141
 142def empiricalProtocolCert : EmpiricalProtocolCert where
 143  all_covered := empiricallyCovered
 144  c1_covered := c1_protocol
 145  c3_covered := c3_protocol
 146  c5_covered := c5_protocol
 147  c8_covered := c8_protocol
 148  unique_protocol := uniqueProtocolSpec
 149  protocol_injective := protocolSpec_injective
 150  c3_unique_protocol := c3_uniqueProtocol
 151  protocol_eq_iff := protocolSpec_eq_iff
 152  c1_c3_distinct := c1_c3_protocol_distinct
 153  c3_c5_distinct := c3_c5_protocol_distinct
 154  c5_c8_distinct := c5_c8_protocol_distinct
 155
 156end OptionAEmpiricalProtocol
 157end Foundation
 158end IndisputableMonolith
 159