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

alpha_seed

show as:
view Lean formalization →

alpha_seed supplies the real number 4π × 11 as the geometric baseline for the inverse fine-structure constant. Researchers deriving α_EM from ledger structure and the phi-ladder cite this seed when building the exponential resummation for alphaInv. The declaration is a direct one-line assignment with no lemmas or reductions.

claimLet $α_{seed} := 4π · 11$. This quantity is the baseline spherical closure cost over 11-edge interaction paths and enters the formula for the inverse fine-structure constant as the prefactor in $α^{-1} = α_{seed} · exp(-f_{gap}/α_{seed})$.

background

Recognition Science derives dimensionless constants from structural seeds on the phi-ladder. The alpha_seed is the multiplicative factor in the canonical expression for alphaInv, which is defined as alpha_seed times the exponential of minus the gap weight divided by alpha_seed. Upstream results in AlphaHigherOrder and AlphaPrecision supply parallel seeds (4π times passive_edges or 44π) while the present definition fixes the 11-edge count for the canonical pipeline. The module imports RSNativeUnits.voxel and GapWeight to keep all quantities in native units with c = 1 and no free parameters.

proof idea

The declaration is a direct definition that assigns the literal expression 4 * Real.pi * 11. No tactics or upstream lemmas are invoked; the @[simp] attribute simply registers the constant for later rewriting in alphaInv and its exponential forms.

why it matters in Recognition Science

alpha_seed anchors the derivation of alphaInv (~137.036) that lies inside the predicted band (137.030, 137.039). It is referenced by alpha_components_derived, alphaInv_def, alphaInv_of_gap, and alphaInv_seed_ratio, which together confirm the exponential resummation matches the structural seed and gap. The seed therefore closes the constants section of the forcing chain (T5–T8) by supplying the 11-edge ledger factor without adjustable parameters.

scope and limits

Lean usage

def alphaInv : ℝ := alpha_seed * Real.exp (-(f_gap / alpha_seed))

formal statement (Lean)

  25@[simp] def alpha_seed : ℝ := 4 * Real.pi * 11

proof body

Definition body.

  26
  27/-- Legacy curvature correction (voxel seam count).
  28    Retained for compatibility with older reports, but no longer used in
  29    the canonical certified `alphaInv` pipeline. -/

used by (36)

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

… and 6 more

depends on (9)

Lean names referenced from this declaration's body.