alpha
plain-language theorem explainer
Local alias for the CODATA 2022 fine-structure constant α ≈ 7.297×10⁻³, the single measured input in the C-010 cosmological-constant derivation. Cosmology proofs cite it inside Ω_Λ = 11/16 − α/π. The body is a one-line re-export of the external anchor, not a derived RS constant.
Claim. Define $\alpha \in \mathbb{R}$ to be the CODATA 2022 fine-structure constant $\alpha = 7.2973525643 \times 10^{-3}$, used as the unique measured electromagnetic input in the Recognition Science formula $\Omega_\Lambda = 11/16 - \alpha/\pi$.
background
Module C-010 attacks the cosmological-constant problem: QFT vacuum energy is ~10¹²⁰ too large, while observation gives Ω_Λ ≈ 0.7. Recognition Science replaces that with a geometric seed minus an IR correction,
$$\Omega_\Lambda = 11/16 - \alpha/\pi.$$
The seed 11/16 = 0.6875 comes from the D = 3 ledger (T8 eight-tick structure 2³ together with gap-45 synchronization; LCM(8,45) = 360 feeds the 11/16 fraction). The correction α/π is O(10⁻³) and uses the laboratory fine-structure constant rather than an RS-derived α.
Upstream, ExternalAnchors.alpha_CODATA freezes the CODATA 2022 value with relative uncertainty 1.5×10⁻¹⁰. Sibling modules (Constants.Alpha) also expose a symbolic α = 1/α_inv for pure RS formulas; this cosmology binding deliberately chooses the external anchor so the dark-energy prediction carries exactly one measured input.
proof idea
Definitional one-liner: bind the local name to Constants.ExternalAnchors.alpha_CODATA, itself the literal real 7.2973525643e-3. No lemmas, no tactics, no computation.
why it matters
C-010’s key formula needs a concrete α to turn the geometric seed 11/16 into a sharp Ω_Λ interval near 0.68. This binding is that input. Downstream siblings (Omega_Lambda_RS, positivity and upper-bound lemmas, the well-definedness certificate) all read through this name. Framework-wise it sits after T8 (D = 3, eight-tick octave) and the gap-45 ledger arithmetic that produce 11/16; the α/π term is the only non-forced piece. It also appears in the broader zero-parameter-status scaffold: unlike c, ℏ, G (RS-native), α here remains an external anchor, so the master “all constants derived” certificate still treats electromagnetic α as measured in this channel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.