alphaInv_def
The theorem states that the inverse fine-structure constant equals the geometric seed 4π·11 multiplied by the exponential of minus the gap weight divided by the seed. Researchers deriving constants from Recognition Science ledger structures cite this as the explicit unfolded form of α⁻¹. The proof is a one-line reflexivity on the definitional expression of alphaInv supplied by the Alpha module.
claim$α^{-1} = 4π·11 · exp(-f_gap / (4π·11))$, where $f_gap = w_8 ln φ$ and $φ$ is the golden ratio.
background
The module examines the exponential form of the fine-structure constant. alphaInv is the dimensionless inverse fine-structure constant (~137.036) obtained from the structural seed and gap with no free parameters. alpha_seed is defined as 4π·11, the baseline spherical closure cost over 11-edge interaction paths. f_gap is the gap weight w8·ln(φ) from the DFT-8 projection in GapWeight.
proof idea
The proof is a term-mode reflexivity that directly matches alphaInv to its defining expression alpha_seed * Real.exp(-(f_gap / alpha_seed)). It applies the definitional equality from the Alpha module without further reduction.
why it matters in Recognition Science
This supplies the explicit form consumed by the downstream exponential_form_uniqueness_ode_principle theorem. It documents the structural motivation for the exponential in the AlphaExponentialForm module, linking to the J-cost log-coordinate structure and the eight-tick octave. The module flags the physical reason for constant logarithmic derivative as the remaining open gap after this step.
scope and limits
- Does not derive the exponential form from a first-principles variational argument.
- Does not prove uniqueness of the exponential against other functional forms such as rational approximations.
- Does not compute a numerical value or bound beyond the definitional expression.
- Does not formalize renormalization-group flow beyond identifying the logarithmic ODE.
formal statement (Lean)
57theorem alphaInv_def : alphaInv = alpha_seed * Real.exp (-(f_gap / alpha_seed)) := rfl
proof body
Term-mode proof.
58
59/-- The seed is positive: α_seed = 4π·11 > 0. -/