alphaInv_linear_rate
plain-language theorem explainer
The theorem states that the derivative of alpha inverse with respect to the gap function equals minus one at the origin. Modelers of the fine-structure constant running in Recognition Science cite this when verifying the leading linear behavior of the exponential ansatz. The proof is a one-line wrapper that substitutes the precomputed derivative formula and the zero-gap value then clears denominators by field simplification.
Claim. $ (d/dg) [α^{-1}(g)]_{g=0} = -1 $, where $α^{-1}(g) := α_{seed} · exp(-g/α_{seed})$ and $α_{seed} = 4π·11$.
background
The module examines the exponential ansatz $α^{-1} = α_{seed} · exp(-f_gap / α_{seed})$ for the inverse fine-structure constant. Here alphaInv_of_gap is the function that realizes this ansatz, alphaInv_linear_term records its value at zero gap, and deriv_alphaInv_of_gap supplies the explicit derivative formula $-(alphaInv_of_gap g / α_{seed})$. The local setting is the remaining structural gap between the canonical formula and a first-principles derivation; the module proves positivity and the logarithmic ODE but leaves uniqueness open. Upstream, alphaInv_linear_term states that the first-order term matches a naive perturbative expansion.
proof idea
One-line wrapper that applies deriv_alphaInv_of_gap, substitutes alphaInv_linear_term, then invokes field_simp to obtain the numerical result -1.
why it matters
The result supplies the constant leading slope required by the exponential form and is invoked by the downstream uniqueness ODE principle. It belongs to the structural analysis of the alpha exponential form documented as a bridge claim in the module, where the integer 44 in α_seed is already forced and the exponential shape remains the open step. The constant rate -1 is independent of α_seed at this order and is consistent with the logarithmic derivative that appears in renormalization-group flow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.