pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Constants.Alpha

show as:
view Lean formalization →

The Constants.Alpha module supplies the geometric seed 4π·11 for the fine-structure constant from ledger structure, encoding baseline spherical closure over 11-edge paths. Researchers deriving parameter-free α values cite these definitions to anchor the electromagnetic coupling in the phi-ladder. The module contains only definitions and imports from Constants and GapWeight, establishing the starting point for gap-weighted exponential corrections without any proofs.

claimThe geometric seed is defined by $4π·11$, with inverse fine-structure constant $α^{-1} = α_{seed} exp(-f_{gap}/α_{seed})$ where $f_{gap} = w_8 ln φ$ and $w_8$ is the parameter-free 8-tick gap weight.

background

This module operates in the Constants domain of Recognition Science, which derives physical constants from the single functional equation and forcing chain T0-T8. It imports the base time quantum τ₀ = 1 tick and the gap weight w₈ from upstream modules, where f_gap = w₈ · ln(φ) supplies the single gap term in the α pipeline.

proof idea

This is a definition module with no proofs. It declares alpha_seed as the 4π·11 ledger factor, delta_kappa for adjustments, alphaInv and alpha as derived objects, and alpha_components_derived for breakdowns, all built directly from the imported GapWeight projection.

why it matters in Recognition Science

The module feeds the structural seed into AlphaExponentialForm for the full α derivation, HartreeRydbergScoreCard for binding energies, RSNativeUnits for native scaling, and Cosmology.HubbleTension for dark energy links. It closes Gap B in the validation program by supplying α^{-1} = α_seed exp(-f_gap / α_seed) and anchors the alpha band inside the eight-tick octave.

scope and limits

used by (22)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (5)