alphaInv_of_gap_at_canonical
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the exponential form from a first-principles variational principle.
- Does not prove uniqueness of the exponential against other functional forms.
- Does not compute or bound numerical deviations from the measured fine-structure constant.
- Does not address higher-order gap corrections or renormalization-group flow.
formal statement (Lean)
127theorem alphaInv_of_gap_at_canonical : alphaInv_of_gap f_gap = alphaInv := rfl
proof body
Term-mode proof.
128
129/-- The derivative of alphaInv with respect to f_gap. -/