alpha
plain-language theorem explainer
Local alias for the CODATA 2022 fine-structure constant α ≈ 7.297×10⁻³, the single measured input in this cosmology module. Anyone citing the RS dark-energy formula Ω_Λ = 11/16 − α/π needs this anchor. The body is a one-line re-export of ExternalAnchors.alpha_CODATA.
Claim. Let $\alpha$ denote the measured electromagnetic fine-structure constant (CODATA 2022 value $\alpha = 7.2973525643 \times 10^{-3}$). In this module, $\alpha$ is that external anchor, used as the sole empirical input in the dark-energy fraction $\Omega_\Lambda = 11/16 - \alpha/\pi$.
background
The module PhaseSaturationVacuum derives the cosmological dark-energy fraction from discrete-ledger phase saturation. The core claim is that the equilibrium vacuum fraction equals a passive-mode fraction fixed by cube geometry, corrected by electromagnetism: $\Omega_\Lambda = 11/16 - \alpha/\pi \approx 0.6852$.
Here $\alpha$ is not derived inside the module. It is the measured fine-structure constant, imported from the external-anchor layer (CODATA 2022, relative uncertainty $1.5\times 10^{-10}$). A parallel definition exists in CosmologicalConstantDerivation with the same meaning: one measured input against an otherwise combinatorial geometric seed.
The geometric piece $11/16$ comes from proved mode counting (passive vs active modes on the $Q_3$ ledger geometry). The $\alpha/\pi$ term is the EM correction that shifts the pure geometric seed into the observed dark-energy band.
proof idea
No proof: this is a noncomputable definition. The right-hand side is Constants.ExternalAnchors.alpha_CODATA, itself the literal CODATA decimal $7.2973525643\times 10^{-3}$. The declaration is a module-local name binding so downstream formulas can write $\alpha$ without threading the external-anchor path.
why it matters
Without this anchor the RS prediction $\Omega_\Lambda = 11/16 - \alpha/\pi$ cannot be stated numerically or compared to observation. The module status list marks Omega_Lambda_RS bounds as proved once $\alpha$ is fixed; the open pieces are the hypotheses CosmicPhaseEquilibrium and vacuum_fraction_bridge that connect ledger saturation to cosmology.
In the broader framework, $\alpha$ is the fine-structure constant whose inverse sits in the RS band $(137.030, 137.039)$ when derived elsewhere; here it is deliberately the measured value so the dark-energy formula has exactly one empirical input. Downstream zero-parameter status scaffolding (e.g. mass-to-light certificates) treats $\alpha$ as among the constants that must eventually be fully derived rather than anchored.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.