IndisputableMonolith.Verification.CminDerivationCert

   1import Mathlib
   2import IndisputableMonolith.CPM.LawOfExistence
   3
   4/-!
   5# c_min Derivation Certificate
   6
   7This certificate proves that the coercivity constants c_min are COMPUTED
   8from the derived CPM constants, not assumed.
   9
  10## The Formula
  11
  12c_min = 1 / (K_net · C_proj · C_eng)
  13
  14## Two Routes, Two Values
  15
  161. **Cone route**: c_min = 1/2
  17   - K_net = 1, C_proj = 2, C_eng = 1
  18   - c_min = 1/(1 · 2 · 1) = 1/2
  19
  202. **Eight-tick route**: c_min = 49/162
  21   - K_net = 81/49, C_proj = 2, C_eng = 1
  22   - c_min = 1/((81/49) · 2 · 1) = 49/162
  23
  24## Why This Matters
  25
  26c_min is the coercivity constant: energy_gap ≥ c_min · defect.
  27Larger c_min means stronger control. The cone route has better
  28coercivity (1/2 > 49/162) but the eight-tick is more explicit.
  29-/
  30
  31namespace IndisputableMonolith
  32namespace Verification
  33namespace CminDerivation
  34
  35open IndisputableMonolith.CPM.LawOfExistence
  36
  37structure CminDerivationCert where
  38  deriving Repr
  39
  40/-- Verification predicate: c_min values are computed from derived constants.
  41
  42Certifies:
  431. c_min = 1/2 for cone route
  442. c_min = 49/162 for eight-tick route
  453. Positivity for coercivity proofs
  464. Explicit computation formula
  47-/
  48@[simp] def CminDerivationCert.verified (_c : CminDerivationCert) : Prop :=
  49  -- Cone route: c_min = 1/2
  50  (cmin RS.coneConstants = 1/2) ∧
  51  -- Eight-tick route: c_min = 49/162
  52  (cmin Bridge.eightTickConstants = 49/162) ∧
  53  -- Positivity
  54  (0 < cmin RS.coneConstants) ∧
  55  (0 < cmin Bridge.eightTickConstants) ∧
  56  -- Cone has better coercivity than eight-tick
  57  (cmin RS.coneConstants > cmin Bridge.eightTickConstants)
  58
  59@[simp] theorem CminDerivationCert.verified_any (c : CminDerivationCert) :
  60    CminDerivationCert.verified c := by
  61  refine ⟨?cone_cmin, ?eight_cmin, ?cone_pos, ?eight_pos, ?cone_better⟩
  62  · exact Bridge.c_value_cone
  63  · exact Bridge.c_value_eight_tick
  64  · rw [Bridge.c_value_cone]; norm_num
  65  · rw [Bridge.c_value_eight_tick]; norm_num
  66  · rw [Bridge.c_value_cone, Bridge.c_value_eight_tick]; norm_num
  67
  68end CminDerivation
  69end Verification
  70end IndisputableMonolith
  71