FRWCalibrated_hypothesis
plain-language theorem explainer
The declaration defines FRWCalibrated_hypothesis as the proposition asserting existence of a non-vanishing scale factor a together with matter and psi densities satisfying the first Friedmann equation. Cosmologists working inside the Recognition Science framework cite it to treat the ILG-to-FRW transition as an explicit modeling assumption. The definition is a direct existential statement over three real functions with two universal constraints and carries no proof obligations.
Claim. There exist functions $a, rho_matter, rho_psi : ℝ → ℝ$ such that $a(t) ≠ 0$ for all real $t$ and $(a'(t)/a(t))^2 = (8π/3)(rho_matter(t) + rho_psi(t))$ for all real $t$.
background
The module Relativity.ILG.FRW treats the passage from Indisputable Logic Geometry dynamics to the Friedmann-Robertson-Walker metric as a calibration step. The declaration encodes the hypothesis that this calibration has already been performed, keeping the step explicit rather than deriving it from the J-functional equation or the phi-ladder. The module is deliberately model-level, as stated in its documentation, until a full certificate is supplied from upstream results on the forcing chain.
proof idea
This is a definition, not a theorem. It introduces the proposition directly by an existential quantifier over three real-valued functions, followed by the non-vanishing condition on a and the equality constraint that reproduces the Friedmann equation. No lemmas or tactics are invoked; the body is the statement itself.
why it matters
The declaration supplies the interface assumption that lets downstream cosmological calculations inside the Recognition Science mirror proceed under standard FRW evolution. It stands in for the missing derivation from T5 J-uniqueness and T6 phi fixed point through the eight-tick octave to D=3. The open question it touches is the explicit certificate that ILG dynamics reduce to the observed Friedmann equation after calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.