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

alpha_seed

show as:
view Lean formalization →

The geometric seed for the inverse fine-structure constant is supplied as the constant 44 pi. Researchers deriving electromagnetic constants from Recognition Science ledger structure cite this baseline before exponential resummation with the gap term. The declaration is a direct one-line assignment with no computation or hypotheses.

claimThe seed value for the inverse fine-structure constant is given by $44 pi$.

background

The Alpha-Inverse Precision Refinement module presents two RS formulas for the inverse fine-structure constant. The additive seed is $alpha^{-1}_add = 4 pi times 11 approx 138.23$, equivalent to 44 pi, representing baseline spherical closure cost over 11-edge paths. The exponential resummation is $alpha^{-1} = alpha_seed times exp(-w_8 ln phi / alpha_seed)$ with $w_8 approx 2.490$. Upstream results from the Alpha module define the identical seed as $4 pi times 11$ from ledger geometry, while the HigherOrder module uses $4 pi times passive_edges$.

proof idea

This is a one-line definition that directly assigns the real number 44 times pi to the seed constant.

why it matters in Recognition Science

The seed enters the definition of alphaInv in the Alpha module via the exponential form $alpha_seed times exp(-f_gap / alpha_seed)$, which is proved to lie in (137.030, 137.039). It supplies the additive component of the two RS formulas and supports the zero-parameter derivation of the fine-structure constant. The declaration feeds 36 downstream uses including alpha_components_derived and alphaInv_def, advancing the framework target of 1 ppm precision once curvature corrections are added.

scope and limits

formal statement (Lean)

  29noncomputable def alpha_seed : ℝ := 44 * Real.pi

proof body

Definition body.

  30

used by (36)

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

… and 6 more

depends on (2)

Lean names referenced from this declaration's body.