Relativity Ilg Frw

The calibrated expansion

In general relativity, the Friedmann–Lemaître–Robertson–Walker (FLRW) metric describes a homogeneous, isotropic expanding universe. Its key equation relates the expansion rate, the scale factor a(t), to the energy density of matter and radiation. The standard form is (a'/a)² = (8π/3)(ρ_matter + ρ_radiation), where a' is the time derivative of the scale factor and ρ are densities. This is the starting point for modern cosmology, from the Big Bang model to dark energy.

The framework Recognition Science builds physical structure from a discrete record of recognition events, called a ledger. It has a machine-checked library of formal theorems, meaning each result is verified by a computer. Within this framework, the ILG module addresses how the ledger's internal geometry connects to the large-scale FLRW expansion. The module does not derive the expansion from first principles; instead, it states a hypothesis: the calibration step from the ILG (internal ledger geometry) to the FLRW form has been performed.

The module defines the property FRWCalibrated_hypothesis, which asserts that there exist functions a(t), ρ_matter(t), and ρ_psi(t) such that a(t) is never zero and the Friedmann equation holds for all times t. Here ρ_psi represents an additional energy density, possibly from a scalar field or other component. The definition is a formal statement of the standard cosmological equation, but it is intentionally model-level. The module keeps the calibration as an explicit assumption until a full derivation is formalized in the library, which remains an open target.

In plain language, the module says: if the ledger's internal geometry is to match the observed expanding universe, it must satisfy the same Friedmann equation that general relativity uses. The module sets up the equation as a testable hypothesis, not a proved theorem. It establishes the precise mathematical form that a future derivation must produce, and it flags the missing step. This is a useful checkpoint: it tells researchers exactly what the framework must eventually prove, and it does not overclaim what has not been shown.

/-- Hypothesis: the ILG→FRW calibration step has been performed.

This module is intentionally *model-level*: we keep the calibration as an explicit
assumption until a full derivation/certificate is formalized in Lean.
-/
def FRWCalibrated_hypothesis : Prop :=
  ∃ (a rho_matter rho_psi : ℝ → ℝ),
    (∀ t, a t ≠ 0) ∧
      (∀ t, (deriv a t / a t) ^ 2 = (8 * Real.pi / 3) * (rho_matter t + rho_psi t))

/-- Hypothesis: the ILG→FRW calibration step has been performed.

This module is intentionally *model-level*: we keep the calibration as an explicit
assumption until a full derivation/certificate is formalized in Lean.
-/
def FRWCalibrated_hypothesis : Prop :=
  ∃ (a rho_matter rho_psi : ℝ → ℝ),
    (∀ t, a t ≠ 0) ∧
      (∀ t, (deriv a t / a t) ^ 2 = (8 * Real.pi / 3) * (rho_matter t + rho_psi t))

What this page does not claim

The Friedmann equation is not proved from the framework; it is stated as a hypothesis. The ILG-to-FRW calibration is not derived; it remains an open target. No specific form for ρ_psi is given; it is only a placeholder for additional energy density.

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/ILG/FRW.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: