Pith. sign in
module module moderate

IndisputableMonolith.Verification.AlphaCorrectionAnalysis

show as:
view Lean formalization →

Module that quantifies the exact additive correction needed so the RS inverse fine-structure constant matches the CODATA anchor. Auditors of the alpha gap cite the required-correction window, positivity facts, and four candidate closed forms. The argument is interval arithmetic against ExternalAnchors plus elementary residual comparisons; it does not re-derive alpha.

claimLet $\alpha^{-1}_{\mathrm{RS}}$ be the Recognition-Science inverse fine-structure constant built from the cubic-ledger seed and $\varphi$-dressing, and let $\alpha^{-1}_{\mathrm{CODATA}}$ be the external empirical anchor. The module defines the required correction $\delta := \alpha^{-1}_{\mathrm{CODATA}} - \alpha^{-1}_{\mathrm{RS}}$, proves $\delta > 0$ under the current bounds, supplies a numerical window for $\delta$, and records four candidate closed-form expressions for $\delta$.

background

Recognition Science forces an $O(4\pi)$ recognition-scale seed and a $\varphi$-dressing for the inverse fine-structure constant, but the exact infrared value $\alpha^{-1}(0)$ remains an open boundary condition. The AlphaDerivation module assembles the combinatorial seed $4\pi\cdot 11$ from the cubic ledger and is explicit that identifying that seed with the measured EM coupling fails a first-principles audit; only the seed geometry and dressing structure are forced.

ExternalAnchors is the single quarantined home for CODATA and other empirical calibration data. AlphaBounds supplies rigorous interval bounds on the RS $\alpha^{-1}$ constructed from the symbolic derivation. This verification module sits downstream of those three pieces: it treats the residual between the RS interval and the CODATA anchor as an object of study rather than absorbing the mismatch into the core cost calculus.

Sibling objects include the exact residual required_correction, positivity lemmas, a window extracted from current bounds, and four named candidate closed forms with partial numerical control.

proof idea

Definition-and-comparison module, not a single theorem. It introduces the residual $\delta$ against the CODATA anchor, then proves positivity by comparing the upper end of the RS $\alpha^{-1}$ interval (from AlphaBounds) to the external anchor. A window lemma packages the same interval data into concrete numerical bounds on $\delta$. Four candidate expressions are recorded as named constants; one has interval bounds and another an exact evaluated form. The structure is arithmetic residual analysis plus bookkeeping of candidate closed forms, with no new forcing from the RCL or the T0–T8 chain.

why it matters in Recognition Science

The RS alpha band in native units sits near $(137.030, 137.039)$; matching CODATA still needs a small positive correction whose status is open in AlphaDerivation. This module isolates that residual so the cost-first core stays free of empirical tuning while verification can state exactly how large the gap is and which closed forms remain viable.

No downstream consumers are wired yet (used_by is empty). The natural parents are future audit or closure theorems that either discharge one candidate as the forced IR boundary condition or prove that no simple $\varphi$-ladder form fits the window. Until then the module is the honest ledger of the alpha mismatch: seed and dressing forced, exact $\alpha^{-1}(0)$ still external.

scope and limits

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (12)