cosmologicalConstantCert
plain-language theorem explainer
The definition assembles a certificate for the RS cosmological constant by supplying the phi^5 Fibonacci identity together with positivity and the interval bounds on lambdaRS. Cosmologists modeling dark energy from recognition science would cite this to obtain Lambda_RS in (1.88, 2.03) in native units. The construction is a direct record update that invokes three upstream theorems without additional reasoning steps.
Claim. Let phi denote the golden ratio. Define Lambda_RS = 8 phi^5 / 45. Then the certificate structure satisfies phi^5 = 5 phi + 3, 0 < Lambda_RS, and 1.88 < Lambda_RS < 2.03.
background
The module derives the cosmological constant from Recognition Science, stating Lambda_RS = 8 phi^5 / 45 lies in (1.88, 2.03). The key identity phi^5 = 5 phi + 3 follows from the Fibonacci recurrence for powers of phi. Upstream results include phi5_eq from DarkEnergyEquationOfStateDepth, HubbleTensionPipelineFromZAging, and InflatonPotentialStructural, each proving the identity by nlinarith after lower powers. lambdaRS_pos and lambdaRS_band from OmegaLambdaBITKernelBand establish positivity and the numerical band by unfolding lambdaRS and applying phi bounds.
proof idea
This is a definition that constructs the CosmologicalConstantCert record by assigning the phi5_val field to phi5_eq, the lambda_pos field to lambdaRS_pos, and the lambda_band field to lambdaRS_band. No further tactics are required.
why it matters
This definition supplies the concrete certificate for the RS prediction of the cosmological constant, which is used to compute the dark energy density parameter Omega_Lambda approx 0.685. It closes the chain from the phi-ladder (T5 J-uniqueness, T6 phi fixed point) to observable cosmology, matching the Planck value 0.689 within the stated band. The parent structure CosmologicalConstantCert formalizes the claim that Lambda_RS is positive and lies in the narrow interval derived from phi^5 = 5 phi + 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.