alpha_seed_positive
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 in Recognition Science
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.
scope and limits
- Does not establish numerical bounds on α^{-1} itself.
- Does not incorporate curvature or gap corrections.
- Does not prove uniqueness of the seed value.
- Does not address higher-order terms beyond the seed definition.
Lean usage
theorem alphaInv_positive : 0 < alphaInv := by unfold alphaInv; exact mul_pos alpha_seed_positive (Real.exp_pos _)formal statement (Lean)
34theorem alpha_seed_positive : 0 < alpha_seed := by
proof body
One-line wrapper that applies unfold.
35 unfold alpha_seed; exact mul_pos (by norm_num) Real.pi_pos
36