lambdaRS_pos
plain-language theorem explainer
The theorem establishes that the RS cosmological constant Lambda_RS is strictly positive. Cosmologists deriving vacuum energy from the phi-ladder would cite it to confirm the sign before forming the dimensionless Omega_Lambda ratio. The proof is a term-mode reduction that unfolds the definition and applies standard positivity lemmas for multiplication, division, and powers.
Claim. $0 < 8 phi^5 / 45$ where $phi$ is the golden ratio satisfying $phi^5 = 5 phi + 3$.
background
In Recognition Science the cosmological constant is defined as Lambda_RS = 8 phi^5 / 45 with phi the self-similar fixed point obeying phi^2 = phi + 1. The module imports this definition from Cosmology.OmegaLambdaBITKernelBand and adds the ratio Omega_Lambda = Lambda_RS / (3 H_0^2) that yields approximately 0.685, close to the Planck value 0.689. Upstream results supply the explicit definition lambdaRS : R := 8 * phi ^ 5 / 45 together with phi_pos establishing phi > 0 and the Fibonacci identity phi^5 = 5 phi + 3.
proof idea
The term proof unfolds lambdaRS to expose the quotient 8 * phi^5 / 45, then applies div_pos to reduce the claim to positivity of the numerator, followed by mul_pos on the positive constant 8 and the term phi^5, and finally pow_pos using the already-established phi_pos lemma.
why it matters
The result is required by the certificate structures cosmologicalConstantCert and omegaLambdaBandCert that bundle phi5_eq, lambda_pos and lambda_band to certify the RS band (1.88, 2.03). It closes the sign verification step that follows the phi-ladder construction from T5 J-uniqueness and feeds directly into the comparison of the predicted Omega_Lambda with Planck data. No scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.