corrected_at_closingLoad
plain-language theorem explainer
Plugging the closed-form closing load into the load-form correction recovers α⁻¹_CODATA exactly. Anyone citing uniqueness of the residual-closing δ₂ needs this identity. The proof unfolds the definitions, cancels the spectral-load shift by algebra, and finishes with the real power/log inversion for ρ > 0.
Claim. Let $B$ be the EM channel budget, $L$ the first-order spectral load per channel, and $\rho=1/\varphi\in(0,1)$. Define the load-form correction $\alpha^{-1}_{\mathrm{corr}}(\delta_2)=B\,\rho^{L+\delta_2}$ and the closing load $\delta_2^{\star}=\log(\alpha^{-1}_{\mathrm{CODATA}}/B)/\log\rho-L$. Then $\alpha^{-1}_{\mathrm{corr}}(\delta_2^{\star})=\alpha^{-1}_{\mathrm{CODATA}}$.
background
This lives in the Alpha Genesis residual-target quarantine: the only module allowed to mention the measured inverse fine-structure constant. M1–M3 derive the first-order genesis value blind to CODATA; here one compares and localizes the residual.
The channel budget $B$ is the total angular budget of the voxel boundary spread over passive dressing edges (evaluates to $4\pi\cdot 11$). The spectral load $L$ is the gap weight $w_8$ (φ-pattern projection from the eight-tick structure) per unit of that budget. With the dressing response forced, any second-order correction must enter as additional spectral load in the exponent, never as an additive display patch: $\alpha^{-1}_{\mathrm{corr}}(\delta_2)=B,\mathrm{contWeight}(L+\delta_2)$, with continuous weight $\rho^{\cdot}$ for $\rho=1/\varphi$.
The closing load is the explicit real solving that equation for the CODATA anchor: $\delta_2^{\star}=\log(\alpha^{-1}_{\mathrm{CODATA}}/B)/\log\rho-L$. Positivity of $B$ and $\log\rho\neq 0$ (since $\rho\in(0,1)$) make the expression well-defined.
proof idea
Unfold $\alpha^{-1}{\mathrm{corr}}$ and $\delta_2^{\star}$. Positivity of the channel budget and of $\alpha^{-1}{\mathrm{CODATA}}$ gives a positive ratio argument for the log. The exponent $L+(\log(\alpha^{-1}{\mathrm{CODATA}}/B)/\log\rho-L)$ collapses by ring to the pure log ratio. Rewrite the real power via $\mathrm{rpow_def_of_pos}$ (using $\rho>0$), cancel $\log\rho$ in the product by field simplification ($\log\rho\neq 0$), apply $\exp\circ\log$ on the positive ratio, and finish with field_simp to recover $\alpha^{-1}{\mathrm{CODATA}}$.
why it matters
This is the existence half of the residual-target package: the dressed value at the closed-form load hits CODATA on the nose. Downstream, corrected_eq_codata_iff upgrades it to uniqueness (strict decrease in load because $\rho<1$), and existsUnique_closingLoad packages $\exists!,\delta_2$. Together they pin the open Alpha Genesis target to a single real: derive this $\delta_2^{\star}$ from D=3 voxel seam geometry without ever reading CODATA. If a blind seam derivation lands here, the $\alpha$ chain closes at experimental precision inside the RS band; if not, the channel-budget bridge is falsified. The anti-epicycle rule still forbids admitting candidates by numerical proximity alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.