alphaInvGenesis_band
plain-language theorem explainer
The inverse fine-structure constant, defined forward from the EM recognition loop as channel budget times forced dressing weight at the spectral load, lies strictly in (137.030, 137.039). Anyone citing the Alpha Genesis certificate or the RS-native α band uses this transfer. Proof is a one-line rewrite by the genesis identity, then the existing numerical bounds on the certified pipeline value.
Claim. The forward inverse coupling satisfies $137.030 < \alpha^{-1}_{\mathrm{genesis}} < 137.039$, where $\alpha^{-1}_{\mathrm{genesis}}$ is the product of the voxel channel budget and the T9 forced continuous weight evaluated at the spectral load.
background
In Alpha Genesis M3 the inverse EM coupling is defined forward, before any measurement comparison. The channel budget is the angular content of the voxel boundary times the passive dressing count: $\Omega(\partial Q_3)\times E_{\mathrm{passive}}=4\pi\times 11$, both factors cube theorems on the D=3 voxel forced by T8. The spectral load is the Parseval-normalized DFT-8 gap weight $w_8$ of the forced $\varphi$-pattern (M2), placed in rung units. Dressing is the unique factorizing recognition weight forced by T9 (M1), evaluated at that load.
The forward object is therefore $\alpha^{-1}_{\mathrm{genesis}}:=\mathrm{channelBudget}\cdot\mathrm{contWeight}(\mathrm{spectralLoad})$. The genesis identity equates this object to the certified pipeline constant $\alpha^{-1}$. The module records four discrete choices: resummation form and $\varphi$-pattern are forced (M1, M2), D=3 is forced upstream (T8), and the remaining named input is the channel-budget bridge reading itself.
proof idea
One-line transfer. Rewrite the goal by the genesis identity, which states that the forward object equals the certified pipeline value $\alpha^{-1}$. The goal becomes the already-proved numerical sandwich on that pipeline constant; discharge both conjuncts by the existing interval lemmas Numerics.alphaInv_gt and Numerics.alphaInv_lt.
why it matters
Closes the band clause of the Alpha Genesis certificate: the structure AlphaGenesisCert bundles seed structure, forced pattern, forced spectral envelope, forced dressing response, genesis identity, and this transferred band. Without the transfer, the forward object would be equal to the pipeline value but not yet known to sit in the RS-native window $(137.030,137.039)$ quoted in the constants primer.
The result is pure bookkeeping once the genesis identity and the numerics bounds exist; its place in the framework is to make the certificate self-contained for the forward definition. It does not touch the honest remaining BRIDGE input (the channel-budget reading), which is named once as ChannelBudgetBridge and is not discharged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.