seam_closes_iff
plain-language theorem explainer
A blind second-order spectral load closes the fine-structure residual exactly when it equals the unique CODATA-aligned closing load. Auditors of the Alpha Genesis quarantine and the seam-geometry open target cite this biconditional as the kill condition. The proof is a one-line term rephrasing of the uniqueness theorem for the dressed inverse-alpha.
Claim. For every real second-order load $\delta_2$, the seam-derivation closing predicate holds if and only if $\delta_2$ equals the unique closing load. Equivalently, the dressed inverse fine-structure constant at load $\delta_2$ equals the CODATA value precisely when $\delta_2$ is that closing load.
background
This module is the quarantine layer of Alpha Genesis: the only place allowed to mention the measured CODATA inverse-alpha. M1–M3 stay blind by construction. The residual is the certified gap between the structural band and CODATA. Any second-order correction must enter as additional spectral load in the exponent (multiplicatively), never as an additive display patch; the legacy additive tail is retired.
The dressed inverse-alpha is the channel budget times a power of the measure-forcing ratio $\rho=1/\varphi$, with total exponent equal to first-order spectral load plus $\delta_2$. Because $\rho<1$ the map is strictly decreasing in the load, so exactly one real $\delta_2$ aligns the dressed value with CODATA. That value is the closing load, written in closed form as $\log(\alpha^{-1}_{\mathrm{CODATA}}/\mathrm{channelBudget})/\log\rho$ minus the first-order spectral load.
The seam-closing predicate packages the kill condition: a candidate load from blind seam geometry closes the program exactly when the dressed value hits CODATA. Upstream uniqueness already proves that equality holds iff the load is the closing load.
proof idea
One-line term wrapper. Unfolding the seam-closing predicate turns the goal into equality of the dressed inverse-alpha with CODATA, which is exactly the left-hand side of the upstream uniqueness theorem. Applying that theorem (strict decrease of the dressed map in the load, $\rho<1$) discharges both directions at once.
why it matters
Localizes the open Alpha Genesis target: derive the closing load from D=3 voxel seam topology without ever referencing CODATA. If a blind derivation lands on that number (within tolerance), the alpha program closes at experimental precision; any other value falsifies the channel-budget bridge of M3. The declaration restates the definition-level seam falsifier as a proved biconditional, so audits can cite a theorem rather than a Prop def. No downstream uses yet; it sits at the tip of the residual-target quarantine. It enforces the binding anti-epicycle rule: numerical proximity to the closing load is never admission. Framework context is the RS alpha band near $(137.030,137.039)$ and the forced multiplicative response of the constants pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.