OmegaLambdaBandCert
plain-language theorem explainer
The structure certifies that the RS cosmological constant Lambda_RS equals 8 phi^5 over 45 lies in the open interval from 1.88 to 2.03, given the identity phi^5 equals 5 phi plus 3 and strict positivity. Cosmologists using the Recognition Science framework cite it to confirm the predicted band for Omega_Lambda against Planck data. The definition assembles three independent upstream facts into a single record by direct field assignment.
Claim. Let $Lambda_RS := 8 phi^5 / 45$. The certificate asserts the Fibonacci relation $phi^5 = 5 phi + 3$, the open interval $1.88 < Lambda_RS < 2.03$, and the strict inequality $Lambda_RS > 0$.
background
The module sets the RS prediction Lambda_RS = 8 phi^5 / 45 inside the interval (1.88, 2.03). This rests on the identity phi^5 = 5 phi + 3, a direct Fibonacci relation on the phi-ladder. Upstream lambdaRS is defined exactly as that quotient, while positivity follows from the theorem that lambda exceeds zero once phi exceeds one.
proof idea
The declaration defines a structure whose three fields are filled by separate upstream results: the phi-five identity, the band inequality, and the positivity theorem.
why it matters
This certificate is consumed by the construction of omegaLambdaBandCert, which packages the band for downstream cosmology calculations. It realizes the RS structural prediction for the cosmological constant inside the eight-tick octave, placing the value inside the observed range for Omega_Lambda while respecting the phi-ladder constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.