corrected_eq_codata_iff
plain-language theorem explainer
The dressed inverse fine-structure constant equals the CODATA anchor if and only if the second-order spectral load equals the unique closing load. Anyone localizing the open α seam-derivation target cites this equivalence. The proof is an iff: one direction rewrites the known closing identity; the other cancels the positive channel budget and uses strict antitonicity of ρ^x for ρ∈(0,1).
Claim. For every real second-order load $\delta_2$, the load-corrected inverse fine-structure value equals the CODATA anchor $\alpha^{-1}_{\mathrm{CODATA}}$ if and only if $\delta_2$ equals the closed-form closing load $\delta_2^{\star}=\log(\alpha^{-1}_{\mathrm{CODATA}}/B)/\log\rho-L$, where $B$ is the channel budget and $L$ is the first-order spectral load per channel.
background
This lives in the Alpha Genesis residual-target quarantine: the only module allowed to mention the measured $\alpha^{-1}$. Upstream M1–M3 stay CODATA-blind; here one compares the dressed prediction to the external anchor and isolates a single open number.
The channel budget $B$ is the EM loop angular budget $\Omega(\partial Q_3)\times E_{\mathrm{passive}}$ (evaluating to $4\pi\cdot 11$). The spectral load $L=w_8/B$ is the eight-tick gap weight per unit budget. The load-form correction is $B\cdot\rho^{L+\delta_2}$ (equivalently $B$ times the continuous weight at total load $L+\delta_2$), forced by the response theorem: second-order terms enter only as additional spectral load in the exponent, never as additive display patches.
The closing load is defined by solving that formula for equality with $\alpha^{-1}_{\mathrm{CODATA}}$. A prior lemma already shows the formula hits CODATA exactly at that load. The measure-forcing base $\rho=1/\varphi\in(0,1)$ makes the map $\delta_2\mapsto\rho^{L+\delta_2}$ strictly decreasing, which is the uniqueness engine.
proof idea
Split the biconditional.
($\Rightarrow$) Assume the corrected value at $\delta_2$ equals CODATA. Rewrite via the known identity that the corrected value at the closing load also equals CODATA, so the two corrected values agree. Unfold the definition and cancel the positive channel budget to obtain $\rho^{L+\delta_2}=\rho^{L+\delta_2^{\star}}$. If the exponents differed, strict increase of $x\mapsto\rho^x$ under raising the exponent when $0<\rho<1$ (Mathlib rpow_lt_rpow_of_exponent_gt with $\rho>0$ and $\rho<1$) would contradict equality of the powers. Hence the exponents match, and cancelling $L$ yields $\delta_2=\delta_2^{\star}$.
($\Leftarrow$) Substitute $\delta_2=\delta_2^{\star}$ and apply the prior closing identity.
why it matters
This is the uniqueness half of the residual-target package. It feeds existsUnique_closingLoad (exactly one real load hits CODATA) and seam_closes_iff (a seam derivation closes precisely when it returns the closing load).
In the Alpha Genesis story the first-order assembly is already forced; the residual after that assembly sits in a certified band of width a few parts in $10^3$. Any remaining correction must be pure additional spectral load. The present iff collapses the comparison to CODATA onto a single real parameter $\delta_2^{\star}$. The open problem is then sharply localized: derive that number from D=3 voxel seam geometry without ever reading CODATA. Landing on it closes $\alpha$ at experimental precision; landing elsewhere falsifies the channel-budget bridge. The anti-epicycle rule forbids admitting candidates by numerical proximity alone.
Framework landmarks in play: the eight-tick gap weight behind $w_8$, the $\varphi$-forced base $\rho=1/\varphi$, and the quarantine separation that keeps M1–M3 measurement-blind.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.