IndisputableMonolith.CPM.Examples

   1import Mathlib
   2import IndisputableMonolith.CPM.LawOfExistence
   3
   4/-!
   5# CPM Examples and Unit Tests
   6
   7This module provides sample instantiations of the abstract CPM model,
   8demonstrating usage of the core theorems and validating the infrastructure.
   9
  10## Contents
  11
  121. Trivial model (all functionals zero) — baseline sanity check
  132. Subspace model (K_net = C_proj = 1) — tests the subspace shortcut
  143. RS cone model — tests the canonical RS constants
  154. Custom model — demonstrates typical domain instantiation pattern
  16
  17All examples include explicit verification that the core theorems apply.
  18-/
  19
  20namespace IndisputableMonolith
  21namespace CPM
  22namespace Examples
  23
  24open LawOfExistence
  25
  26/-! ## Example 1: Trivial Model -/
  27
  28/-- Trivial model: all functionals return zero.
  29This validates that the CPM inequalities hold vacuously. -/
  30def trivialModel : Model Unit := {
  31  C := {
  32    Knet := 1,
  33    Cproj := 1,
  34    Ceng := 1,
  35    Cdisp := 1,
  36    Knet_nonneg := by norm_num,
  37    Cproj_nonneg := by norm_num,
  38    Ceng_nonneg := by norm_num,
  39    Cdisp_nonneg := by norm_num
  40  },
  41  defectMass := fun _ => 0,
  42  orthoMass := fun _ => 0,
  43  energyGap := fun _ => 0,
  44  tests := fun _ => 0,
  45  projection_defect := by intro _; norm_num,
  46  energy_control := by intro _; norm_num,
  47  dispersion := by intro _; norm_num
  48}
  49
  50/-- Verify coercivity theorem applies to trivial model. -/
  51example : trivialModel.defectMass () ≤
  52    (trivialModel.C.Knet * trivialModel.C.Cproj * trivialModel.C.Ceng) *
  53    trivialModel.energyGap () :=
  54  trivialModel.defect_le_constants_mul_energyGap ()
  55
  56/-- Verify aggregation theorem applies to trivial model. -/
  57example : trivialModel.defectMass () ≤
  58    (trivialModel.C.Knet * trivialModel.C.Cproj * trivialModel.C.Cdisp) *
  59    trivialModel.tests () :=
  60  trivialModel.defect_le_constants_mul_tests ()
  61
  62/-! ## Example 2: Subspace Model -/
  63
  64/-- Subspace model: K_net = C_proj = 1, functionals satisfy equality.
  65This tests the subspace shortcut lemmas. -/
  66def subspaceModel : Model Unit := {
  67  C := {
  68    Knet := 1,
  69    Cproj := 1,
  70    Ceng := 2,
  71    Cdisp := 1,
  72    Knet_nonneg := by norm_num,
  73    Cproj_nonneg := by norm_num,
  74    Ceng_nonneg := by norm_num,
  75    Cdisp_nonneg := by norm_num
  76  },
  77  defectMass := fun _ => 1,
  78  orthoMass := fun _ => 1,
  79  energyGap := fun _ => 1,
  80  tests := fun _ => 2,
  81  projection_defect := by intro _; norm_num,
  82  energy_control := by intro _; norm_num,
  83  dispersion := by intro _; norm_num
  84}
  85
  86/-- Verify subspace shortcut: D ≤ orthoMass when K_net = C_proj = 1. -/
  87example : subspaceModel.defectMass () ≤ subspaceModel.orthoMass () :=
  88  Model.defect_le_ortho_of_Knet_one_Cproj_one subspaceModel rfl rfl ()
  89
  90/-- Verify subspace equality when orthoMass = defectMass. -/
  91example : subspaceModel.defectMass () = subspaceModel.orthoMass () :=
  92  Model.defect_eq_ortho_of_subspace_case subspaceModel rfl rfl (fun _ => rfl) ()
  93
  94/-! ## Example 3: RS Cone Constants Model -/
  95
  96/-- Model using the canonical RS cone constants. -/
  97def rsConeModel : Model Unit := {
  98  C := RS.coneConstants,
  99  defectMass := fun _ => 1,
 100  orthoMass := fun _ => 1,
 101  energyGap := fun _ => 2,
 102  tests := fun _ => 1,
 103  projection_defect := by
 104    intro _
 105    simp only [RS.cone_Knet_eq_one, RS.cone_Cproj_eq_two]
 106    norm_num,
 107  energy_control := by
 108    intro _
 109    simp only [RS.cone_Ceng_eq_one]
 110    norm_num,
 111  dispersion := by
 112    intro _
 113    simp only [RS.cone_Cdisp_eq_one]
 114    norm_num
 115}
 116
 117/-- Verify the RS model has positive constants. -/
 118lemma rsConeModel_pos :
 119    0 < rsConeModel.C.Knet ∧ 0 < rsConeModel.C.Cproj ∧ 0 < rsConeModel.C.Ceng := by
 120  refine ⟨?_, ?_, ?_⟩ <;> norm_num [rsConeModel, RS.coneConstants]
 121
 122/-- Verify coercivity with explicit c_min for RS model. -/
 123example : rsConeModel.energyGap () ≥ cmin rsConeModel.C * rsConeModel.defectMass () :=
 124  Model.energyGap_ge_cmin_mul_defect rsConeModel rsConeModel_pos ()
 125
 126/-- The RS cone coercivity constant is 1/2. -/
 127lemma rs_cone_cmin_value : cmin RS.coneConstants = 1 / 2 := by
 128  simp only [cmin, RS.cone_Knet_eq_one, RS.cone_Cproj_eq_two, RS.cone_Ceng_eq_one]
 129  norm_num
 130
 131/-! ## Example 4: Eight-Tick Net Constants Model -/
 132
 133/-- Model using the eight-tick aligned constants (K_net = (9/7)², C_proj = 2).
 134This matches the constants derived in the LaTeX support document. -/
 135noncomputable def eightTickModel : Model Unit := {
 136  C := {
 137    Knet := (9/7)^2,
 138    Cproj := 2,
 139    Ceng := 1,
 140    Cdisp := 1,
 141    Knet_nonneg := by norm_num,
 142    Cproj_nonneg := by norm_num,
 143    Ceng_nonneg := by norm_num,
 144    Cdisp_nonneg := by norm_num
 145  },
 146  defectMass := fun _ => 1,
 147  orthoMass := fun _ => 1,
 148  energyGap := fun _ => 4,
 149  tests := fun _ => 1,
 150  projection_defect := by
 151    intro _
 152    -- Need: 1 ≤ (9/7)^2 * 2 * 1
 153    have h : (1 : ℝ) ≤ (9/7)^2 * 2 := by norm_num
 154    linarith,
 155  energy_control := by intro _; norm_num,
 156  dispersion := by intro _; norm_num
 157}
 158
 159/-- The eight-tick coercivity constant is 49/162. -/
 160lemma eight_tick_cmin_value : cmin eightTickModel.C = 49 / 162 := by
 161  simp only [cmin, eightTickModel]
 162  norm_num
 163
 164/-- Verify positivity of eight-tick constants. -/
 165lemma eightTickModel_pos :
 166    0 < eightTickModel.C.Knet ∧ 0 < eightTickModel.C.Cproj ∧ 0 < eightTickModel.C.Ceng := by
 167  simp only [eightTickModel]
 168  norm_num
 169
 170/-- Verify coercivity applies to eight-tick model. -/
 171example : eightTickModel.energyGap () ≥ cmin eightTickModel.C * eightTickModel.defectMass () :=
 172  Model.energyGap_ge_cmin_mul_defect eightTickModel eightTickModel_pos ()
 173
 174/-! ## Demonstration: cpmsimp tactic -/
 175
 176/-- Demonstration that `cpmsimp` normalizes products correctly. -/
 177example (a b c d : ℝ) : a * b * c * d = a * (b * c) * d := by cpmsimp
 178
 179example (a b c : ℝ) : a * b * c = b * a * c := by cpmsimp
 180
 181end Examples
 182end CPM
 183end IndisputableMonolith
 184