IndisputableMonolith.Verification.Exclusivity.ParameterSurface

   1import Mathlib
   2import IndisputableMonolith.Verification.Exclusivity.Framework
   3
   4namespace IndisputableMonolith
   5namespace Verification
   6namespace Exclusivity
   7
   8/-!
   9# Parameter Surface Formalization
  10
  11This module provides a **non-trivial** formalization of the "zero free parameters" claim.
  12
  13## The Problem with the Old Definition
  14
  15The old `HasZeroParameters := HasAlgorithmicSpec` definition captures "countable state space"
  16but doesn't capture "no adjustable numerical knobs" in the physics sense.
  17
  18A framework could have a countable state space but still contain a free parameter
  19(e.g., a coupling constant that can be set to any value).
  20
  21## New Approach: Parameter Records
  22
  231. **ParameterRecord**: A type representing the adjustable parameters of a framework
  242. **HasZeroParameters_Strong**: The parameter record is `PUnit` (unique/empty)
  253. **HasFreeKnob_Strong**: The parameter record contains at least one `ℝ` component
  26
  27## Key Insight
  28
  29A truly parameter-free framework has `ParameterRecord = PUnit`, meaning there is
  30exactly one way to configure it. A framework with free parameters has
  31`ParameterRecord = ℝ` or `ParameterRecord = ℝ × ℝ × ...`, meaning infinitely many
  32configurations are possible.
  33
  34-/
  35
  36open Framework
  37
  38/-! ### Parameter Record Type -/
  39
  40/-- A parameter record captures the adjustable numerical knobs of a physics framework.
  41
  42    For a zero-parameter framework, this should be `PUnit` (unique).
  43    For a framework with parameters, this could be `ℝ`, `ℝ × ℝ`, etc. -/
  44class HasParameterRecord (F : PhysicsFramework) where
  45  /-- The type of parameter configurations -/
  46  ParameterRecord : Type
  47  /-- How parameters affect the framework's evolution -/
  48  configure : ParameterRecord → (F.StateSpace → F.StateSpace)
  49  /-- The configuration is meaningful: different parameters give different evolution -/
  50  configure_injective : ∀ p₁ p₂ : ParameterRecord,
  51    configure p₁ = configure p₂ → p₁ = p₂
  52
  53namespace HasParameterRecord
  54
  55/-- A framework has zero free parameters if its parameter record is unique (PUnit). -/
  56def HasZeroParameters_Strong (F : PhysicsFramework) [HasParameterRecord F] : Prop :=
  57  Nonempty (ParameterRecord F ≃ PUnit.{1})
  58
  59/-- A framework has at least one free ℝ knob if ℝ embeds into its parameter record. -/
  60def HasFreeRealKnob (F : PhysicsFramework) [HasParameterRecord F] : Prop :=
  61  ∃ (embed : ℝ → ParameterRecord F), Function.Injective embed
  62
  63/-- Zero parameters and free knobs are mutually exclusive. -/
  64theorem zero_params_excludes_real_knob (F : PhysicsFramework) [HasParameterRecord F]
  65    (hZero : HasZeroParameters_Strong F)
  66    (hKnob : HasFreeRealKnob F) : False := by
  67  obtain ⟨eqv⟩ := hZero
  68  obtain ⟨embed, hInj⟩ := hKnob
  69  -- If ParameterRecord ≃ PUnit and ℝ ↪ ParameterRecord, then ℝ ↪ PUnit
  70  -- But PUnit has only one element, so ℝ cannot inject into it
  71  have h1 : ∀ x y : ℝ, eqv (embed x) = eqv (embed y) := fun _ _ => Subsingleton.elim _ _
  72  have h2 : ∀ x y : ℝ, embed x = embed y := fun x y => eqv.injective (h1 x y)
  73  -- Pick two different reals
  74  have hne : (0 : ℝ) ≠ 1 := by norm_num
  75  exact hne (hInj (h2 0 1))
  76
  77end HasParameterRecord
  78
  79/-! ### Example: Zero-Parameter Framework -/
  80
  81/-- A toy zero-parameter framework. -/
  82def toyZeroParamFramework : PhysicsFramework where
  83  StateSpace := Unit
  84  evolve := id
  85  Observable := Unit
  86  measure := id
  87  hasInitialState := ⟨()⟩
  88
  89/-- The toy framework has PUnit as its parameter record. -/
  90instance : HasParameterRecord toyZeroParamFramework where
  91  ParameterRecord := PUnit.{1}
  92  configure := fun _ => id
  93  configure_injective := fun _ _ _ => Subsingleton.elim _ _
  94
  95/-- The toy framework genuinely has zero parameters. -/
  96theorem toy_has_zero_params : HasParameterRecord.HasZeroParameters_Strong toyZeroParamFramework :=
  97  ⟨Equiv.refl PUnit.{1}⟩
  98
  99/-! ### Example: One-Parameter Framework -/
 100
 101/-- A framework with one free real parameter (coupling constant). -/
 102def oneParamFramework : PhysicsFramework where
 103  StateSpace := ℝ
 104  evolve := fun x => x  -- Trivial evolution for demonstration
 105  Observable := ℝ
 106  measure := id
 107  hasInitialState := ⟨0⟩
 108
 109/-- The one-parameter framework has ℝ as its parameter record (the coupling). -/
 110instance : HasParameterRecord oneParamFramework where
 111  ParameterRecord := ℝ
 112  configure := fun coupling => fun (x : ℝ) => coupling * x  -- Coupling affects evolution
 113  configure_injective := by
 114    intro p₁ p₂ h
 115    -- If configure p₁ = configure p₂, then p₁ * x = p₂ * x for all x
 116    have : (fun (x : ℝ) => p₁ * x) = (fun (x : ℝ) => p₂ * x) := h
 117    have h1 : p₁ * 1 = p₂ * 1 := congrFun this 1
 118    simp at h1
 119    exact h1
 120
 121/-- The one-parameter framework has a free real knob. -/
 122theorem oneParam_has_knob : HasParameterRecord.HasFreeRealKnob oneParamFramework :=
 123  ⟨id, fun _ _ h => h⟩
 124
 125/-- The one-parameter framework does NOT have zero parameters. -/
 126theorem oneParam_not_zero : ¬HasParameterRecord.HasZeroParameters_Strong oneParamFramework := by
 127  intro hZero
 128  exact HasParameterRecord.zero_params_excludes_real_knob oneParamFramework hZero oneParam_has_knob
 129
 130/-! ### Summary
 131
 132The `HasParameterRecord` typeclass and `HasZeroParameters_Strong` predicate provide
 133a **non-trivial** formalization:
 134
 135- `toyZeroParamFramework` satisfies `HasZeroParameters_Strong` ✓
 136- `oneParamFramework` does NOT satisfy `HasZeroParameters_Strong` ✗
 137- The two predicates are provably mutually exclusive
 138
 139This fixes the vacuity issue where the old `HasZeroParameters` was just
 140`HasAlgorithmicSpec`, which could be satisfied even by frameworks with free knobs.
 141-/
 142
 143end Exclusivity
 144end Verification
 145end IndisputableMonolith
 146