alphaInv
plain-language theorem explainer
The definition encodes the inverse fine-structure constant as the geometric seed multiplied by the exponential of the negative normalized gap weight. Researchers deriving constants from Recognition Science ledger structures cite it for the zero-parameter result near 137.036. The construction is a direct algebraic substitution of the seed and gap functions.
Claim. $α^{-1} = 4π·11 · exp(−g/(4π·11))$, where $g$ is the gap weight $w_8 log ϕ$ obtained from the eight-tick DFT projection and $ϕ$ is the golden ratio.
background
The Constants module builds fundamental constants from ledger geometry in Recognition Science. The seed equals four pi times eleven and represents baseline spherical closure cost over eleven-edge interaction paths. The gap weight is the product of the eight-tick weight and the logarithm of the golden ratio. This exponential resummation produces the inverse fine-structure constant in the interval (137.030, 137.039) with no adjustable parameters, matching the framework's native units where c=1, ħ=ϕ^{-5} and G=ϕ^5/π.
proof idea
The definition is a one-line wrapper that substitutes the alpha_seed value and applies the exponential to the negative ratio of f_gap over that seed.
why it matters
This supplies the central expression for alpha inverse invoked by the gauge-invariance theorems in Bridge.GaugeVsParams, including alphaInv_dimensionless and alphaInv_gauge_invariant. It fills the constants slot in the Recognition Science framework by deriving the value from the phi-ladder and eight-tick octave (T7). The definition closes the structural computation without free parameters and feeds directly into the fine-structure constant alpha itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.