existsUnique_closingLoad
plain-language theorem explainer
Exactly one real second-order spectral load makes the dressed inverse fine-structure constant equal the CODATA anchor. Residual-target and α-genesis workers cite this to pin the open seam problem to a single number. The proof is a short package of the explicit closing-load witness with the strict-monotonicity uniqueness iff.
Claim. There exists a unique real number $\delta_2$ such that the load-corrected inverse fine-structure constant at $\delta_2$ equals the external CODATA anchor $\alpha^{-1}_{\mathrm{CODATA}}$.
background
This lives in the Alpha Genesis M4 residual-target quarantine: the only α module allowed to mention the measured value. M1–M3 stay blind to CODATA; here one states the comparison and the open target.
The load-form correction multiplies the channel budget by a continuous weight of total spectral load plus a second-order increment $\delta_2$. That form is forced: second-order terms enter as additional spectral load in the exponent, not as additive display patches. The continuous weight is built from $\rho=1/\varphi\in(0,1)$, so the dressed value is strictly monotone in load.
The closing load is the explicit real that aligns the dressed value with CODATA: $\log(\alpha^{-1}_{\mathrm{CODATA}}/\mathrm{channelBudget})/\log\rho$ minus the first-order spectral load. Upstream, that witness is already shown to hit CODATA, and an iff lemma equates equality to CODATA with equality to that unique load.
proof idea
Term-mode existence-uniqueness package. Existence is the pair (closing load, the theorem that the corrected value at that load equals CODATA). Uniqueness is one application of the forward direction of the corrected-equals-CODATA iff: any $\delta$ with corrected value equal to CODATA must equal the closing load. No further arithmetic is unfolded here; monotonicity and the closed-form inversion sit in the iff lemma.
why it matters
This is item 3 of what the residual-target module claims to prove: existence and uniqueness of the second-order load that closes the residual. It sharpens the open problem to a single number: derive that load from D=3 voxel seam geometry without ever reading CODATA. If a blind seam derivation lands on it (within tolerance), the α program closes at experimental precision; if not, the channel-budget bridge is falsified.
The module's anti-epicycle rule is binding: numerical proximity alone never admits a candidate. The immediately following seam-falsifier definition records the kill condition at definition level. In the broader RS constants story this sits inside the α band near 137.03–137.04 and the forced response/load architecture; it does not itself touch T5–T8, but it is the comparison hinge for the fine-structure assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.