deltaAlphaInv_geometric
plain-language theorem explainer
Geometric additive correction to inverse fine structure: CODATA α⁻¹ minus the RS seed/gap formula α_seed·exp(−f_gap/α_seed). Verification authors cite it when locking the symbolic RS α⁻¹ expression to the external anchor. Pure definition over canonical seed, gap weight, and CODATA; no geometric derivation is claimed here.
Claim. Define the geometric closure correction $\delta_{\mathrm{geom}}:=\alpha^{-1}_{\mathrm{CODATA}}-\bigl(\alpha_{\mathrm{seed}}\,e^{-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}}}\bigr)$, where $\alpha_{\mathrm{seed}}=4\pi\cdot 11$ is the ledger spherical seed, $f_{\mathrm{gap}}$ is the eight-tick gap weight, and $\alpha^{-1}_{\mathrm{CODATA}}$ is the CODATA 2022 inverse fine-structure constant.
background
Alpha Resolution Pass 2 turns the residual between the symbolic RS formula for $\alpha^{-1}$ and the CODATA anchor into an explicit additive closure target. The module does not yet derive a new geometric correction; it names the exact mismatch and proves that adding it lands on CODATA.
The RS seed $\alpha_{\mathrm{seed}}=4\pi\cdot 11$ is the baseline spherical closure cost over 11-edge interaction paths. The gap weight $f_{\mathrm{gap}}$ comes from the DFT-8 / eight-tick projection ($w_8\log\varphi$). Their combination $\alpha_{\mathrm{seed}},e^{-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}}}$ is the current symbolic RS $\alpha^{-1}$ (written alphaInv elsewhere in the module). CODATA supplies the external anchor $137.035999177$.
Writing the mismatch directly in seed/gap form removes any separate ad-hoc correction symbol and keeps the target as a derived expression over those canonical ingredients.
proof idea
Definitional, not a proof. The body is the single real expression CODATA anchor minus seed times exponential of minus gap-over-seed. Downstream equalities (identity with the required mismatch, corrected value equals CODATA) follow by simp/unfold against the parallel definition of the symbolic RS formula.
why it matters
This is the named closure term that the rest of Pass 2 builds on. It feeds the corrected inverse-fine-structure definition, the by-construction equality to CODATA, the uniqueness theorem that any additive aligner must equal this term, the existence-uniqueness of exact alignment, and the module-level closure-status bundle.
In the Recognition framework it sits inside the $\alpha^{-1}$ band check (primer: $\alpha^{-1}$ inside $(137.030,137.039)$). The module doc states the open task explicitly: derive this correction (or an equivalent) from RS geometry as a first-principles result. Until that derivation lands, the term is a formal target, not a geometric theorem. Downstream uniqueness then says there is only one additive number that closes the gap, so any future geometric derivation must recover exactly this value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.