pith. machine review for the scientific record. sign in
def definition def or abbrev high

alphaInv

show as:
view Lean formalization →

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 in Recognition Science

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.

scope and limits

Lean usage

theorem use_in_alpha : Alpha.alpha = 1 / Alpha.alphaInv := by rfl

formal statement (Lean)

  35@[simp] def alphaInv : ℝ := alpha_seed * Real.exp (-(f_gap / alpha_seed))

proof body

Definition body.

  36
  37/-- Fine-structure constant (α_EM). -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (7)

Lean names referenced from this declaration's body.