Pith. sign in
module module high

IndisputableMonolith.Constants.AlphaGenesis

show as:
view Lean formalization →

Barrel module for the Alpha Genesis derivation of the inverse fine-structure constant from recognition geometry. It re-exports pattern forcing, the EM loop certificate, resummation, spectral and calibration forcing, κ_γ-irreducibility, and two CODATA-quarantine modules. Anyone citing the RS-native α⁻¹ band lands here. No standalone proofs: the argument lives in the eight named submodules.

claimAlpha Genesis constructs $\alpha^{-1}$ forward from the electromagnetic recognition loop. The channel budget is $\Omega(\partial Q_3)\times E_{\mathrm{passive}}=4\pi\times 11$ (discrete Gauss-Bonnet on the voxel). The dressing uses the forced $\varphi$-ladder pattern $u_t=\varphi^t$ with decay envelope $\varphi^{-k}$, under self-similar response with no free calibration. Residual comparison to CODATA and the measurement verdict are quarantined. The $\kappa_\gamma$-scaling test upgrades the status of $\alpha^{-1}$ from boundary datum to structural theorem.

background

Recognition Science treats dimensionless constants as forced outputs of ledger geometry, not inputs. The upstream forcing chain already supplies T5 (unique $J$-cost), T6 ($\varphi$ as the self-similar fixed point of $r^2=r+1$), T7 (eight-tick octave), and T8 ($D=3$). Alpha Genesis builds the EM sector on that spine.

The central object is the EM recognition loop: one active edge transition spread over the passive dressing field of the voxel, with channel budget $\Omega(\partial Q_3)\times E_{\mathrm{passive}}=4\pi\times 11$. Pattern forcing shows any eight-tick ladder with unit base, constant positive step ratio, and the T6 equation is exactly $u_t=\varphi^t$, and the spectral weight's decay $\varphi^{-k}$ is the forced measure termwise. Calibration forcing replaces unit-linear-response normalization by a self-similar dressing whose premises are factorization over independent loads, not a chosen scale.

Two modules (ResidualTarget, MeasurementVerdict) are explicitly quarantined: they alone may mention CODATA, and nothing in the forward M1–M3-style construction imports them. KappaGammaIrreducibility formalizes the panel's $\kappa_\gamma$-scaling test and the finite $\sigma=0$ closure that places $\alpha^{-1}$ in the irreducible branch.

proof idea

Definition-and-import barrel: no theorems are proved at this file. The logical spine is assembled by re-exporting eight submodules. PatternForcing forces the $\varphi$-ladder and spectral envelope; LoopCertificate defines $\alpha^{-1}$ as the EM loop's channel budget; ResummationForcing, SpectralForcing, and CalibrationForcing eliminate free dressing and normalization choices; KappaGammaIrreducibility upgrades boundary status to a structural theorem. ResidualTarget and MeasurementVerdict sit behind a quarantine wall and are never imported by the forward path. Downstream consumers import this barrel once and obtain the whole namespace.

why it matters in Recognition Science

Feeds the public root IndisputableMonolith, which exports the T-2 through T8 spine, recognition geometry, and core ILG gravity, and deliberately excludes later-physics verticals. This module is the constants-side home of the RS claim that $\alpha^{-1}$ lies in the narrow band $(137.030, 137.039)$ as a derived quantity rather than a fit. The quarantine split (forward derivation blind to CODATA; comparison modules isolated) is load-bearing for the framework's non-circularity claim. KappaGammaIrreducibility is the step that converts "measured boundary datum" into a theorem under the $\kappa_\gamma$-scaling test. Parent import is only the monolith root; specialized callers should prefer the individual M2–M7 submodules when they need a single lemma.

scope and limits

used by (1)

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

depends on (8)

Lean names referenced from this declaration's body.