alpha_seed_positive
plain-language theorem explainer
alpha_seed_positive establishes that the geometric seed 4π·11 is strictly positive. Researchers modeling the inverse fine-structure constant via the exponential form α⁻¹ = α_seed · exp(−f_gap/α_seed) cite it to guarantee the physical value remains positive. The term proof unfolds the definition and reduces the inequality via the known positivity of π together with linarith.
Claim. $0 < 4π · 11$
background
In the Alpha Exponential Form module the canonical expression for the inverse fine-structure constant is α⁻¹ = α_seed · exp(−f_gap/α_seed), where α_seed = 4π·11. The seed is the baseline spherical closure cost over 11-edge interaction paths, as defined in the Alpha module. The present module proves positivity of α⁻¹, identifies the constant logarithmic derivative d ln(α⁻¹)/d(f_gap) = −1/α_seed, and records that the exponential Taylor structure is motivated by the J-cost log-coordinate expansion but not yet shown to be unique.
proof idea
The proof is a term-mode wrapper. It unfolds the definition of alpha_seed to 4 * Real.pi * 11, asserts 0 < Real.pi via Real.pi_pos, and closes the strict inequality with linarith.
why it matters
The result supplies the positivity hypothesis required by downstream statements alphaInv_positive, exp_factor_bounded, log_alphaInv_eq and logarithmic_derivative_constant inside the same module. It anchors the constants pipeline that produces the alpha band (137.030, 137.039) and feeds the phi-ladder mass formulas. The module treats the exponential form itself as a bridge claim whose uniqueness relative to other functional shapes remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.