lambdaRS_band
plain-language theorem explainer
The theorem establishes that the RS cosmological constant satisfies 1.88 < Λ_RS < 2.03 in native units. Dark energy researchers comparing Recognition Science to Planck data would cite this interval for the dimensionless Ω_Λ ratio. The tactic proof substitutes the Fibonacci identity φ^5 = 5φ + 3 then reduces both sides of the conjunction via linear arithmetic on the supplied bounds 1.61 < φ < 1.62.
Claim. $1.88 < 8φ^5/45 < 2.03$
background
The CosmologicalConstantFromRS module states the RS prediction Λ_RS = 8φ^5/45 ∈ (1.88, 2.03) and supplies the dimensionless ratio Ω_Λ = Λ_RS / (3H₀²). Upstream, the definition lambdaRS encodes exactly this expression 8 * phi ^ 5 / 45. The theorem phi5_eq supplies the identity φ^5 = 5φ + 3, while phi_gt_onePointSixOne and phi_lt_onePointSixTwo give the tight numerical bounds on φ.
proof idea
The proof unfolds lambdaRS, substitutes φ^5 = 5φ + 3 from phi5_eq, then splits the conjunction. The lower bound applies div_lt_div_of_pos_right followed by nlinarith on the lower bound for φ and closes with linarith; the upper bound repeats the same steps with the upper bound for φ.
why it matters
This bound populates the lambda_band field inside both omegaLambdaBandCert and cosmologicalConstantCert. It supplies the concrete numerical verification required to certify the RS cosmological constant, consistent with the phi-ladder scaling and the eight-tick octave in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.