alphaInv_linear_term
plain-language theorem explainer
alphaInv_linear_term establishes that the inverse fine-structure constant at vanishing gap weight equals the geometric seed 4π·11. Workers on the Taylor expansion of α⁻¹(f_gap) cite it for the constant term in perturbative calculations. The proof is a direct term reduction that unfolds the exponential definition and simplifies the zero argument case.
Claim. At gap weight zero, $α^{-1}(0) = 4π·11$, where $α^{-1}(g) := 4π·11 · exp(-g/(4π·11))$.
background
The module examines the exponential form $α^{-1} = α_seed · exp(-f_gap/α_seed)$ for the inverse fine-structure constant, with $α_seed = 4π·11$ arising from the ledger structure as the baseline spherical closure cost over 11-edge paths. The function alphaInv_of_gap parameterizes this expression by the gap weight f_gap. Upstream results supply the definition of alpha_seed as 4π·11 and the parameterized form alphaInv_of_gap(g) = alpha_seed * exp(-g/alpha_seed). This local setting documents structural properties of the form without closing the uniqueness gap from first principles.
proof idea
The term proof unfolds the definition of alphaInv_of_gap and applies simplification using the fact that exp(0) = 1.
why it matters
It supplies the base case for the linear rate theorem that follows, which computes the derivative at zero gap, and supports the ODE uniqueness principle for the exponential form. The result confirms the leading term matches the naive perturbative expansion, as stated in the module's analysis of the canonical formula. It addresses part of the structural motivation from the J-cost log-structure but leaves the full uniqueness question open, as flagged in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.