alpha_seed
plain-language theorem explainer
The alpha_seed definition supplies the constant 44π as the baseline additive seed for the inverse fine-structure constant in Recognition Science. Researchers computing electromagnetic constants from ledger geometry cite it to fix the starting value before applying the exponential resummation with gap term. The declaration is introduced by a direct equational assignment with no reduction steps or lemmas.
Claim. The seed for the inverse fine-structure constant is defined by $α_{seed} = 44π$.
background
The AlphaPrecision module addresses Q8 refinement of α^{-1} via two Recognition Science formulas. The additive seed is given as 4π × 11, rewritten here as 44π, which encodes the baseline spherical closure cost over 11-edge interaction paths. The exponential form then reads α^{-1} = α_seed × exp(−w₈ ln φ / α_seed), with the module targeting the interval (137.030, 137.039) to approach CODATA 2022 precision.
proof idea
The declaration is a direct definition that sets alpha_seed equal to 44 * Real.pi, matching the upstream geometric seed 4 * Real.pi * 11 from the Alpha module.
why it matters
This seed is used by alphaInv and alpha_components_derived in the Alpha module to unfold the canonical exponential expression for α^{-1}. It supports the Q8 precision step in the Recognition Science constants pipeline, connecting the geometric ledger seed to the phi-ladder and eight-tick structure while keeping zero adjustable parameters. Downstream results apply it to derive linear terms, positivity, and seed-ratio properties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.