alpha_pos_aux
plain-language theorem explainer
The measured fine-structure constant α (CODATA anchor) is strictly positive. Cosmology and weak-coupling bound lemmas cite it whenever they need 0 < α or 0 < α/π. The proof is a two-step numeric check: unfold the CODATA definition and discharge with norm_num.
Claim. The measured fine-structure constant satisfies $0 < \alpha$, where $\alpha$ is the CODATA 2022 external anchor $\alpha = 7.2973525643 \times 10^{-3}$.
background
In the phase-saturation cosmology module, the dark-energy fraction is identified with the equilibrium vacuum share of the discrete ledger:
$$\Omega_\Lambda = \frac{11}{16} - \frac{\alpha}{\pi}.$$
The geometric seed $11/16$ comes from Q₃ mode counting; the electromagnetic correction uses one measured input, the fine-structure constant. Locally alpha is defined as the CODATA 2022 anchor alpha_CODATA ($7.2973525643 \times 10^{-3}$), not the RS-derived symbolic $\alpha$.
Any lower or upper bound on $\Omega_\Lambda$ therefore needs elementary sign facts about $\alpha$ and $\alpha/\pi$. This private lemma supplies the base positivity $0 < \alpha$.
proof idea
Term-mode numeric proof. Unfold the local alpha definition to the external CODATA constant, then apply norm_num to the concrete decimal $7.2973525643 \times 10^{-3} > 0$. No algebraic lemmas are required.
why it matters
Feeds every subsequent positivity and bound step in the module: alpha_over_pi_pos ($0 < \alpha/\pi$), the local alias alpha_pos_local, and the unconditional lower bound Omega_Lambda_gt_068 ($\Omega_\Lambda > 0.68$). The same pattern appears in weak-coupling comparisons (alpha_W_gt_alpha, alpha_W_gt_two_alpha), which need $0 < \alpha$ when rearranging $\alpha_W = \alpha / \sin^2\theta_W$.
Within the Recognition chain this is scaffolding for the proved half of the $\Omega_\Lambda$ story (definition and numeric bounds). The still-open pieces are the hypotheses CosmicPhaseEquilibrium and vacuum_fraction_bridge that would identify the ledger vacuum fraction with cosmology; those do not depend on this lemma directly, but every numeric check that $\Omega_\Lambda$ lands near $0.685$ does.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.