`c_value_cone`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CPM.LawOfExistence on GitHub at line 359.

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

 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 -/
 385  Cproj_source : String
 386  /-- Consistency check: c_min = 1/(K_net · C_proj · C_eng) -/
 387  cmin_consistent : cmin = (Knet * Cproj * Ceng)⁻¹
 388
 389/-- RS cone constants record. -/

papers checked against this theorem

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