Relativity Cosmology Frwfriedmann

The Friedmann equations

The Friedmann equations are the standard starting point for modern cosmology. They describe how the scale factor, a(t), which measures the relative size of the universe, changes with time. In their simplest form, for a spatially flat universe, the first equation relates the expansion rate (the Hubble parameter, ā/a) to the energy density ρ: (ā/a)² = κρ/3. The second equation relates the acceleration of the expansion to both the energy density and the pressure p: ä/a = -κ(ρ + 3p)/6. Here κ is Einstein's gravitational constant, 8πG. These equations were first derived by Alexander Friedmann in 1922 and independently by Georges Lemaître in 1927, and they form the backbone of the standard Big Bang model.

The equations are not independent postulates. They follow from Albert Einstein's field equations of general relativity (1915), once one assumes the universe is homogeneous and isotropic on large scales, a symmetry encoded in the Friedmann–Lemaître–Robertson–Walker (FLRW) metric. The metric describes a universe that expands uniformly, with no preferred location or direction. The standard derivation writes down this metric, computes the curvature tensors, and then applies the Einstein equations with a perfect fluid as the source. The result is the two Friedmann equations above. This is a classical result, taught in every graduate cosmology course.

In Recognition Science, the framework's machine-checked library of formal theorems has formalized this derivation. The module FRWFriedmann (a formal development in the framework's library) defines the FLRW metric in a componentwise encoding, computes the Christoffel symbols, the Ricci tensor, the Ricci scalar, and the Einstein tensor, all as finite sums of time derivatives. It then defines the Einstein equations as a premise, honestly labeled as a MODEL input, together with a comoving perfect fluid. From these, the two Friedmann equations are derived as theorems, not definitions. The library proves, for example, that the 00-component of the Einstein tensor equals 3(ā/a)², and that the 11-component equals -(2aä + ā²). These component results are then assembled into the final Friedmann equations.

The formalization is a two-layer construction. The first layer is pure geometry: the FLRW metric and all its derived curvature quantities, with no physics assumed. The second layer adds the Einstein equations as an explicit hypothesis. The library proves that, given this hypothesis and a smooth, positive scale factor, the Friedmann equations follow. This is a theorem in the framework's library, with the proof checked by the machine. The key point is that the Friedmann equations are not taken as axioms; they are consequences of the Einstein equations on an FLRW background. This matches the standard physics derivation, but now with every step verified.

The module also includes a certificate theorem, friedmannCert, which packages both Friedmann equations into a single statement. It says that, for any smooth, positive scale factor, if the Einstein equations hold, then both Friedmann equations hold for all time. This is a clean statement of the result: the standard cosmological equations are a logical consequence of general relativity, within the framework's formal system. The practical consequence is that any further cosmological model built on the Friedmann equations can, in principle, be traced back to this verified foundation.

/-- Flat FRW metric components (diagonal): `g₀₀ = -1`, `gᵢᵢ = a(t)²`. -/
noncomputable def gMetric (a : ℝ → ℝ) (μ ν : Fin 4) : ℝ → ℝ :=
  fun t => if μ = ν then (if μ = 0 then -1 else (a t) ^ 2) else 0

/-- `G₀₀ = 3(ȧ/a)²` (the Friedmann-I side). -/
theorem einstein_00 (a : ℝ → ℝ) (ha : ContDiff ℝ 2 a) (hpos : ∀ t, 0 < a t)
    (t : ℝ) :
    EinsteinT a 0 0 t = 3 * (deriv a t / a t) ^ 2 := by
  have hne : a t ≠ 0 := (hpos t).ne'
  simp only [EinsteinT]
  rw [ricci_00 a ha hpos t, ricci_scalar_eq a ha hpos t]
  simp [gMetric]
  field_simp
  ring

