`c_value_derivation`

proved

show as: view math explainer →

module: IndisputableMonolith.CPM.LawOfExistence
domain: CPM
line: 354 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CPM.LawOfExistence on GitHub at line 354.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 351
 352/-- Explicit computation: c_min = 1 / (K_net · C_proj · C_eng)
 353    = 1 / ((81/49) · 2 · 1) = 49 / 162. -/
 354theorem c_value_derivation :
 355    (1 : ℝ) / ((9/7)^2 * 2 * 1) = 49/162 := by
 356  norm_num
 357
 358/-- RS cone coercivity constant is 1/2. -/
 359theorem c_value_cone : cmin RS.coneConstants = 1/2 := by
 360  simp only [cmin, RS.cone_Knet_eq_one, RS.cone_Cproj_eq_two, RS.cone_Ceng_eq_one]
 361  norm_num
 362
 363end Bridge
 364
 365/-! ## Formal Constants Record
 366
 367A structured record of all CPM constants with their derivations,
 368suitable for auditing and JSON export. -/
 369
 370/-- Complete record of CPM constants with provenance. -/
 371structure CPMConstantsRecord where
 372  /-- Net/covering constant -/
 373  Knet : ℝ
 374  /-- Projection constant -/
 375  Cproj : ℝ
 376  /-- Energy control constant -/
 377  Ceng : ℝ
 378  /-- Dispersion constant -/
 379  Cdisp : ℝ
 380  /-- Coercivity constant c_min -/
 381  cmin : ℝ
 382  /-- Derivation source for K_net -/
 383  Knet_source : String
 384  /-- Derivation source for C_proj -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.