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 α⁻¹ against the CODATA anchor, and the unique closing load that cancels it. Anyone matching the forward α derivation to experiment cites the residual bounds and the seam-closure criterion. The module is mostly definitions plus elementary uniqueness and evaluation lemmas around that residual.

claimLet $R$ be the signed residual of the first-order genesis value of $\alpha^{-1}$ against the CODATA anchor. The module introduces a corrected inverse fine-structure constant $\alpha^{-1}_{\mathrm{corr}}(\ell)$ depending on a closing load $\ell$, records bounds on $R$, and proves there exists a unique $\ell$ at which the corrected value equals the CODATA value (seam closure).

background

Alpha Genesis builds $\alpha^{-1}$ forward from the EM recognition loop (channel budget $\Omega(\partial Q_3)\times E_{\mathrm{passive}}=4\pi\times 11$) and the forced exponential dressing, before any comparison with measurement. The first-order genesis value therefore sits a finite signed distance from the external CODATA anchor; that distance is the residual this module names.

External anchors are quarantined: CODATA enters only through the dedicated calibration module, so the cost-first core never imports empirical numbers. Interval bounds on $\alpha^{-1}$ from the symbolic derivation supply the rigorous window in which the residual is evaluated. Measure forcing (T9) supplies the weighting context for the dressing that produces the genesis seed.

Sibling objects include the residual itself, residual bounds, the load-dependent corrected inverse, evaluation at zero and at the closing load, uniqueness of that load, and the seam-closure predicate equating correction with CODATA match.

proof idea

Definition-heavy module, not a single deep proof. It names the residual as genesis value minus CODATA, packages interval bounds, and defines the corrected $\alpha^{-1}$ as a function of a closing load. Elementary lemmas evaluate the correction at load zero and at the closing load, record that the log-density factor is nonzero, and prove existence and uniqueness of the load that drives the residual to zero. Seam closure is then the propositional packaging of that equality, with an iff linking the predicate to the corrected-equals-CODATA statement.

why it matters in Recognition Science

Closes the measurement interface of the forward $\alpha$ program: after LoopCertificate and the resummation forcing produce a first-order genesis value, this module states how far that value sits from CODATA and what unique load would absorb the gap. The Alpha Genesis aggregator imports it as part of the forward derivation that mirrors the mass program. MeasurementVerdict (M7) imports it under quarantine to formalize the decisive comparison with experiment without feeding CODATA back into the constructive chain. In framework terms it sits downstream of the T5–T9 forcing (J-uniqueness, $\phi$, eight-tick, $D=3$, forced measure) and of the RS-native $\alpha^{-1}$ band, converting a residual into a unique seam-closure condition rather than a free fit.

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)