alphaInv_def
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.