alphaInv_of_gap
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.
claimLet $α^{-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 in Recognition Science
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.
scope and limits
- Does not prove uniqueness of the exponential form against rational or power-law alternatives.
- Does not derive the form from a variational principle or first-principles RS equation.
- Does not supply numerical evaluation or direct comparison with measured values.
- Does not close the gap in a definitive sense as a theorem.
formal statement (Lean)
124noncomputable def alphaInv_of_gap (g : ℝ) : ℝ := alpha_seed * Real.exp (-(g / alpha_seed))
proof body
Definition body.
125
126/-- At the canonical f_gap, alphaInv_of_gap agrees with alphaInv. -/