ℝ→Float32 bridge: assembling a ResNet block step

The first genuinely-composed block step: relu(BN(·)) where the BN input is the perturbed float activation (the output of an upstream float conv). This is where the per-block composition becomes real — the BN closeness splits into

rounding-at-fixed-input (bnForward_close_of, the float BN's own roundoff)

• input-shift (bnForward_input_close, real BN moving with its input)

and relu_close carries it through the (exact-in-float) ReLU. bnRelu_close proves exactly that. A full identity block relu(F(x) + x) is then this step twice (drop the inner ReLU on the second) chained through flatConvF_close for each conv and closed by reluAdd_close at the skip — the same parts, no new numerical content.

noncomputable def Proofs.FloatModel.bnReluBudget (u D S G Bbnd emean eistd A e1 ε : ℝ) : ℝ

Budget of the BN→relu block step: the BN rounding (bnNormBudget) plus the real-BN input-shift from a per-coordinate input error e1 at BN-input magnitude A (δ ≤ e1 collapses the mean term).

Equations

• Proofs.FloatModel.bnReluBudget u D S G Bbnd emean eistd A e1 ε = Proofs.bnNormBudget u D S G Bbnd emean eistd + G * ((e1 + e1) * (1 / √ε) + 2 * A * (8 * A * e1 / (2 * ε * √ε)))

theorem Proofs.FloatModel.bnStep_close (M : FloatModel) {n : ℕ} {ε γ β emean eistd D S G Bbnd A e1 fμ fistdv : ℝ} (vt va : Vec n) (i : Fin n) (hn : 0 < n) (hε : 0 < ε) (he1 : ∀ (k : Fin n), |vt k - va k| ≤ e1) (hAvt : ∀ (k : Fin n), |vt k| ≤ A) (hAva : ∀ (k : Fin n), |va k| ≤ A) (hmean : |fμ - bnMean n vt| ≤ emean) (histd : |fistdv - bnIstd n vt ε| ≤ eistd) (hD : ∀ (j : Fin n), |vt j - bnMean n vt| ≤ D) (hSabs : |bnIstd n vt ε| ≤ S) (hγ : |γ| ≤ G) (hβ : |β| ≤ Bbnd) : |M.bnForwardF γ β fμ fistdv vt i - bnForward n ε γ β va i| ≤ bnReluBudget M.u D S G Bbnd emean eistd A e1 ε

BN forward block step closeness (no activation). With the BN input vt (float) within e1 of va (real) per coordinate (both magnitude ≤ A), the float per-example BN mean/istd within emean/eistd of the real ones at vt, and the usual BN magnitude bounds, the rounded bnForwardF vt is within bnReluBudget of bnForward va. The composition split: rounding (bnForward_close_of) + input-shift (bnForward_input_close). This is the pre-activation bound; bnRelu_close is relu_close on top, and the BN-before- swish path in EfficientNet's MBConv uses this one directly.

theorem Proofs.FloatModel.bnRelu_close (M : FloatModel) {n : ℕ} {ε γ β emean eistd D S G Bbnd A e1 fμ fistdv : ℝ} (vt va : Vec n) (i : Fin n) (hn : 0 < n) (hε : 0 < ε) (he1 : ∀ (k : Fin n), |vt k - va k| ≤ e1) (hAvt : ∀ (k : Fin n), |vt k| ≤ A) (hAva : ∀ (k : Fin n), |va k| ≤ A) (hmean : |fμ - bnMean n vt| ≤ emean) (histd : |fistdv - bnIstd n vt ε| ≤ eistd) (hD : ∀ (j : Fin n), |vt j - bnMean n vt| ≤ D) (hSabs : |bnIstd n vt ε| ≤ S) (hγ : |γ| ≤ G) (hβ : |β| ≤ Bbnd) : |relu n (M.bnForwardF γ β fμ fistdv vt) i - relu n (bnForward n ε γ β va) i| ≤ bnReluBudget M.u D S G Bbnd emean eistd A e1 ε

BN → relu block step closeness. relu_close on top of bnForward_close: the rounded relu(bnForwardF vt) is within bnReluBudget of relu(bnForward va) (ReLU is exact in float and 1-Lipschitz, so it carries the pre-activation bound through unchanged).