IndisputableMonolith.Relativity.Cosmology.FRWFriedmann

   1import Mathlib
   2
   3/-!
   4# Friedmann Equations from Componentwise FRW Geometry (Target C skeleton)
   5
   6Panel-prescribed two-layer derivation (cosmo-chain panel verdict, 2026-07-02),
   7unlocked by the passing tractability probe `FRWComponentsProbe.lean`.
   8
   9**Layer 1 (geometry)**: flat FRW metric in componentwise `Fin 4` encoding,
  10Christoffel symbols, Ricci tensor, Ricci scalar, Einstein tensor. All are
  11finite `Fin 4` sums of time derivatives: convergence-free differential algebra.
  12
  13**Layer 2 (field equations)**: a named `EinsteinEqns` Prop (the GR input,
  14honestly a MODEL premise until the Einstein equations themselves are forced
  15upstream) plus a comoving perfect fluid, from which Friedmann I and II are
  16*theorems*, not definitions.
  17
  18This upgrades `Relativity.Cosmology.Friedmann`'s bare `Prop` definitions
  19(`FriedmannI`, `FriedmannII`) to derived consequences of the Einstein
  20equations on FRW.
  21
  22Conventions: signature (-,+,+,+), c = 1, spatial curvature k = 0,
  23`κ = 8πG`. Ricci: `R_{μν} = ∂_λ Γ^λ_{μν} − ∂_ν Γ^λ_{μλ}
  24+ Γ^λ_{λσ} Γ^σ_{μν} − Γ^λ_{νσ} Γ^σ_{μλ}`.
  25
  26Standard results being formalized (all classical GR):
  27* `Γ⁰ᵢᵢ = a·ȧ`, `Γⁱ₀ᵢ = ȧ/a`, all others zero
  28* `R₀₀ = −3ä/a`, `Rᵢᵢ = a·ä + 2ȧ²`
  29* `R = 6(ä/a + (ȧ/a)²)`
  30* `G₀₀ = 3(ȧ/a)²`, `Gᵢᵢ = −(2a·ä + ȧ²)`
  31* Friedmann I: `(ȧ/a)² = κρ/3`
  32* Friedmann II: `ä/a = −κ(ρ + 3p)/6`
  33
  34STATUS: skeleton with statement-fixed sorries; the cosmo-formalize loop
  35grinds these. The probe file has working proofs of the two Christoffel
  36component shapes.
  37-/
  38
  39namespace IndisputableMonolith
  40namespace Relativity
  41namespace Cosmology
  42namespace FRWFriedmann
  43
  44open Real
  45
  46/-! ## Layer 1: componentwise FRW geometry -/
  47
  48/-- Flat FRW metric components (diagonal): `g₀₀ = -1`, `gᵢᵢ = a(t)²`. -/
  49noncomputable def gMetric (a : ℝ → ℝ) (μ ν : Fin 4) : ℝ → ℝ :=
  50  fun t => if μ = ν then (if μ = 0 then -1 else (a t) ^ 2) else 0
  51
  52/-- Inverse metric components (diagonal): `g⁰⁰ = -1`, `gⁱⁱ = 1/a(t)²`. -/
  53noncomputable def gInv (a : ℝ → ℝ) (μ ν : Fin 4) : ℝ → ℝ :=
  54  fun t => if μ = ν then (if μ = 0 then -1 else 1 / (a t) ^ 2) else 0
  55
  56/-- Coordinate partial derivative: `∂₀ = d/dt`, spatial partials vanish
  57(homogeneity). -/
  58noncomputable def pd (μ : Fin 4) (f : ℝ → ℝ) : ℝ → ℝ :=
  59  if μ = 0 then deriv f else 0
  60
  61/-- Christoffel symbols of the second kind,
  62`Γ^λ_{μν} = ½ Σ_σ g^{λσ} (∂_μ g_{νσ} + ∂_ν g_{μσ} − ∂_σ g_{μν})`. -/
  63noncomputable def Γ (a : ℝ → ℝ) (l m n : Fin 4) : ℝ → ℝ :=
  64  fun t => (1 / 2) * ∑ σ : Fin 4,
  65    gInv a l σ t *
  66      (pd m (gMetric a n σ) t + pd n (gMetric a m σ) t - pd σ (gMetric a m n) t)
  67
  68/-- Ricci tensor from Christoffel symbols (componentwise, all sums finite):
  69`R_{μν} = ∂_λ Γ^λ_{μν} − ∂_ν Γ^λ_{μλ} + Γ^λ_{λσ} Γ^σ_{μν} − Γ^λ_{νσ} Γ^σ_{μλ}`. -/
  70noncomputable def RicciT (a : ℝ → ℝ) (μ ν : Fin 4) : ℝ → ℝ :=
  71  fun t =>
  72    (∑ l : Fin 4, pd l (Γ a l μ ν) t)
  73    - (∑ l : Fin 4, pd ν (Γ a l μ l) t)
  74    + (∑ l : Fin 4, ∑ σ : Fin 4, Γ a l l σ t * Γ a σ μ ν t)
  75    - (∑ l : Fin 4, ∑ σ : Fin 4, Γ a l ν σ t * Γ a σ μ l t)
  76
  77/-- Ricci scalar `R = g^{μν} R_{μν}`. -/
  78noncomputable def RicciScalarT (a : ℝ → ℝ) : ℝ → ℝ :=
  79  fun t => ∑ μ : Fin 4, ∑ ν : Fin 4, gInv a μ ν t * RicciT a μ ν t
  80
  81/-- Einstein tensor `G_{μν} = R_{μν} − ½ g_{μν} R`. -/
  82noncomputable def EinsteinT (a : ℝ → ℝ) (μ ν : Fin 4) : ℝ → ℝ :=
  83  fun t => RicciT a μ ν t - (1 / 2) * gMetric a μ ν t * RicciScalarT a t
  84
  85/-! ## Layer 2: matter and field equations -/
  86
  87/-- Comoving perfect fluid stress-energy, componentwise:
  88`T₀₀ = ρ`, `Tᵢᵢ = p·a²`, off-diagonal zero.
  89(This is `T_{μν} = (ρ+p) u_μ u_ν + p g_{μν}` with `u = ∂_t`.) -/
  90noncomputable def Tmn (a ρ p : ℝ → ℝ) (μ ν : Fin 4) : ℝ → ℝ :=
  91  fun t =>
  92    if μ = 0 ∧ ν = 0 then ρ t
  93    else if μ = ν then p t * (a t) ^ 2
  94    else 0
  95
  96/-- **The GR input (MODEL premise)**: the Einstein field equations hold
  97componentwise on this FRW background with coupling `κ = 8πG`. Friedmann I/II
  98are derived FROM this named premise; the premise itself remains the honest
  99import until the field equations are forced upstream. -/
 100def EinsteinEqns (a ρ p : ℝ → ℝ) (κ : ℝ) : Prop :=
 101  ∀ (μ ν : Fin 4) (t : ℝ), EinsteinT a μ ν t = κ * Tmn a ρ p μ ν t
 102
 103/-! ## Christoffel component values (statement-fixed targets) -/
 104
 105/-- `d(a²)/dt = 2·a·ȧ`, in the lambda form the metric produces (proved in the
 106probe file; reproved here so the module is self-contained). -/
 107lemma deriv_a_sq (a : ℝ → ℝ) (ha : Differentiable ℝ a) (t : ℝ) :
 108    deriv (fun t => (a t) ^ 2) t = 2 * a t * deriv a t := by
 109  rw [show (fun t => (a t) ^ 2) = (fun x : ℝ => x ^ 2) ∘ a from rfl]
 110  rw [deriv_comp t (differentiable_pow 2).differentiableAt (ha t)]
 111  simp
 112
 113/-- The `00` metric component is the constant `-1` (as a function). -/
 114@[simp] lemma gMetric_00 (a : ℝ → ℝ) : gMetric a 0 0 = fun _ => (-1 : ℝ) := by
 115  funext t; simp [gMetric]
 116
 117/-- The spatial metric component is `a²` (as a function). -/
 118@[simp] lemma gMetric_spatial (a : ℝ → ℝ) (i : Fin 4) (hi : i ≠ 0) :
 119    gMetric a i i = fun t => (a t) ^ 2 := by
 120  funext t; simp [gMetric, hi]
 121
 122/-- Off-diagonal metric components vanish. -/
 123@[simp] lemma gMetric_offdiag (a : ℝ → ℝ) {μ ν : Fin 4} (h : μ ≠ ν) :
 124    gMetric a μ ν = fun _ => 0 := by
 125  funext t; simp [gMetric, h]
 126
 127/-- `Γ⁰₀₀ = 0` (as a function; needed under `deriv` in the Ricci terms). -/
 128lemma christoffel_0_00 (a : ℝ → ℝ) : Γ a 0 0 0 = fun _ => 0 := by
 129  funext t
 130  simp [Γ, gInv, pd, gMetric, Fin.sum_univ_four]
 131
 132/-- `Γ⁰₁₁ = a·ȧ` as a function equation (probe proved it pointwise). -/
 133theorem christoffel_0_11 (a : ℝ → ℝ) (ha : Differentiable ℝ a) :
 134    Γ a 0 1 1 = fun t => a t * deriv a t := by
 135  funext t
 136  simp [Γ, gInv, pd, gMetric, Fin.sum_univ_four, deriv_a_sq a ha]
 137  ring
 138
 139/-- `Γ⁰₂₂ = a·ȧ`. -/
 140theorem christoffel_0_22 (a : ℝ → ℝ) (ha : Differentiable ℝ a) :
 141    Γ a 0 2 2 = fun t => a t * deriv a t := by
 142  funext t
 143  simp [Γ, gInv, pd, gMetric, Fin.sum_univ_four, deriv_a_sq a ha]
 144  ring
 145
 146/-- `Γ⁰₃₃ = a·ȧ`. -/
 147theorem christoffel_0_33 (a : ℝ → ℝ) (ha : Differentiable ℝ a) :
 148    Γ a 0 3 3 = fun t => a t * deriv a t := by
 149  funext t
 150  simp [Γ, gInv, pd, gMetric, Fin.sum_univ_four, deriv_a_sq a ha]
 151  ring
 152
 153/-- `Γ¹₀₁ = ȧ/a` (uses `a > 0` to cancel `a/a²`). -/
 154theorem christoffel_1_01 (a : ℝ → ℝ) (ha : Differentiable ℝ a)
 155    (hpos : ∀ t, 0 < a t) :
 156    Γ a 1 0 1 = fun t => deriv a t / a t := by
 157  funext t
 158  have hne : a t ≠ 0 := (hpos t).ne'
 159  simp [Γ, gInv, pd, gMetric, Fin.sum_univ_four, deriv_a_sq a ha]
 160  field_simp
 161
 162/-- `Γ²₀₂ = ȧ/a`. -/
 163theorem christoffel_2_02 (a : ℝ → ℝ) (ha : Differentiable ℝ a)
 164    (hpos : ∀ t, 0 < a t) :
 165    Γ a 2 0 2 = fun t => deriv a t / a t := by
 166  funext t
 167  have hne : a t ≠ 0 := (hpos t).ne'
 168  simp [Γ, gInv, pd, gMetric, Fin.sum_univ_four, deriv_a_sq a ha]
 169  field_simp
 170
 171/-- `Γ³₀₃ = ȧ/a`. -/
 172theorem christoffel_3_03 (a : ℝ → ℝ) (ha : Differentiable ℝ a)
 173    (hpos : ∀ t, 0 < a t) :
 174    Γ a 3 0 3 = fun t => deriv a t / a t := by
 175  funext t
 176  have hne : a t ≠ 0 := (hpos t).ne'
 177  simp [Γ, gInv, pd, gMetric, Fin.sum_univ_four, deriv_a_sq a ha]
 178  field_simp
 179
 180/-- Christoffel symbols are symmetric in the lower indices (definitional:
 181the bracket is symmetric under `m ↔ n`). -/
 182theorem christoffel_symm (a : ℝ → ℝ) (l m n : Fin 4) :
 183    Γ a l m n = Γ a l n m := by
 184  have hg : gMetric a m n = gMetric a n m := by
 185    by_cases h : m = n
 186    · subst h; rfl
 187    · rw [gMetric_offdiag a h, gMetric_offdiag a (Ne.symm h)]
 188  funext t
 189  simp only [Γ, hg]
 190  congr 1
 191  apply Finset.sum_congr rfl
 192  intro σ _
 193  ring
 194
 195/-! ## Derivative helpers (statement-fixed targets) -/
 196
 197/-- Quotient rule for the Hubble rate:
 198`d(ȧ/a)/dt = ä/a − (ȧ/a)²` in cleared form. -/
 199theorem deriv_hubble (a : ℝ → ℝ) (ha : ContDiff ℝ 2 a)
 200    (hpos : ∀ t, 0 < a t) (t : ℝ) :
 201    deriv (fun t => deriv a t / a t) t
 202      = (deriv (deriv a) t * a t - (deriv a t) ^ 2) / (a t) ^ 2 := by
 203  have h1 : DifferentiableAt ℝ (deriv a) t := ha.differentiable_deriv_two t
 204  have h2 : DifferentiableAt ℝ a t := (ha.differentiable (by norm_num)) t
 205  have hne : a t ≠ 0 := (hpos t).ne'
 206  have hfun : (fun t => deriv a t / a t) = deriv a / a := rfl
 207  rw [hfun, deriv_div h1 h2 hne]
 208  ring
 209
 210/-- Product rule for `a·ȧ`: `d(a·ȧ)/dt = ȧ² + a·ä`. -/
 211theorem deriv_a_adot (a : ℝ → ℝ) (ha : ContDiff ℝ 2 a) (t : ℝ) :
 212    deriv (fun t => a t * deriv a t) t
 213      = (deriv a t) ^ 2 + a t * deriv (deriv a) t := by
 214  have h1 : DifferentiableAt ℝ a t := (ha.differentiable (by norm_num)) t
 215  have h2 : DifferentiableAt ℝ (deriv a) t := ha.differentiable_deriv_two t
 216  have hfun : (fun t => a t * deriv a t) = a * deriv a := rfl
 217  rw [hfun, deriv_mul h1 h2]
 218  ring
 219
 220/-! ## Ricci and Einstein components (statement-fixed targets) -/
 221
 222/-- `R₀₀ = −3ä/a`. -/
 223theorem ricci_00 (a : ℝ → ℝ) (ha : ContDiff ℝ 2 a) (hpos : ∀ t, 0 < a t)
 224    (t : ℝ) :
 225    RicciT a 0 0 t = -3 * deriv (deriv a) t / a t := by
 226  have hd : Differentiable ℝ a := ha.differentiable (by norm_num)
 227  have hne : a t ≠ 0 := (hpos t).ne'
 228  simp only [RicciT, Fin.sum_univ_four]
 229  rw [christoffel_0_00 a, christoffel_1_01 a hd hpos, christoffel_2_02 a hd hpos,
 230      christoffel_3_03 a hd hpos]
 231  simp [Γ, gInv, pd, gMetric, Fin.sum_univ_four, deriv_a_sq a hd,
 232        deriv_hubble a ha hpos]
 233  field_simp
 234  ring
 235
 236/-- `Γ¹₁₀ = ȧ/a` (lower-index symmetric partner, needed pointwise in Ricci). -/
 237lemma christoffel_1_10 (a : ℝ → ℝ) (ha : Differentiable ℝ a)
 238    (hpos : ∀ t, 0 < a t) :
 239    Γ a 1 1 0 = fun t => deriv a t / a t := by
 240  rw [christoffel_symm a 1 1 0]; exact christoffel_1_01 a ha hpos
 241
 242/-- `R₁₁ = a·ä + 2ȧ²`. -/
 243theorem ricci_11 (a : ℝ → ℝ) (ha : ContDiff ℝ 2 a) (hpos : ∀ t, 0 < a t)
 244    (t : ℝ) :
 245    RicciT a 1 1 t = a t * deriv (deriv a) t + 2 * (deriv a t) ^ 2 := by
 246  have hd : Differentiable ℝ a := ha.differentiable (by norm_num)
 247  have hne : a t ≠ 0 := (hpos t).ne'
 248  simp only [RicciT, Fin.sum_univ_four]
 249  rw [christoffel_0_11 a hd]
 250  simp [Γ, gInv, pd, gMetric, Fin.sum_univ_four, deriv_a_sq a hd,
 251        deriv_a_adot a ha]
 252  field_simp
 253  ring
 254
 255/-- `R₂₂ = a·ä + 2ȧ²` (helper; same computation as `ricci_11`). -/
 256lemma ricci_22 (a : ℝ → ℝ) (ha : ContDiff ℝ 2 a) (hpos : ∀ t, 0 < a t)
 257    (t : ℝ) :
 258    RicciT a 2 2 t = a t * deriv (deriv a) t + 2 * (deriv a t) ^ 2 := by
 259  have hd : Differentiable ℝ a := ha.differentiable (by norm_num)
 260  have hne : a t ≠ 0 := (hpos t).ne'
 261  simp only [RicciT, Fin.sum_univ_four]
 262  rw [christoffel_0_22 a hd]
 263  simp [Γ, gInv, pd, gMetric, Fin.sum_univ_four, deriv_a_sq a hd,
 264        deriv_a_adot a ha]
 265  field_simp
 266  ring
 267
 268/-- `R₃₃ = a·ä + 2ȧ²` (helper; same computation as `ricci_11`). -/
 269lemma ricci_33 (a : ℝ → ℝ) (ha : ContDiff ℝ 2 a) (hpos : ∀ t, 0 < a t)
 270    (t : ℝ) :
 271    RicciT a 3 3 t = a t * deriv (deriv a) t + 2 * (deriv a t) ^ 2 := by
 272  have hd : Differentiable ℝ a := ha.differentiable (by norm_num)
 273  have hne : a t ≠ 0 := (hpos t).ne'
 274  simp only [RicciT, Fin.sum_univ_four]
 275  rw [christoffel_0_33 a hd]
 276  simp [Γ, gInv, pd, gMetric, Fin.sum_univ_four, deriv_a_sq a hd,
 277        deriv_a_adot a ha]
 278  field_simp
 279  ring
 280
 281/-- Ricci scalar `R = 6(ä/a + (ȧ/a)²)`. -/
 282theorem ricci_scalar_eq (a : ℝ → ℝ) (ha : ContDiff ℝ 2 a)
 283    (hpos : ∀ t, 0 < a t) (t : ℝ) :
 284    RicciScalarT a t
 285      = 6 * (deriv (deriv a) t / a t + (deriv a t / a t) ^ 2) := by
 286  have hne : a t ≠ 0 := (hpos t).ne'
 287  simp only [RicciScalarT, Fin.sum_univ_four]
 288  rw [ricci_00 a ha hpos t, ricci_11 a ha hpos t, ricci_22 a ha hpos t,
 289      ricci_33 a ha hpos t]
 290  simp [gInv]
 291  field_simp
 292  ring
 293
 294/-- `G₀₀ = 3(ȧ/a)²` (the Friedmann-I side). -/
 295theorem einstein_00 (a : ℝ → ℝ) (ha : ContDiff ℝ 2 a) (hpos : ∀ t, 0 < a t)
 296    (t : ℝ) :
 297    EinsteinT a 0 0 t = 3 * (deriv a t / a t) ^ 2 := by
 298  have hne : a t ≠ 0 := (hpos t).ne'
 299  simp only [EinsteinT]
 300  rw [ricci_00 a ha hpos t, ricci_scalar_eq a ha hpos t]
 301  simp [gMetric]
 302  field_simp
 303  ring
 304
 305/-- `G₁₁ = −(2a·ä + ȧ²)` (the Friedmann-II side). -/
 306theorem einstein_11 (a : ℝ → ℝ) (ha : ContDiff ℝ 2 a) (hpos : ∀ t, 0 < a t)
 307    (t : ℝ) :
 308    EinsteinT a 1 1 t = -(2 * a t * deriv (deriv a) t + (deriv a t) ^ 2) := by
 309  have hne : a t ≠ 0 := (hpos t).ne'
 310  simp only [EinsteinT]
 311  rw [ricci_11 a ha hpos t, ricci_scalar_eq a ha hpos t]
 312  simp [gMetric]
 313  field_simp
 314  ring
 315
 316/-! ## The Friedmann equations as theorems -/
 317
 318/-- **Friedmann I** from the Einstein equations on FRW:
 319`(ȧ/a)² = κρ/3`. -/
 320theorem friedmann_I (a ρ p : ℝ → ℝ) (κ : ℝ) (ha : ContDiff ℝ 2 a)
 321    (hpos : ∀ t, 0 < a t) (hEE : EinsteinEqns a ρ p κ) (t : ℝ) :
 322    (deriv a t / a t) ^ 2 = κ / 3 * ρ t := by
 323  have h00 := hEE 0 0 t
 324  rw [einstein_00 a ha hpos t] at h00
 325  simp [Tmn] at h00
 326  linarith
 327
 328/-- **Friedmann II** (acceleration equation) from the Einstein equations on
 329FRW: `ä/a = −κ(ρ + 3p)/6`. -/
 330theorem friedmann_II (a ρ p : ℝ → ℝ) (κ : ℝ) (ha : ContDiff ℝ 2 a)
 331    (hpos : ∀ t, 0 < a t) (hEE : EinsteinEqns a ρ p κ) (t : ℝ) :
 332    deriv (deriv a) t / a t = -(κ / 6) * (ρ t + 3 * p t) := by
 333  have hne : a t ≠ 0 := (hpos t).ne'
 334  -- 00-equation: 3(ȧ/a)² = κρ, cleared: 3ȧ² = κρa²
 335  have h00 := hEE 0 0 t
 336  rw [einstein_00 a ha hpos t] at h00
 337  simp [Tmn] at h00
 338  have h00' : 3 * (deriv a t) ^ 2 = κ * ρ t * (a t) ^ 2 := by
 339    have := h00
 340    field_simp at this
 341    linarith
 342  -- 11-equation: −(2aä + ȧ²) = κ·p·a²
 343  have h11 := hEE 1 1 t
 344  rw [einstein_11 a ha hpos t] at h11
 345  simp [Tmn] at h11
 346  -- Combine: 2aä = −κpa² − ȧ² = −κpa² − κρa²/3
 347  have key : deriv (deriv a) t * a t
 348      = (-(κ / 6) * (ρ t + 3 * p t) * a t) * a t := by
 349    nlinarith [h00', h11]
 350  have h2 : deriv (deriv a) t = -(κ / 6) * (ρ t + 3 * p t) * a t :=
 351    mul_right_cancel₀ hne key
 352  rw [h2, mul_div_assoc, div_self hne, mul_one]
 353
 354/-- Certificate bundling the two Friedmann theorems: from the named
 355`EinsteinEqns` premise (the honest GR import), both Friedmann equations
 356hold on any positive C² scale factor. -/
 357theorem friedmannCert :
 358    ∀ (a ρ p : ℝ → ℝ) (κ : ℝ), ContDiff ℝ 2 a → (∀ t, 0 < a t) →
 359      EinsteinEqns a ρ p κ →
 360      (∀ t, (deriv a t / a t) ^ 2 = κ / 3 * ρ t) ∧
 361      (∀ t, deriv (deriv a) t / a t = -(κ / 6) * (ρ t + 3 * p t)) := by
 362  intro a ρ p κ ha hpos hEE
 363  exact ⟨fun t => friedmann_I a ρ p κ ha hpos hEE t,
 364         fun t => friedmann_II a ρ p κ ha hpos hEE t⟩
 365
 366end FRWFriedmann
 367end Cosmology
 368end Relativity
 369end IndisputableMonolith
 370