IndisputableMonolith.Relativity.Cosmology.FRWComponentsProbe

   1import Mathlib
   2
   3/-!
   4# FRW Componentwise Probe (panel-prescribed tractability test)
   5
   6Standalone probe, per the cosmo-chain panel verdict (2026-07-02): before locking
   7the full two-layer Friedmann skeleton, verify that the componentwise `Fin 4`
   8encoding of flat-FRW geometry is convergence-free differential algebra that
   9`simp` + `deriv` lemmas can actually discharge.
  10
  11Encoding: homogeneous flat FRW, k = 0, c = 1. Every field depends only on
  12cosmic time `t`, so spatial partials vanish identically and `∂₀ = deriv`.
  13
  14Probe goals:
  15* `Γ⁰ᵢᵢ = a·ȧ`  (the panel's named first probe)
  16* `Γⁱ₀ᵢ = ȧ/a`
  17
  18If these close, the full skeleton (Ricci, Einstein tensor, Friedmann I/II from a
  19named `EinsteinEqns` Prop) gets locked as loop targets. If they stall, re-encode
  20before locking anything.
  21-/
  22
  23namespace IndisputableMonolith
  24namespace Relativity
  25namespace Cosmology
  26namespace FRWComponentsProbe
  27
  28open Real
  29
  30/-- Flat FRW metric components (diagonal): `g₀₀ = -1`, `gᵢᵢ = a(t)²`. -/
  31noncomputable def gMetric (a : ℝ → ℝ) (μ ν : Fin 4) : ℝ → ℝ :=
  32  fun t => if μ = ν then (if μ = 0 then -1 else (a t) ^ 2) else 0
  33
  34/-- Inverse metric components (diagonal): `g⁰⁰ = -1`, `gⁱⁱ = 1/a(t)²`. -/
  35noncomputable def gInv (a : ℝ → ℝ) (μ ν : Fin 4) : ℝ → ℝ :=
  36  fun t => if μ = ν then (if μ = 0 then -1 else 1 / (a t) ^ 2) else 0
  37
  38/-- Coordinate partial derivative: `∂₀ = d/dt`, spatial partials vanish
  39(homogeneity). -/
  40noncomputable def pd (μ : Fin 4) (f : ℝ → ℝ) : ℝ → ℝ :=
  41  if μ = 0 then deriv f else 0
  42
  43/-- Christoffel symbols of the second kind,
  44`Γ^λ_{μν} = ½ Σ_σ g^{λσ} (∂_μ g_{νσ} + ∂_ν g_{μσ} − ∂_σ g_{μν})`. -/
  45noncomputable def Γ (a : ℝ → ℝ) (l m n : Fin 4) : ℝ → ℝ :=
  46  fun t => (1 / 2) * ∑ σ : Fin 4,
  47    gInv a l σ t *
  48      (pd m (gMetric a n σ) t + pd n (gMetric a m σ) t - pd σ (gMetric a m n) t)
  49
  50/-- The spatial metric component is `a²` (as a function). -/
  51@[simp] lemma gMetric_spatial (a : ℝ → ℝ) (i : Fin 4) (hi : i ≠ 0) :
  52    gMetric a i i = fun t => (a t) ^ 2 := by
  53  funext t; simp [gMetric, hi]
  54
  55/-- Off-diagonal metric components vanish. -/
  56@[simp] lemma gMetric_offdiag (a : ℝ → ℝ) {μ ν : Fin 4} (h : μ ≠ ν) :
  57    gMetric a μ ν = fun _ => 0 := by
  58  funext t; simp [gMetric, h]
  59
  60/-- Time derivative of `a²`: `d(a²)/dt = 2·a·ȧ` (stated in the lambda form the
  61metric simp lemma produces, so it chains in `simp`). -/
  62lemma deriv_a_sq (a : ℝ → ℝ) (ha : Differentiable ℝ a) (t : ℝ) :
  63    deriv (fun t => (a t) ^ 2) t = 2 * a t * deriv a t := by
  64  rw [show (fun t => (a t) ^ 2) = (fun x : ℝ => x ^ 2) ∘ a from rfl]
  65  rw [deriv_comp t (differentiable_pow 2).differentiableAt (ha t)]
  66  simp
  67
  68/-- **Probe 1**: `Γ⁰₁₁ = a·ȧ`. -/
  69theorem Γ_0_11 (a : ℝ → ℝ) (ha : Differentiable ℝ a) (t : ℝ) :
  70    Γ a 0 1 1 t = a t * deriv a t := by
  71  simp [Γ, gInv, pd, Fin.sum_univ_four, deriv_a_sq a ha]
  72  ring
  73
  74/-- **Probe 2**: `Γ¹₀₁ = ȧ·a / a²` (no division-by-zero commitment). -/
  75theorem Γ_1_01 (a : ℝ → ℝ) (ha : Differentiable ℝ a) (t : ℝ) :
  76    Γ a 1 0 1 t = deriv a t * a t / (a t) ^ 2 := by
  77  simp [Γ, gInv, pd, Fin.sum_univ_four, deriv_a_sq a ha,
  78        gMetric_offdiag a (show (1 : Fin 4) ≠ 2 by decide),
  79        gMetric_offdiag a (show (1 : Fin 4) ≠ 3 by decide),
  80        gMetric_offdiag a (show (0 : Fin 4) ≠ 1 by decide)]
  81  ring
  82
  83end FRWComponentsProbe
  84end Cosmology
  85end Relativity
  86end IndisputableMonolith
  87