Pith. sign in
module module moderate

IndisputableMonolith.Constants.AlphaGenesis.MeasurementVerdict

show as:
view Lean formalization →

Measurement verdict for Alpha Genesis: certified numerical comparison of the forward-derived inverse fine-structure constant against the quarantined CODATA anchor. Constants and metrology readers cite it for the RS residual (about 0.0007 above CODATA). The module is a chain of Taylor interval bounds on exp and log φ that discharge the residual inequality.

claimWith $\varphi$ the golden ratio, the module certifies $\log\varphi < 0.48122$ via $\exp(0.48122) > 1.61804$, related exponential-load bounds near $8.6705\times 10^{-3}$, and the comparison $\alpha^{-1}_{\mathrm{gen}} - \alpha^{-1}_{\mathrm{CODATA}} > 7\times 10^{-4}$ (with matching uncertainty identity).

background

Alpha Genesis derives $\alpha^{-1}$ forward from the EM recognition loop before any measurement comparison. Upstream LoopCertificate (M3) defines the object from the channel budget $\Omega(\partial Q_3)\times E_{\mathrm{passive}}=4\pi\times 11$ and the eight-tick gap weight $w_8$; the dressing is forced exponential, not additive. ResidualTarget (M4) is the sole quarantine that may mention the measured value; ExternalAnchors holds CODATA and other empirical anchors.

This module sits on that quarantine boundary. It imports interval infrastructure (AlphaBounds, W8Bounds) and supplies the concrete decimal lemmas needed to turn the symbolic genesis formula into a strict inequality versus CODATA. Sibling names fix the working cutoffs: Taylor degree-12 expansions at $0.48122$ and $-0.0086705$, floors, and one-sided exp/log comparisons.

Framework context: RS targets $\alpha^{-1}$ inside $(137.030,137.039)$ in native units, with $w_8$ the closed form $(348+210\sqrt{2}-(204+130\sqrt{2})\varphi)/7$.

proof idea

Not a single theorem: a stacked numerics file. First block proves $\exp(0.48122)>1.61804$ by degree-12 Taylor polynomial plus explicit remainder, hence $\log\varphi<0.48122$. Parallel block at $-0.0086705$ bounds the exponential load from below and yields $\mathrm{exponentialLoad}<0.0086705$. Those inequalities feed the residual comparison alphaInvGenesis_exceeds_CODATA_by_0007 and the uncertainty identity alpha_inv_uncertainty_eq. All steps are interval/Taylor arithmetic; no new physical hypothesis is introduced.

why it matters in Recognition Science

Feeds the AlphaGenesis aggregator, which assembles the forward derivation of the fine-structure constant as the mirror of the mass-ladder program. Downstream doc: $\alpha^{-1}=\mathrm{seed}\cdot\mathrm{contWeight}(w_8/\mathrm{seed})$, with the dressing forced by the same factorization premise as the T9 measure. The verdict module is what turns that symbolic object into a referee-checkable claim against CODATA without contaminating M1–M3 (those remain measurement-blind). It touches the RS alpha band $(137.030,137.039)$ and records the open residual rather than forcing an exact match. Parent import edge is only the aggregator; scientific consumers are any theorem that needs “genesis $\alpha^{-1}$ lies a certified $7\times 10^{-4}$ above the external anchor.”

scope and limits

used by (1)

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

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (15)