theorem
proved
lambda_positive
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.DarkEnergy on GitHub at line 106.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
103 3 * H0^2 -- In natural units with c = 1
104
105/-- **THEOREM**: The cosmological constant is positive (repulsive). -/
106theorem lambda_positive : cosmologicalConstant > 0 := by
107 unfold cosmologicalConstant H0
108 norm_num
109
110/-! ## The Dark Energy Density -/
111
112/-- Critical density of the universe. -/
113noncomputable def criticalDensity : ℝ := 3 * H0^2 / (8 * Real.pi)
114
115/-- Dark energy density parameter Ω_Λ. -/
116noncomputable def omegaLambda : ℝ := 0.68 -- Observed value
117
118/-- The dark energy density. -/
119noncomputable def darkEnergyDensity : ℝ := omegaLambda * criticalDensity
120
121/-- **THEOREM**: Dark energy dominates the universe today. -/
122theorem dark_energy_dominates : omegaLambda > 0.5 := by
123 unfold omegaLambda
124 norm_num
125
126/-! ## Connection to J-Cost Structure -/
127
128/-- The fundamental origin of Λ: ledger tension per unit volume.
129
130 When space expands:
131 1. New "cells" appear in the 3D voxel lattice
132 2. Each cell requires ledger entries to maintain balance
133 3. The J-cost of these entries = dark energy density
134
135 Λ = (J-cost per entry) × (entry density) × (expansion rate)² -/
136noncomputable def lambdaFromJCost : ℝ :=