structure
definition
SpacetimeRegion
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 73.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
70/-! ## Ledger Tension Model -/
71
72/-- A region of spacetime with ledger entries. -/
73structure SpacetimeRegion where
74 /-- Proper volume (in Planck units). -/
75 volume : ℝ
76 /-- Volume is positive. -/
77 volume_pos : volume > 0
78 /-- Number of ledger entries. -/
79 entries : ℕ
80 /-- Total J-cost of entries. -/
81 totalCost : ℝ
82
83/-- The ledger balance requirement: total cost should be zero. -/
84def isBalanced (R : SpacetimeRegion) : Prop := R.totalCost = 0
85
86/-- The ledger density: entries per unit volume. -/
87noncomputable def entryDensity (R : SpacetimeRegion) : ℝ := R.entries / R.volume
88
89/-- The cost density: J-cost per unit volume. -/
90noncomputable def costDensity (R : SpacetimeRegion) : ℝ := R.totalCost / R.volume
91
92/-! ## Expansion and Ledger Tension -/
93
94/-- When space expands, new volume appears that needs new entries.
95 The "tension" is the cost of creating entries to maintain balance. -/
96noncomputable def expansionTension (oldVolume newVolume : ℝ) (entryDensity : ℝ) : ℝ :=
97 (newVolume - oldVolume) * entryDensity * (Jcost phi)
98
99/-- The tension energy density is the cosmological constant. -/
100noncomputable def cosmologicalConstant : ℝ :=
101 -- Λ ≈ (energy to maintain ledger balance) / volume
102 -- This scales as H₀² due to the expansion rate
103 3 * H0^2 -- In natural units with c = 1