No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
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. -/
used by (8)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (22)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
Functionals
in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D
decl_use
-
tau0
in IndisputableMonolith.Compat.Constants
decl_use
-
tau0_pos
in IndisputableMonolith.Compat.Constants
decl_use
-
tau0
in IndisputableMonolith.Constants
decl_use
-
tau0_pos
in IndisputableMonolith.Constants
decl_use
-
tau0
in IndisputableMonolith.Constants.Derivation
decl_use
-
tau0_pos
in IndisputableMonolith.Constants.Derivation
decl_use
-
scale
in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS
decl_use
-
scale_pos
in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS
decl_use
-
Defect
in IndisputableMonolith.CPM.LNALBridge
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
energy_nonneg
in IndisputableMonolith.Foundation.NoetherTheoremDeep
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
energy_nonneg
in IndisputableMonolith.Thermodynamics.JCostThermoBridge
decl_use