isBalanced

formal source

  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
 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