alpha_over_pi_lt_seed
plain-language theorem explainer
The measured fine-structure constant over π sits strictly below the geometric seed 11/16. Cosmologists citing the RS dark-energy formula Ω_Λ = 11/16 − α/π need this inequality to guarantee a positive vacuum fraction. The proof is a short linarith chain: α > 0 and π > 1 give α/π < α, and α < 1/2 forces the ratio under 11/16.
Claim. With $\alpha$ the measured fine-structure constant (CODATA anchor), one has $\alpha/\pi < 11/16$.
background
This module identifies the cosmological dark-energy fraction with the equilibrium vacuum share of a phase-saturated discrete ledger: $\Omega_\Lambda = 11/16 - \alpha/\pi$. The seed $11/16$ is the passive-mode fraction from $Q_3$ cube geometry; the $\alpha/\pi$ term is the electromagnetic correction from the single measured input $\alpha$.
Locally, $\alpha$ is the CODATA anchor Constants.ExternalAnchors.alpha_CODATA. Two private facts are already on hand: $\alpha > 0$ (alpha_pos_local) and $\alpha < 1/2$ (alpha_lt_half, by norm_num on the anchor). The present inequality is the remaining arithmetic gate before positivity of $\Omega_\Lambda$.
proof idea
Three steps. First, $\pi > 3$ yields $\pi > 1$ by linarith. Second, positivity of $\alpha$ and $\pi > 1$ give $\alpha/\pi < \alpha$ via div_lt_self. Third, linarith closes with $\alpha < 1/2$: the chain $\alpha/\pi < \alpha < 1/2 < 11/16$ supplies the claim.
why it matters
Feeds directly into Omega_Lambda_pos, which unfolds $\Omega_\Lambda = 11/16 - \alpha/\pi$ and applies this bound by linarith to conclude $\Omega_\Lambda > 0$ (dark energy exists in the RS formula). That positivity is the first basic bound in the module's proved layer (Omega_Lambda_RS), sitting under the still-open hypotheses CosmicPhaseEquilibrium and vacuum_fraction_bridge that connect ledger saturation to cosmology. The seed $11/16$ itself is the proved combinatorial count geometric_seed_eq; this lemma only clears the EM correction so the difference stays positive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.