omegaLambdaBandCert
plain-language theorem explainer
The definition assembles a certificate structure confirming that the golden ratio satisfies φ^5 = 5φ + 3, that the RS cosmological constant lambdaRS lies strictly between 1.88 and 2.03, and that it is positive. Researchers in Recognition Science cosmology cite this to certify the structural prediction for the cosmological constant against the observed band. It is assembled by direct assignment of three pre-established theorems into the structure fields.
Claim. An instance of the structure certifying φ^5 = 5φ + 3, 1.88 < λ_RS < 2.03, and λ_RS > 0 is defined by assigning the identity theorem to the first field, the interval theorem to the band field, and the positivity theorem to the final field, where λ_RS = 8φ^5/45.
background
The module states the RS prediction Λ_RS = 8φ^5/45 ∈ (1.88, 2.03) in native units, with the key Fibonacci identity φ^5 = 5φ + 3. The structure OmegaLambdaBandCert collects exactly these three properties: the identity, band membership of lambdaRS, and positivity. Upstream results include the theorem phi5_eq proving the identity via nlinarith on lower powers, lambdaRS_band proving the interval by unfolding lambdaRS and applying phi bounds, and lambdaRS_pos proving positivity via power and division rules.
proof idea
The definition constructs the structure by direct field assignment: phi5_value receives the theorem phi5_eq, lambda_band receives lambdaRS_band, and lambda_pos receives lambdaRS_pos. No tactics beyond the assignments are applied.
why it matters
This definition completes the formal bundling of the cosmological constant band in the OmegaLambdaBITKernelBand module, which derives from the BIT kernel arc-11. It supports cosmology pipelines that invoke the same phi5 identity, such as those in DarkEnergyEquationOfStateDepth and HubbleTensionPipelineFromZAging. Within the framework it instantiates the T5 J-uniqueness and phi fixed-point steps by confirming the numerical band for Lambda in RS units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.