alphaInv_of_gap_at_canonical
plain-language theorem explainer
The equality shows that the parameterized inverse fine-structure constant recovers its canonical value when the gap weight is set to the physical f_gap. Researchers deriving alpha from Recognition Science structures cite this to confirm that the general expression specializes correctly. The proof is immediate reflexivity because the definition of alphaInv_of_gap at the canonical gap matches the body of alphaInv exactly.
Claim. Let $f(g) := 4π·11 · exp(-g/(4π·11))$ denote the parameterized form of the inverse fine-structure constant. Then $f(f_{gap}) = α^{-1}$, where $f_{gap} = w_8 ln φ$ is the canonical gap weight from the eight-tick octave and $α^{-1}$ is the constant $4π·11 · exp(-f_{gap}/(4π·11))$.
background
The AlphaExponentialForm module analyzes the structural form $α^{-1} = α_{seed} exp(-f_{gap}/α_{seed})$ with $α_{seed} = 4π·11$. The definition alphaInv_of_gap generalizes this expression to an arbitrary real gap argument g. Upstream, alphaInv is defined directly by substituting the canonical f_gap, which itself comes from GapWeight as w8_from_eight_tick times log φ, where φ is the golden ratio fixed point of the J-cost. The module documents that this exponential satisfies a logarithmic ODE consistent with running-coupling behavior and arises from the log-coordinate structure of the J-cost cosh expansion.
proof idea
The proof is a one-line wrapper that applies reflexivity: substituting the canonical f_gap into the definition of alphaInv_of_gap produces exactly the body of alphaInv.
why it matters
This equality anchors the parameterized analysis to the canonical constant used throughout the Recognition framework for mass ladders and coupling calculations. It supports the module's documentation of positivity and the differential equation while leaving open the uniqueness question for the exponential Taylor coefficients. In the broader chain it connects to the phi-forcing fixed point and the eight-tick octave that determine the gap weight, confirming consistency at the physical value near 137.036.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.