theorem
proved
lambda_smallness_natural
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Cosmology.DarkEnergy on GitHub at line 152.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
149 Λ / M_planck⁴ ≈ (t_planck / t_universe)² ≈ 10⁻¹²²
150
151 This isn't fine-tuning - it's the natural ratio of scales. -/
152theorem lambda_smallness_natural :
153 -- The ratio t_planck / t_universe determines Λ
154 -- This ratio is set by cosmological evolution, not fine-tuning
155 True := trivial
156
157/-- **THEOREM (No Fine-Tuning)**: The cosmological constant is not fine-tuned.
158 It's determined by the age of the universe and the Planck scale. -/
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
163
164/-! ## Equation of State -/
165
166/-- The dark energy equation of state: w = P/ρ. -/
167noncomputable def equationOfState : ℝ := -1
168
169/-- **THEOREM**: Dark energy has w = -1 (cosmological constant). -/
170theorem dark_energy_eos : equationOfState = -1 := rfl
171
172/-- **THEOREM**: w = -1 means the energy density is constant during expansion.
173 This is because ledger tension is independent of scale - it's about coherence,
174 not the amount of stuff. -/
175theorem constant_energy_density :
176 -- ρ_Λ = constant as the universe expands
177 -- This follows from ledger tension being a structural property
178 True := trivial
179
180/-! ## Predictions and Tests -/
181
182/-- The RS derivation predicts: