alpha_over_pi_pos
plain-language theorem explainer
The fine-structure constant over π is strictly positive. Cosmology proofs that bound Ω_Λ = 11/16 − α/π from above by the geometric seed 11/16 cite this positivity. The argument is a one-line application of positivity of quotients to the already-established positivity of α and of π.
Claim. If $\alpha$ denotes the measured fine-structure constant used in this module, then $0 < \alpha/\pi$.
background
This module identifies the 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$ geometry; the correction subtracts the electromagnetic contribution measured by $\alpha$.
Here $\alpha$ is the CODATA fine-structure constant imported as a single measured input (Constants.ExternalAnchors.alpha_CODATA). An auxiliary lemma already records $0 < \alpha$ by unfolding that numeric anchor and evaluating. Real analysis supplies $0 < \pi$. The present statement only packages the quotient positivity needed for the $\Omega_\Lambda$ bounds.
proof idea
One-line term proof: apply Mathlib's div_pos to the two positivity facts alpha_pos_aux ($0 < \alpha$) and Real.pi_pos ($0 < \pi$). No further unfolding or numeric work is required at this step.
why it matters
Feeds directly into Omega_Lambda_lt_seed, which unfolds $\Omega_\Lambda = 11/16 - \alpha/\pi$ and uses this positivity with linarith to conclude $\Omega_\Lambda < 11/16$. That upper bound is the first half of the basic analytic control on the RS dark-energy prediction (the module also targets positivity and the subunitary bound $\Omega_\Lambda < 1$).
In the broader chain, the formula sits under the phase-saturation story: ledger capacity $\varphi^{45}$, equilibrium of matter and vacuum modes, and the geometric seed $11/16$. The bridge from ledger saturation to cosmology remains a named hypothesis (CosmicPhaseEquilibrium, vacuum_fraction_bridge); this lemma is pure real-arithmetic scaffolding inside the proved bound layer, not a resolution of those hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.