defectMass

formal source

  65/-- Defect mass: measures deviation from the structured (Newtonian) solution.
  66    For ILG, this is the squared L² norm of (w - 1) weighted by the baryonic
  67    distribution, representing the "dark matter-like" modification. -/
  68noncomputable def defectMass (P : KernelParams) (s : ILGState) : ℝ :=
  69  let w := kernel P s.wavenumber s.scale
  70  (w - 1) ^ 2 * s.baryonicMass
  71
  72/-- Orthogonal mass: the projection onto the orthogonal complement of the
  73    Newtonian subspace. For ILG, this equals the defect mass scaled by
  74    the projection constant. -/
  75noncomputable def orthoMass (P : KernelParams) (s : ILGState) : ℝ :=
  76  defectMass P s
  77
  78/-- Energy gap: excess energy above the Newtonian ground state.
  79    Proportional to the integral of (∇w)² + potential terms. -/
  80noncomputable def energyGap (s : ILGState) : ℝ :=
  81  s.energy
  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,