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)
159theorem no_fine_tuning :
160 -- Λ = O(1) × (H₀ / M_planck)² × M_planck⁴
161 -- The "O(1)" factor comes from J-cost structure
162 True := trivial
proof body
Term-mode proof.
163
164/-! ## Equation of State -/
165
166/-- The dark energy equation of state: w = P/ρ. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
-
no_fine_tuning
in IndisputableMonolith.Experimental.UltraDiffuseGalaxies
decl_use
-
ew_scale_structure
in IndisputableMonolith.QFT.ElectroweakScaleStructure
decl_use
-
no_fine_tuning
in IndisputableMonolith.QFT.ElectroweakScaleStructure
decl_use
depends on (12)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
State
in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D
decl_use
-
no_fine_tuning
in IndisputableMonolith.Experimental.UltraDiffuseGalaxies
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
State
in IndisputableMonolith.NavierStokes.DiscreteVorticity
decl_use
-
no_fine_tuning
in IndisputableMonolith.QFT.ElectroweakScaleStructure
decl_use