Pith. sign in
module module moderate

IndisputableMonolith.Verification.AlphaResolutionPass2

show as:
view Lean formalization →

Verification pass that isolates the exact additive shift needed so the RS prediction for the inverse fine-structure constant matches the CODATA anchor. It equates a required numerical mismatch to a geometric curvature correction built from π⁵, proves uniqueness of that additive closure, and checks the corrected value lies inside the CODATA 3σ band. Cite when auditing α⁻¹ alignment or the curvature-space exponent. The argument is algebraic identity plus uniqueness of the additive fix, not a new derivation of α itself.

claimLet $\alpha^{-1}_{\mathrm{RS}}$ be the Recognition Science inverse fine-structure constant and $\alpha^{-1}_{\mathrm{CODATA}}$ the external anchor. The module constructs the required additive correction $\delta\alpha^{-1}$ such that $\alpha^{-1}_{\mathrm{RS}}+\delta\alpha^{-1}=\alpha^{-1}_{\mathrm{CODATA}}$, identifies it with the geometric curvature term $\delta_\kappa=-103/(102\pi^5)$, proves that additive closure is unique for exact alignment, and verifies the residual is zero and the corrected value lies in the CODATA $3\sigma$ window.

background

Recognition Science predicts $\alpha^{-1}$ in a narrow band near $137.03$–$137.04$ from the cost-first core (RCL and the forcing chain). Comparison with experiment is deliberately quarantined: all CODATA and calibration numbers live in ExternalAnchors, so the derivation core never imports lab data.

CurvatureSpaceDerivation supplies the geometric correction $\delta_\kappa=-103/(102\pi^5)$. Its doc states that the $\pi^5$ power appears because the relevant integration is over a five-dimensional configuration space, not an ad hoc fit. Constants.Alpha holds the native RS expression for $\alpha^{-1}$ before this pass.

This module sits in Verification: it does not re-derive $\alpha$; it measures the residual between the RS value and the CODATA anchor, packages that residual as an additive $\delta\alpha^{-1}$, and checks that the curvature term closes the gap exactly (within the stated identities).

proof idea

The module defines the required additive mismatch $\delta\alpha^{-1}{\mathrm{req}}$ between RS and CODATA, then the geometric candidate $\delta\alpha^{-1}{\mathrm{geom}}$ from the curvature formula. Equality of the two is proved by direct numerical/algebraic identification. Corrected $\alpha^{-1}$ is RS plus that shift; residual-zero and CODATA-$3\sigma$ membership follow by rewriting. Uniqueness of additive closure for exact alignment is a short uniqueness argument in the additive group of reals (any other additive fix would differ by a nonzero constant). A side lemma forces the curvature exponent inside the natural power family, tying the $\pi^5$ choice to the five-dimensional configuration-space story rather than free parameters. PPM forms of the mismatch are definitional rewrites for reporting.

why it matters in Recognition Science

Without an explicit, unique additive bridge, the RS $\alpha^{-1}$ band cannot be audited against CODATA inside the Lean graph. This pass is that bridge: it names the exact correction, equates it to the curvature-space term $\delta_\kappa=-103/(102\pi^5)$, and records residual-zero plus $3\sigma$ containment. Downstream consumers (none listed yet in the graph) would cite it whenever a theorem claims “RS $\alpha^{-1}$ matches experiment after the geometric curvature correction.” It also locks the exponent story from CurvatureSpaceDerivation into the verification layer, so the $\pi^5$ factor cannot be swapped for another power without breaking the unique-alignment lemmas. Framework landmark: the primer’s $\alpha^{-1}\in(137.030,137.039)$ band is the native target this correction is measured against.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (18)