alpha_pos
plain-language theorem explainer
The fine-structure constant α used in the C-010 cosmological-constant formula is strictly positive. Bound lemmas for Ω_Λ = 11/16 − α/π cite it to get a positive correction term and a strict upper bound below the geometric seed. The proof unfolds the local α to the CODATA external anchor and discharges positivity by numeric evaluation.
Claim. Let $\alpha$ be the measured fine-structure constant used in this module (the CODATA 2022 external anchor). Then $0 < \alpha$.
background
Module C-010 derives the dark-energy fraction from Recognition Science as $\Omega_\Lambda = 11/16 - \alpha/\pi$. The seed $11/16$ comes from the D=3 ledger (eight-tick structure and gap-45 synchronization); $\alpha/\pi$ is the IR electromagnetic correction.
In this file, $\alpha$ is not the symbolic RS fine-structure formula. It is the single measured input Constants.ExternalAnchors.alpha_CODATA $\approx 7.297\times 10^{-3}$. Sibling lemmas need $0 < \alpha$ so that $\alpha/\pi > 0$ and the correction strictly lowers the geometric seed.
Upstream, Constants.Alpha.alpha is the symbolic $1/\alpha_{\mathrm{inv}}$ definition; the cosmology module deliberately pins to the external CODATA anchor instead.
proof idea
Term-mode proof by unfolding. Expand the local alpha to Constants.ExternalAnchors.alpha_CODATA, then run norm_num on the concrete decimal $7.2973525643\times 10^{-3}$. No algebraic lemmas are required; positivity is a pure numeric fact about the anchor.
why it matters
Private positivity fact for the C-010 chain. Downstream, omega_lambda_lt_11_16 uses $0 < \alpha/\pi$ (from this lemma and $\pi > 0$) plus linarith to get $\Omega_\Lambda^{\mathrm{RS}} < 11/16$. omega_lambda_positive uses it with $\alpha < 1/2$ to show the correction is smaller than the seed, hence $\Omega_\Lambda^{\mathrm{RS}} > 0$.
Those two bounds feed the public interval theorems (Omega_Lambda_bounds, Omega_Lambda_interval) that package the RS answer to the cosmological-constant problem: both terms are $O(1)$, their difference is forced near $0.68$, with no $10^{120}$ fine-tuning. Framework landmarks: T8 (D=3, eight-tick) supplies the $11/16$ seed; $\alpha$ is the measured EM input in the $\alpha^{-1}\in(137.030,137.039)$ band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.