channelBudget_pos

In Alpha Genesis M3 the inverse fine-structure constant is built forward from a physical process, not from a fit. 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. Concretely the budget is the product of the discrete Gauss–Bonnet total curvature of the voxel boundary and the passive edge count, $\Omega(\partial Q_3)\times E_{\mathrm{passive}}$.

Both factors are cube theorems (gauss_bonnet_Q3, passive_edges_at_D3); the cube is the forced D=3 voxel (T8). The definition therefore evaluates to the pure number $4\pi\cdot 11$, recorded by channelBudget_eq. The present lemma only records that this number is positive, which is needed before one may form the spectral load (gap weight $w_8$ per unit budget) or invoke division in residual-target arguments.

One-line rewrite-and-positivity proof. Rewrite channelBudget by channelBudget_eq to obtain $4\pi\cdot 11$, then apply Mathlib’s positivity tactic, which discharges $0 < 4$, $0 < \pi$, and $0 < 11$ automatically.

Positivity of the channel budget is the gate for the rest of the genesis certificate. Downstream, spectralLoad_pos is exactly div_pos w8_pos channelBudget_pos, so the spectral load (Parseval-normalized DFT-8 projection of the forced φ-pattern, per unit budget) is well-defined and positive. Residual-target lemmas corrected_at_closingLoad and corrected_eq_codata_iff invoke the same fact to justify division by the budget when uniqueness of the closing load is proved.

In the framework this sits under the Alpha Genesis no-fit table: D=3 is forced (T8), the cube readings are structural, and the only named bridge is the channel-budget identification itself. The lemma does not touch that bridge; it only certifies that the already-evaluated seed $4\pi\cdot 11$ is a positive real, so the forward object alphaInvGenesis := channelBudget · contWeight(spectralLoad) is well-posed and the certified band $(137.030, 137.039)$ can transfer.