CosmologicalConstantCert
plain-language theorem explainer
The CosmologicalConstantCert structure records three facts that certify the RS-derived cosmological constant: the identity phi^5 equals 5 phi plus 3, positivity of lambdaRS defined as 8 phi^5 over 45, and its numerical placement in (1.88, 2.03). Cosmologists comparing Recognition Science predictions to Planck data would cite this certificate when discussing the implied Omega_Lambda near 0.685. It is assembled as a direct record of upstream lemmas with no additional reasoning steps.
Claim. The structure asserts the three properties $phi^5 = 5 phi + 3$, $0 < Lambda_{RS}$, and $1.88 < Lambda_{RS} < 2.03$, where $Lambda_{RS} := 8 phi^5 / 45$.
background
In Recognition Science the golden ratio phi is the self-similar fixed point forced at step T6 of the unified forcing chain. The module defines Lambda_RS as 8 phi^5 over 45 and states that this quantity lies in (1.88, 2.03) once the Fibonacci identity phi^5 = 5 phi + 3 is inserted. Upstream results supply the definition of lambdaRS and the theorem lambda_pos establishing positivity; the module doc quotes the prediction directly from OmegaLambdaBITKernelBand.lean.
proof idea
The structure is populated by direct field assignment from the three upstream facts phi5_eq, lambdaRS_pos, and lambdaRS_band. No tactics are executed inside the declaration; it functions as a record type that bundles the already-proved properties.
why it matters
This certificate feeds the downstream cosmologicalConstantCert definition, which enables explicit comparison of the RS Omega_Lambda value 0.685 against the Planck measurement 0.689. It closes the cosmological-constant prediction inside the RS framework by linking the phi-ladder identity to the observable ratio Lambda_RS over 3 H_0 squared. The module records zero sorrys and zero axioms, confirming the result follows from the core functional equation without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.