alpha_seed_positive
plain-language theorem explainer
The theorem establishes that the geometric seed α_seed = 44π is strictly positive. Researchers constructing the exponential resummation for the inverse fine-structure constant cite this result to guarantee that α^{-1} stays positive throughout the refinement pipeline. The proof is a one-line wrapper that unfolds the definition and applies the positivity of multiplication to 44 and π.
Claim. $0 < 44π$, where α_seed is the geometric seed defined by 44π in the AlphaPrecision module.
background
In the AlphaPrecision module the seed is introduced as the noncomputable definition α_seed := 44 * Real.pi, matching the additive formula α^{-1}_add = 4π × 11 that supplies the baseline spherical closure cost. The module doc states the two RS formulas: the additive seed 4π × 11 ≈ 138.23 and the exponential resummation α^{-1} = α_seed × exp(−w₈ ln φ / α_seed), with the target interval (137.030, 137.039). Upstream, the Alpha module records the same seed as “Geometric seed from ledger structure: 4π·11. Represents the baseline spherical closure cost over 11-edge interaction paths.”
proof idea
The proof is a one-line wrapper. It unfolds alpha_seed to expose the product 44 * Real.pi, then applies mul_pos to the norm_num fact that 44 > 0 together with the library fact Real.pi_pos.
why it matters
This positivity result is invoked by alphaInv_positive, exp_factor_bounded, log_alphaInv_eq and alpha_precision_cert_exists in the AlphaExponentialForm and AlphaPrecision modules. It supplies the required positivity hypothesis for the exponential formula that narrows α^{-1} to the 60 ppm band around the CODATA value. Within the Recognition Science constants section it closes the positivity step that precedes curvature and gap corrections on the path to the certified alpha interval.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.