channelBudgetBridge
plain-language theorem explainer
Packages the single named physical input of Alpha Genesis: inverse EM coupling at leading order equals voxel solid angle times passive dressing channels. Both factors are cube theorems (Gauss–Bonnet on ∂Q₃ and the D=3 passive-edge count), so the instance is non-vacuous. Cited by anyone assembling the forward α⁻¹ certificate. Construction is a one-field structure fill from the structural seed equality.
Claim. There is a channel-budget bridge: the EM channel budget equals the solid angle of the cube boundary $Q_3$ times the number of passive field edges at spatial dimension $D=3$, i.e. $\mathrm{budget}=\Omega(\partial Q_3)\times E_{\mathrm{passive}}=4\pi\times 11$.
background
Alpha Genesis defines $\alpha^{-1}$ forward, before any measurement comparison. The channel budget is the EM recognition loop spreading one active edge transition over the passive dressing field of the D=3 voxel: $\Omega(\partial Q_3)\times E_{\mathrm{passive}}=4\pi\times 11$. Both factors are cube theorems; D=3 is forced upstream (T8).
The structure ChannelBudgetBridge isolates the one remaining physical identification: inverse coupling budget equals angular budget times passive channels. Module status marks every numbered clause as theorem and this reading as BRIDGE. The same 11 reappears in $\Omega_\Lambda=11/16$, $\eta_B$ arithmetic, and the lepton torsion ladder (cross-application rigidity).
Upstream, alpha_seed_structural states that the geometric seed factorizes as solid angle times passive channels with zero imported constants, proved by rfl against the cube geometry definitions.
proof idea
One-field structure instance. The sole obligation is seed_reading, the equality of channel budget to solid angle times passive edges. It is discharged by direct assignment of alpha_seed_structural, the structural factorization theorem from AlphaDerivation (itself rfl on the cube geometry). No further tactics.
why it matters
This is the honest remaining input of the no-fit proposition for $\alpha^{-1}$. After M1 (response forced to $\exp(-\varepsilon)$, additive display excluded), M2 (every admissible ladder is $\varphi^t$; spectral envelope forced), and T8 (D=3), the only named physical identification left is the channel-budget reading. Packaging it as a first-class bridge makes the certificate's dependency explicit: theorems for all numbered clauses, BRIDGE once for the seed reading.
It underwrites the forward object $\alpha^{-1}_{\mathrm{genesis}}:=\mathrm{budget}\cdot\mathrm{contWeight}(\mathrm{spectralLoad})$ and the transfer of the proved band $(137.030,137.039)$. No CODATA reference enters. Downstream the genesis certificate bundles this bridge with the forced pattern, measure, and dressing clauses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.