Closing the CIFAR-BN render — the BN parameter-gradient bridges (dγ, dβ certified)

The non-BN closes (cnn_render_conv{W,b}_certified + the M2 dense bridges) and the BN input-grad (bnPerChannel_grad_input_correct, under 0<ε) already cover every parameter of the CIFAR-BN train step except the per-channel BN scale/shift γ, β. This file supplies their bridges — the BN analogue of IR.bias_grad_bridge / conv_bias_grad.

γ and β enter BN affinely: per channel c, y_(c,s) = γ_c · x̂_(c,s) + β_c, and x̂ does not depend on γ or β. So as a function of γ (resp. β), per-channel BN is x̂ ⊙ gather_channel(γ) + const (resp. const + gather_channel(β)) — a constant scaled by a channel-gather, plus a constant. Its Jacobian therefore collapses through pdiv_add/pdiv_mul/pdiv_const/pdiv_reindex to the sparse indicator ∂y_j/∂γ_idx = x̂_j·[chan j = idx] (resp. [chan j = idx]), and contracting with the cotangent dy gives exactly the rendered per-channel reduces dγ_c = Σ_s dy·x̂, dβ_c = Σ_s dy (the bnParamGradPC block in cifarBnTrainStepStructured). Unlike the BN input grad these need no 0<ε (affine in the params; ε only enters the constant x̂). See planning/archive/render_close_handoff.md §2b.

theorem Proofs.bnPerChannel_grad_gamma_correct (oc m : ℕ) (ε : ℝ) (γ β : Vec oc) (v dy : Vec (oc * m)) (idx : Fin oc) : bnPerChannel_grad_gamma oc m ε v dy idx = ∑ j : Fin (oc * m), pdiv (fun (γ' : Vec oc) => bnPerChannelFlat oc m ε γ' β v) γ idx j * dy j

BN γ-gradient bridge. The rendered per-channel dγ_idx = Σ_s dy·x̂ equals the certified Jacobian of per-channel BN (as a function of γ) contracted with the cotangent dy. The BN analogue of the conv/dense weight bridges; affine in γ, so no 0<ε.

theorem Proofs.bnPerChannel_grad_beta_correct (oc m : ℕ) (ε : ℝ) (γ β : Vec oc) (v dy : Vec (oc * m)) (idx : Fin oc) : bnPerChannel_grad_beta oc m dy idx = ∑ j : Fin (oc * m), pdiv (fun (β' : Vec oc) => bnPerChannelFlat oc m ε γ β' v) β idx j * dy j

BN β-gradient bridge. The rendered per-channel dβ_idx = Σ_s dy equals the certified Jacobian of per-channel BN (as a function of β) contracted with dy. The BN analogue of bias_grad_bridge; affine in β, so no 0<ε.

theorem Proofs.cifar_bn_render_gamma_certified (oc m : ℕ) (ε : ℝ) (γ β : Vec oc) (v dy : Vec (oc * m)) (lr : ℝ) (idx : Fin oc) : γ idx - lr * bnPerChannel_grad_gamma oc m ε v dy idx = γ idx - lr * ∑ j : Fin (oc * m), pdiv (fun (γ' : Vec oc) => bnPerChannelFlat oc m ε γ' β v) γ idx j * dy j

BN γ output certified. γ_c − lr·(rendered dγ_c) denotes γ_c − lr·(certified ∂(per-channel BN)/∂γ_c · cotangent). The γ peer of cnn_render_convb_certified.

theorem Proofs.cifar_bn_render_beta_certified (oc m : ℕ) (ε : ℝ) (γ β : Vec oc) (v dy : Vec (oc * m)) (lr : ℝ) (idx : Fin oc) : β idx - lr * bnPerChannel_grad_beta oc m dy idx = β idx - lr * ∑ j : Fin (oc * m), pdiv (fun (β' : Vec oc) => bnPerChannelFlat oc m ε γ β' v) β idx j * dy j

BN β output certified. β_c − lr·(rendered dβ_c) denotes the certified BN ∂/∂β contraction. The β peer.