Relativity Cosmology Frwcomponents Probe

A first step toward cosmic equations

The Friedmann equations describe how a homogeneous, isotropic universe expands or contracts over time. In the standard picture, the universe is filled with a smooth fluid, and its geometry is encoded in a metric, a rule for measuring distances and time intervals. For a flat universe, the metric takes the diagonal form with components g₀₀ = -1 and gᵢᵢ = a(t)², where a(t) is the scale factor, a function of cosmic time t alone. This is the starting point for the framework's recognition ledger, a discrete record of events, applied to cosmology.

The module called FRWComponentsProbe is a tractability test. Before attempting to prove the full Friedmann equations, the framework's machine-checked library of formal theorems verifies that its componentwise encoding of flat FRW geometry can actually handle the necessary calculus. The key simplification is homogeneity: every field depends only on time, so spatial partial derivatives vanish identically, and the time derivative ∂₀ is just the ordinary derivative d/dt. The probe defines the metric, its inverse, and the Christoffel symbols, the connection coefficients that describe how vectors change as they move along the spacetime.

The probe's two goals are explicit. First, it proves that the Christoffel symbol Γ⁰₁₁ equals a(t) · a'(t), where a' is the derivative of the scale factor. Second, it proves that Γ¹₀₁ equals a'(t) · a(t) / a(t)², stated without committing to division by zero. Both are simple consequences of the metric's diagonal form and the derivative rule d(a²)/dt = 2a·a'. The proofs are short: they expand the definitions, apply the chain rule, and simplify with algebra. The library's simplifier and derivative lemmas discharge them without trouble.

Why does this matter? These two Christoffel symbols are the first nontrivial pieces of the machinery needed to compute the Ricci tensor and the Einstein tensor, which in turn yield the Friedmann equations. The probe's success means the encoding is convergence-free differential algebra, a clean setup where the simplifier can close the goals. If the probe had stalled, the full skeleton would need re-encoding before locking anything. Since it closes, the path is clear to lock the full two-layer Friedmann skeleton as loop targets, including the Einstein equations as a named proposition.

In the framework's account, this is a small but necessary step. It does not yet derive the Friedmann equations or any cosmological prediction. It establishes that the geometric language, the metric, the connection, and the derivative rules, works as intended on the standard flat FRW background. The payoff is confidence: the foundation is sound enough to build the full cosmic equations on top of it.

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

What this page does not claim

The module does not derive the Friedmann equations or any cosmological prediction. The module does not prove the existence or uniqueness of the scale factor a(t). The module does not address the physical recognition-to-linking bridge for cosmology.

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/FRWComponentsProbe.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: