SeamDerivationCloses
plain-language theorem explainer
Names the kill condition for the fine-structure program: a second-order spectral load δ₂ closes the α derivation exactly when the load-corrected inverse fine structure equals the CODATA anchor. Anyone auditing Alpha Genesis M4 or the open seam-geometry target cites this predicate. It is a one-line propositional abbreviation of equality between the corrected value and the external measurement.
Claim. For a real second-order load $\delta_2$, the seam derivation closes when the load-corrected inverse fine-structure constant equals the CODATA 2022 anchor: $\alpha^{-1}_{\mathrm{corr}}(\delta_2) = \alpha^{-1}_{\mathrm{CODATA}}$.
background
This lives in the Alpha Genesis M4 quarantine module, the only layer allowed to mention the measured value. M1–M3 derive a first-order inverse fine structure blind to CODATA; M4 states the residual comparison and the open target.
The load-form correction correctedAlphaInv multiplies the channel budget by the continuous weight of the total spectral load: any second-order term must enter as additional load in the exponent, not as an additive display patch. The external anchor is the CODATA 2022 value $\alpha^{-1} = 137.035999177$.
The module already proves a unique closing load exists: exactly one $\delta_2$ makes the dressed value match the measurement. The open problem is to derive that number from D=3 voxel seam geometry without ever reading CODATA.
proof idea
Definitional abbreviation, not a proof. The predicate is the bare equality of the load-corrected inverse fine structure at $\delta_2$ with the CODATA anchor. Downstream, seam_closes_iff rewrites it via corrected_eq_codata_iff into the unique-load statement $\delta_2 = \mathrm{closingLoad}$.
why it matters
This is the definition-level seam falsifier for the α program. A blind derivation of $\delta_2$ from voxel seam topology either lands on the unique closing load (within tolerance) and closes α at experimental precision, or lands elsewhere and falsifies the channel-budget bridge that feeds M3.
It is consumed immediately by seam_closes_iff, which equates closure with equality to the unique closing load. Framework context: α sits in the RS-native band near 137.03–137.04; the residual target localizes the last free number after the forcing chain and the multiplicative load response. The anti-epicycle rule is binding: numerical proximity alone never admits a candidate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.