alphaInv_of_gap
plain-language theorem explainer
Defines the inverse fine-structure constant as a function of arbitrary gap weight g by the expression seed times exp(-g/seed). Researchers examining the differential properties of the alpha exponential form cite this parameterization when deriving rates and logarithmic derivatives. The definition is a direct one-line match to the canonical alphaInv expression with the fixed f_gap replaced by the input variable.
Claim. $α^{-1}(g) := α_{seed} exp(-g / α_{seed})$ for real $g$, where $α_{seed} = 4π × 11$.
background
The module analyzes the exponential form $α^{-1} = α_{seed} · exp(-f_gap / α_{seed})$ with $α_{seed} = 4π·11$ and $f_gap = w_8 ln(φ)$. This definition generalizes the fixed canonical alphaInv (defined in Constants.Alpha as the same expression evaluated at the specific f_gap) to a variable gap input. Upstream results supply the seed value as the geometric baseline from 11-edge paths and the gap weight from the eight-tick projection.
proof idea
One-line definition that directly substitutes the input g into the exponential expression already used for the canonical alphaInv.
why it matters
Supplies the variable-gap function required by the five downstream results on linear terms, derivatives, and the constant logarithmic derivative. It supports the module's documentation of the exponential form's ODE behavior and positivity while leaving the uniqueness question open, as noted in the module doc. The form connects to the alpha band (137.030 to 137.039) and the J-cost log-structure in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.