Gravity Full Efewith Dark Energy

The forced vacuum term

The cosmological constant, usually written Λ, is the simplest way to add dark energy to Einstein's field equations. It appears as a term proportional to the metric tensor, and it behaves like a fluid with negative pressure, pushing space apart. In the standard model of cosmology, Λ is a free parameter, chosen to match observations. Its measured value is tiny but positive, and it accounts for about 68 percent of the universe's energy budget.

In Recognition Science, the framework derives physical structure from a single starting point: reality keeps a ledger, a discrete record of recognition events. From this, a chain of theorems forces the golden ratio, an eight-tick cycle, and three spatial dimensions. The module Full EFE With Dark Energy extends this chain to gravity. It takes the standard Einstein field equations and inserts a cosmological constant that is not chosen but forced.

The framework proves that the vacuum term must be positive. It defines Λ_RS(H₀²) = 3 H₀² Ω_Λ, where H₀ is the Hubble constant and Ω_Λ = 11/16 − α/π. Since Ω_Λ is proved positive, and H₀² is positive, Λ_RS is positive. The module also proves that this Λ-extended data recovers the baseline when H₀² goes to zero, meaning the cosmological constant collapses back to zero. The coupling κ = 8φ⁵ and the dimension 4 are preserved; only the cosmological constant slot changes.

The equation of state for this vacuum is exactly w = −1. Writing the vacuum term as a perfect fluid gives density ρ_vac = Λ/κ and pressure p_vac = −ρ_vac. This is the static anchor that dynamic deviations from w = −1 are measured against. The module proves this is consistent with the Bianchi identity: a constant times the metric has vanishing covariant derivative because the metric is covariantly constant. This is the structural reason a cosmological constant is always consistent with ∇^μ G_μν = 0.

The absolute scale of Λ enters only through the input H₀² > 0. The dimensionless fraction Ω_Λ and every structural property are forced by the framework's logic. This is a theorem in the machine-checked library of formal theorems, with zero sorry and zero new axioms. The framework does not explain why H₀ has the value it does; that remains an input.

/-- `Λ_RS` is positive for any positive Hubble scale (forced by `Ω_Λ > 0`). -/
theorem Lambda_RS_pos {H0sq : ℝ} (h : 0 < H0sq) : 0 < Lambda_RS H0sq := by
  unfold Lambda_RS
  exact mul_pos (mul_pos (by norm_num : (0 : ℝ) < 3) h) Omega_Lambda_RS_pos

/-- The RS-forced dark-energy density fraction `Ω_Λ = 11/16 − α/π` is positive. -/
theorem Omega_Lambda_RS_pos :
    0 < Cosmology.CosmologicalConstantDerivation.Omega_Lambda_RS := by
  obtain ⟨hlo, _⟩ := Cosmology.CosmologicalConstantDerivation.Omega_Lambda_interval
  linarith

/-- The Λ-extended data recovers the baseline `Λ = 0` data in the limit. -/
theorem recovers_baseline_lambda :
    (rs_efe_data_with_lambda 0).cosmological_constant
      = FullEFE.rs_efe_data.cosmological_constant := by
  show Lambda_RS 0 = 0
  exact Lambda_RS_zero

/-- `Λ_RS` collapses to `0` in the `H₀² → 0` limit (recovers the baseline `Λ = 0`). -/
theorem Lambda_RS_zero : Lambda_RS 0 = 0 := by unfold Lambda_RS; ring

/-- **VACUUM EQUATION OF STATE IS `w = −1`.** The static vacuum fluid has `p/ρ = −1`. -/
theorem vacuum_eos (rho : ℝ) (h : rho ≠ 0) : vacuum_pressure rho / rho = -1 := by
  unfold vacuum_pressure
  rw [neg_div, div_self h]

/-- **VACUUM TERM IS COVARIANTLY CONSERVED (general).** For any metric-compatible setup,
the (0,2) tensor `c · g` (constant `c` times the metric) has vanishing covariant
derivative. With `c = −Λ/κ` this is the static vacuum stress tensor `T^vac = −(Λ/κ) g`, so
`∇_λ T^vac_μν = 0` for all indices, hence `∇^μ T^vac_μν = 0`. -/
theorem vacuum_stress_conserved (c : ℝ) (met : Connection.MetricTensor)
    (ch : Connection.ChristoffelData)
    (dg : Connection.Idx → Connection.Idx → Connection.Idx → ℝ)
    (hcompat : Connection.metric_compatibility met ch dg) :
    ∀ lam mu nu : Connection.Idx,
      covDeriv02 ch (fun a b => c * met.g a b) (fun a b d => c * dg a b d) lam mu nu = 0 := by
  intro lam mu nu
  rw [covDeriv02_smul]
  rw [show covDeriv02 ch met.g dg lam mu nu = (0 : ℝ) from hcompat lam mu nu]
  ring

/-- The flat Minkowski metric is covariantly constant: `∇_λ g_μν = 0`. Both the ordinary
derivative (constant metric) and the Christoffel symbols (flat) vanish. -/
theorem minkowski_metric_compatible :
    Connection.metric_compatibility Connection.minkowski
      (Connection.christoffel_from_metric Connection.minkowski_inverse (fun _ _ _ => 0))
      (fun _ _ _ => 0) := by
  unfold Connection.metric_compatibility
  intro lam mu nu
  simp [Connection.flat_christoffel_vanish]

What this page does not claim

This module does not derive the numerical value of the Hubble constant H₀; it takes H₀² as a positive input. This module does not claim that the cosmological constant is the only form of dark energy.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/FullEFEWithDarkEnergy.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: