structure
definition
ILGState
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.ILG.CPMInstance on GitHub at line 45.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
Functionals -
tau0 -
tau0_pos -
tau0 -
tau0_pos -
tau0 -
tau0_pos -
scale -
scale_pos -
Defect -
of -
energy_nonneg -
is -
of -
from -
is -
of -
is -
of -
is -
energy_nonneg
used by
formal source
42/-- ILG configuration state: captures the gravitational field configuration
43 at a given scale. For the CPM formalization, we abstract this to
44 essential quantities needed for the coercivity bounds. -/
45structure ILGState where
46 /-- Scale factor a -/
47 scale : ℝ
48 /-- Wave number k -/
49 wavenumber : ℝ
50 /-- Reference time scale τ₀ -/
51 tau0 : ℝ
52 /-- Baryonic mass distribution (squared norm) -/
53 baryonicMass : ℝ
54 /-- Total energy of the configuration -/
55 energy : ℝ
56 /-- Positivity constraints -/
57 scale_pos : 0 < scale
58 wavenumber_pos : 0 < wavenumber
59 tau0_pos : 0 < tau0
60 baryonicMass_nonneg : 0 ≤ baryonicMass
61 energy_nonneg : 0 ≤ energy
62
63/-! ## ILG Functionals -/
64
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) : ℝ :=