/-- `G₁₁ = −(2a·ä + ȧ²)` (the Friedmann-II side). -/
theorem einstein_11 (a : ℝ → ℝ) (ha : ContDiff ℝ 2 a) (hpos : ∀ t, 0 < a t)
    (t : ℝ) :
    EinsteinT a 1 1 t = -(2 * a t * deriv (deriv a) t + (deriv a t) ^ 2) := by
  have hne : a t ≠ 0 := (hpos t).ne'
  simp only [EinsteinT]
  rw [ricci_11 a ha hpos t, ricci_scalar_eq a ha hpos t]
  simp [gMetric]
  field_simp
  ring

/-- **Friedmann I** from the Einstein equations on FRW:
`(ȧ/a)² = κρ/3`. -/
theorem friedmann_I (a ρ p : ℝ → ℝ) (κ : ℝ) (ha : ContDiff ℝ 2 a)
    (hpos : ∀ t, 0 < a t) (hEE : EinsteinEqns a ρ p κ) (t : ℝ) :
    (deriv a t / a t) ^ 2 = κ / 3 * ρ t := by
  have h00 := hEE 0 0 t
  rw [einstein_00 a ha hpos t] at h00
  simp [Tmn] at h00
  linarith

/-- **Friedmann II** (acceleration equation) from the Einstein equations on
FRW: `ä/a = −κ(ρ + 3p)/6`. -/
theorem friedmann_II (a ρ p : ℝ → ℝ) (κ : ℝ) (ha : ContDiff ℝ 2 a)
    (hpos : ∀ t, 0 < a t) (hEE : EinsteinEqns a ρ p κ) (t : ℝ) :
    deriv (deriv a) t / a t = -(κ / 6) * (ρ t + 3 * p t) := by
  have hne : a t ≠ 0 := (hpos t).ne'
  -- 00-equation: 3(ȧ/a)² = κρ, cleared: 3ȧ² = κρa²
  have h00 := hEE 0 0 t
  rw [einstein_00 a ha hpos t] at h00
  simp [Tmn] at h00
  have h00' : 3 * (deriv a t) ^ 2 = κ * ρ t * (a t) ^ 2 := by
    have := h00
    field_simp at this
    linarith
  -- 11-equation: −(2aä + ȧ²) = κ·p·a²
  have h11 := hEE 1 1 t
  rw [einstein_11 a ha hpos t] at h11
  simp [Tmn] at h11
  -- Combine: 2aä = −κpa² − ȧ² = −κpa² − κρa²/3
  have key : deriv (deriv a) t * a t
      = (-(κ / 6) * (ρ t + 3 * p t) * a t) * a t := by
    nlinarith [h00', h11]
  have h2 : deriv (deriv a) t = -(κ / 6) * (ρ t + 3 * p t) * a t :=
    mul_right_cancel₀ hne key
  rw [h2, mul_div_assoc, div_self hne, mul_one]

/-- Certificate bundling the two Friedmann theorems: from the named
`EinsteinEqns` premise (the honest GR import), both Friedmann equations
hold on any positive C² scale factor. -/
theorem friedmannCert :
    ∀ (a ρ p : ℝ → ℝ) (κ : ℝ), ContDiff ℝ 2 a → (∀ t, 0 < a t) →
      EinsteinEqns a ρ p κ →
      (∀ t, (deriv a t / a t) ^ 2 = κ / 3 * ρ t) ∧
      (∀ t, deriv (deriv a) t / a t = -(κ / 6) * (ρ t + 3 * p t)) := by
  intro a ρ p κ ha hpos hEE
  exact ⟨fun t => friedmann_I a ρ p κ ha hpos hEE t,
         fun t => friedmann_II a ρ p κ ha hpos hEE t⟩

What this page does not claim

The Einstein equations are not derived within the framework; they are assumed as a MODEL premise. This module does not prove the existence of a universe or the physical validity of the FLRW metric. The formalization does not include the derivation of the Friedmann equations for a non-flat universe with k ≠ 0.

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/Relativity/Cosmology/FRWFriedmann.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: