alphaInv_def
plain-language theorem explainer
The equality states that the inverse fine-structure constant equals the geometric seed multiplied by an exponential factor set by the gap weight. Researchers tracing the Recognition Science derivation of electromagnetic constants would cite this when inspecting the resummation structure. The proof is a direct reflexivity step on the defining expression of alphaInv.
Claim. $α^{-1} = α_{seed} · exp(-f_{gap}/α_{seed})$, where $α_{seed} = 4π·11$ and $f_{gap}$ is the gap weight $w_8 ln φ$.
background
The AlphaExponentialForm module examines the canonical expression for the inverse fine-structure constant. Upstream, alphaInv is defined in Constants.Alpha as the product of the seed and the exponential suppression. The seed alpha_seed equals 4π·11 and encodes baseline spherical closure cost over 11-edge paths. The gap weight f_gap is supplied by GapWeight as w8 times the logarithm of φ. The module document notes that this exponential form is currently a definition rather than a first-principles derivation, while recording its positivity and the logarithmic ODE it satisfies.
proof idea
The proof is a one-line term that applies reflexivity to unfold the definition of alphaInv.
why it matters
This equality supplies the concrete expression used by the downstream theorem exponential_form_uniqueness_ode_principle, which records the ODE satisfied by the form and flags the remaining physical question of why the log derivative is constant. It supports the constants pipeline that places α^{-1} inside the interval (137.030, 137.039) and sits inside the structural analysis of the exponential resummation motivated by J-cost log coordinates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.