alpha_lt_half
plain-language theorem explainer
The measured fine-structure constant satisfies α < 1/2. Cosmology and GR-limit arguments cite it to keep the α/π correction below the geometric seed 11/16, so Ω_Λ stays positive and bounded. The proof unfolds the CODATA external anchor and closes by numeric evaluation.
Claim. With $\alpha$ the measured fine-structure constant (CODATA 2022 external anchor), one has $\alpha < 1/2$.
background
Module C-010 derives the dark-energy fraction from Recognition Science structure. The working formula is $\Omega_\Lambda = 11/16 - \alpha/\pi$, where $11/16$ is the geometric seed tied to the D=3 eight-tick ledger and gap-45 synchronization, and $\alpha/\pi$ is the IR electromagnetic correction.
In this file $\alpha$ is not the symbolic RS $\alpha$ from $\phi$; it is the single measured input alpha_CODATA $\approx 7.297\times 10^{-3}$. The same bound appears in the phase-saturation vacuum development, which likewise treats $\alpha$ as that external anchor. The inequality $\alpha < 1/2$ is the crude half-unit ceiling needed before dividing by $\pi$ or comparing to $11/16$.
proof idea
One-line numeric proof. Unfold the local $\alpha$ definition to the CODATA external anchor $7.2973525643\times 10^{-3}$, then norm_num discharges $\alpha < 1/2$ by concrete real arithmetic. No intermediate lemmas.
why it matters
Local parent: omega_lambda_positive uses this with $\pi > 1$ and $\alpha > 0$ to get $\alpha/\pi < \alpha < 1/2 < 11/16$, hence $\Omega_\Lambda = 11/16 - \alpha/\pi > 0$. Downstream phase-saturation results reuse the same ceiling for $\alpha/\pi < 11/16$ (seed) and the tighter $\alpha/\pi < 1/6$ (via $\pi > 3$).
In the framework this is the elementary gate that keeps the C-010 prediction inside the observed dark-energy window without fine-tuning: the geometric seed from T8 (D=3, eight-tick) minus a small $\alpha/\pi$ correction. A parallel GR-limit parameter bound (on the $\phi$-derived coupling, not this CODATA $\alpha$) plays an analogous role for perturbative smallness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.