omega_lambda_bare
plain-language theorem explainer
Bare RS dark-energy density fraction stored as the real constant 0.685177, the numerical value of 11/16 − α/π. Cosmologists comparing Planck Ω_Λ to the RS prediction cite it as the uncorrected baseline. It is a plain numeric definition, not a derived theorem.
Claim. The bare Recognition Science dark-energy density fraction is the real number $0.685177$, equal to $\frac{11}{16} - \frac{\alpha}{\pi}$.
background
The module forces the redshift kernel $K(z)$ in the dark-energy equation of state $w(z) = -1 + \delta w_0 \cdot K(z)$ from two premises: rung factorization of aging-charge attenuation across $\varphi$-rungs, and single-rung balance fixing the attenuation to $\varphi^{-1}$. The forced law is $\mathrm{occ}, n = \varphi^{-n}$, i.e. $1/(1+z)$ on the lattice $1+z = \varphi^n$, which pins the scale-free power to $s=1$ and yields a CPL form on the thawing line.
In that setting one needs a fixed RS baseline for the present-day dark-energy fraction $\Omega_\Lambda$ before any BIT kernel correction is applied. The bare value is the closed form $11/16 - \alpha/\pi$, here recorded as its decimal $0.685177$. Downstream comparison uses this number against both the maximum-amplitude corrected fraction and the Planck central value.
proof idea
Numeric definition: the real constant is set equal to $0.685177$ by a one-line assignment. No lemmas, tactics, or algebraic reduction are involved; the closed form $11/16 - \alpha/\pi$ is documented but not recomputed in the body.
why it matters
Feeds the retirement certificate omega_gap_explanation_retired, which shows that the maximum-amplitude BIT correction lands strictly below this bare value and farther from Planck in the adverse direction, while the forced kernel keeps $w(z)\ge -1$. That kills the hypothesis that BIT closes the Planck–RS $\Omega_\Lambda$ gap. The constant is therefore the fixed RS reference against which every admissible amplitude is measured. It sits in the cosmology layer of the forced-kernel paper, not in the T0–T8 chain, but it inherits $\varphi$-ladder structure through the rung law that forces $K(z)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.