alphaInv_of_gap
plain-language theorem explainer
The definition parameterizes the inverse fine-structure constant by the gap weight g, returning the product of the geometric seed and the exponential of the negated scaled gap. Analysts of the fine-structure constant in Recognition Science cite this form when examining its dependence on the gap parameter. It is supplied as a direct definition that reproduces the canonical expression upon substitution of the standard gap value.
Claim. Let $α^{-1}(g) := α_{seed} · exp(-g / α_{seed})$, where $α_{seed} = 4π · 11$ is the geometric seed from ledger structure and $g$ stands for the gap weight $f_{gap} = w_8 · ln(φ)$.
background
In the Alpha Exponential Form module the canonical expression for the inverse fine-structure constant is $α^{-1} = α_{seed} · exp(-f_{gap} / α_{seed})$, with $α_{seed} = 4π · 11$ the baseline spherical closure cost over 11-edge interaction paths and $f_{gap} = w_8 · ln(φ)$ the gap weight obtained from the DFT-8 projection. The module supplies structural analysis of this exponential form, proving positivity and identifying the logarithmic ODE it satisfies, while documenting that the Taylor coefficients of exp arise from the J-cost log-coordinate structure. Upstream, the identical expression appears as the definition of alphaInv in the Alpha module, described as the dimensionless inverse fine-structure constant derived from the structural seed and gap with zero adjustable parameters.
proof idea
Direct definition that unfolds to the product of the seed constant and the real exponential of the negated gap scaled by the seed; no auxiliary lemmas are invoked beyond the standard definitions of multiplication and Real.exp.
why it matters
This definition supplies the common object for the module's downstream results on the linear term at zero gap, the first derivative, the constant logarithmic derivative, and agreement with alphaInv at the canonical gap. It addresses the remaining open step (Gap B) in the validation program for the exponential form of $α^{-1}$, as stated in the module documentation, and connects to the Recognition Science constants pipeline in which $α^{-1}$ is constrained to the interval (137.030, 137.039) via the phi-ladder and eight-tick octave. The uniqueness question against alternative functional forms remains unproved and is flagged as a BRIDGE claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.