Pith. sign in
module module high

IndisputableMonolith.Constants.AlphaGenesis.ResidualTarget

show as:
view Lean formalization →

Defines the signed residual of the first-order Alpha Genesis value of inverse alpha against the CODATA anchor, plus a corrected inverse-alpha that absorbs a closing load. Anyone matching the forward EM-loop derivation to experiment cites the residual bounds and unique closing load. The module packages interval bounds, uniqueness, and a seam-closure predicate around that residual.

claimLet $\alpha^{-1}_{\mathrm{gen}}$ be the first-order genesis value and $\alpha^{-1}_{\mathrm{CODATA}}$ the external anchor. The signed residual is $r=\alpha^{-1}_{\mathrm{gen}}-\alpha^{-1}_{\mathrm{CODATA}}$. A corrected inverse fine-structure constant $\alpha^{-1}_{\mathrm{corr}}(\ell)$ depends on a closing load $\ell$; there is a unique $\ell_*$ with $\alpha^{-1}_{\mathrm{corr}}(\ell_*)=\alpha^{-1}_{\mathrm{CODATA}}$ precisely when the seam derivation closes.

background

Alpha Genesis builds $\alpha^{-1}$ forward from the EM recognition loop, not by fitting measurement. The LoopCertificate module fixes the channel budget as the discrete Gauss-Bonnet total $\Omega(\partial Q_3)\times E_{\mathrm{passive}}=4\pi\times 11$ and treats the dressing as forced by the same factorization premise that yields the T9 measure. ExternalAnchors is the single quarantine for CODATA and other empirical calibration; the cost-first core never imports it except at comparison points.

This module isolates the signed residual of that first-order genesis value against CODATA, together with a corrected inverse-alpha that folds in a closing load. Sibling objects include residual bounds (via AlphaBounds interval arithmetic), the corrected value at zero load and at the closing load, uniqueness of the closing load, and a seam-closure predicate equating correction-to-CODATA with derivation closure.

proof idea

Definition-heavy module with supporting lemmas, not a single theorem. It introduces the residual as genesis minus CODATA, residual interval bounds from the AlphaBounds numerics, and correctedAlphaInv as a load-dependent adjustment of the genesis value. Algebraic identities give the corrected value at zero load and at the closing load; a non-vanishing log-density hypothesis supports uniqueness. existsUnique_closingLoad and the seam-closes iff statement package the residual match into a single Prop used by the measurement quarantine.

why it matters in Recognition Science

Closes the comparison seam between the forward Alpha Genesis construction and external data without polluting the cost-first core. The AlphaGenesis aggregator imports it as part of the mass-derivation-style forward program (resummation forcing, seed times continuum weight). MeasurementVerdict, the quarantined M7 module formalizing the strongest measurement-side objection, imports it so that CODATA contact stays one-directional. Landmark context: the alpha band in RS-native units sits near $(137.030,137.039)$; residual and closing load make that band checkable against CODATA while preserving the T5--T9 forcing chain and RCL-derived J-cost structure upstream.

scope and limits

used by (2)

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

depends on (6)

Lean names referenced from this declaration's body.

declarations in this module (11)