`tests`

definition

show as: view math explainer →

module: IndisputableMonolith.ILG.CPMInstance
domain: ILG
line: 85 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.ILG.CPMInstance on GitHub at line 85.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  82
  83/-- Test functional: supremum over local tests (for aggregation theorem).
  84    In the gravitational context, this represents local curvature bounds. -/
  85noncomputable def tests (P : KernelParams) (s : ILGState) : ℝ :=
  86  defectMass P s
  87
  88/-! ## CPM Constants for ILG -/
  89
  90/-- ILG-specific CPM constants derived from eight-tick geometry.
  91    - K_net = (9/7)² from ε = 1/8 covering
  92    - C_proj = 2 from J''(1) = 1 normalization
  93    - C_eng = 1 standard energy normalization
  94    - C_disp = 1 dispersion bound -/
  95noncomputable def ilgConstants : Constants := {
  96  Knet := (9/7)^2,
  97  Cproj := 2,
  98  Ceng := 1,
  99  Cdisp := 1,
 100  Knet_nonneg := by norm_num,
 101  Cproj_nonneg := by norm_num,
 102  Ceng_nonneg := by norm_num,
 103  Cdisp_nonneg := by norm_num
 104}
 105
 106/-- Alternative: RS cone constants (K_net = 1). -/
 107def ilgConeConstants : Constants := RS.coneConstants
 108
 109/-! ## CPM Model Instantiation -/
 110
 111/-- Energy control hypothesis: the energy of a configuration bounds its defect.
 112    This is the physical content of the variational principle (Lax-Milgram).
 113    In ILG, this states that the gravitational energy controls the deviation
 114    from the Newtonian solution. -/
 115def EnergyControlHypothesis (P : KernelParams) : Prop :=

papers checked against this theorem

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