channelBudget_eq
plain-language theorem explainer
The EM recognition-loop channel budget equals $4\pi\cdot 11$, the product of discrete Gauss-Bonnet curvature on the voxel boundary and the passive edge count. Anyone citing the Alpha Genesis seed or the forward $\alpha^{-1}$ construction needs this identity. The proof is a one-line appeal to the geometric-seed evaluation already proved in AlphaDerivation.
Claim. The channel budget of the EM recognition loop equals $4\pi \cdot 11$.
background
In Alpha Genesis M3, inverse fine structure is built forward from a physical process, not fitted to data. The first ingredient is the channel budget: one active edge transition of the EM recognition loop is spread over the passive dressing field of the D=3 voxel. Module language writes this as $\Omega(\partial Q_3)\times E_{\mathrm{passive}}$, discrete Gauss-Bonnet total curvature of the cube boundary times the passive edge count.
Both factors are cube theorems (gauss_bonnet_Q3, passive_edges_at_D3); D=3 itself is forced upstream (T8). The local definition simply aliases the channel budget to AlphaDerivation.geometric_seed. Upstream, geometric_seed_eq already records that this seed equals $4\pi\cdot 11$. A separate cosmology identity also called geometric seed (11/16 passive mode fraction) is a different object and is not used here.
proof idea
One-line term proof: unfold nothing locally; apply AlphaDerivation.geometric_seed_eq directly. That upstream theorem unfolds the geometric seed, rewrites by the solid-angle identity on $Q_3$, and simplifies the passive-edge factor to 11. Because channelBudget is definitionally that seed, the equality transfers.
why it matters
This is clause (1) of the Alpha Genesis certificate: the verified predicate on AlphaGenesisCert opens with channelBudget = 4 * Real.pi * 11. Downstream, channelBudget_eq_alpha_seed rewrites the budget onto the certified pipeline seed, and channelBudget_pos gets positivity by the same rewrite plus a positivity tactic.
In the no-fit table, the cube reading of the seed is structural (Gauss-Bonnet and passive edges on the T8-forced D=3 voxel). The remaining physical identification is the named bridge ChannelBudgetBridge (inverse coupling as angular budget times passive channels), not a continuous fit. The identity feeds the forward object alphaInvGenesis := channelBudget · contWeight(spectralLoad), whose equality with the certified $\alpha^{-1}$ transfers the band $(137.030, 137.039)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.