ℝ→Float32 bridge: the ResNet-34 structural ops

Extending the float bridge from CIFAR/BN toward ResNet-34. After the rsqrt keystone (BnFloatBridge.lean), no new numerical primitives remain — the r34 ops are reuses or thin wrappers:

• residual skip relu(F(x) + skip(x)) — needs a two-operand add_close (the additive peer of mul_close); reluAdd_close is the post-skip output.
• strided conv — flatConvStride2 = decimateFlat ∘ flatConv, so the float closeness is flatConvF_close at the decimated coordinate.
• per-channel BN — bnPerChannelMat is bnForward applied per channel-row, so bnPerChannelFlat_close_of maps bnForward_close_of over channels.
• global-avg-pool — a per-channel mean, so gapFlat_close reduces to bnMean_close on the channel slice (sum_s2 flattens the spatial double sum).

The remaining work for a whole-net r34_float_close is the (large, mechanical) per-block + whole-net composition threading the inherited error through the 16 residual blocks — no new numerical content.

theorem Proofs.FloatModel.add_close (M : FloatModel) {xt x yt y ex ey : ℝ} (hx : |xt - x| ≤ ex) (hy : |yt - y| ≤ ey) : |M.add xt yt - (x + y)| ≤ M.u * (|x| + ex + |y| + ey) + (ex + ey)

Rounded addition with inherited operand errors. fl(xt ⊕ yt) is within u·(|x| + ex + |y| + ey) + (ex + ey) of the exact x + y, given |xt − x| ≤ ex and |yt − y| ≤ ey. The additive peer of mul_close; the residual fan-in's float budget.

theorem Proofs.FloatModel.reluAdd_close (M : FloatModel) {n : ℕ} {bt b st s : Vec n} {eb es A B : ℝ} (hb : ∀ (i : Fin n), |bt i - b i| ≤ eb) (hs : ∀ (i : Fin n), |st i - s i| ≤ es) (hB : ∀ (i : Fin n), |b i| ≤ A) (hS : ∀ (i : Fin n), |s i| ≤ B) (i : Fin n) : |relu n (fun (j : Fin n) => M.add (bt j) (st j)) i - relu n (fun (j : Fin n) => b j + s j) i| ≤ M.u * (A + eb + B + es) + (eb + es)

Residual block output (post-skip ReLU). With the two branches bt/st within eb/es of the real b/s (magnitudes ≤ A/B), the rounded relu(fl(bt ⊕ st)) is within the add_close budget of relu(b + s) per coordinate (ReLU is exact in float and 1-Lipschitz). The float closeness of relu(F(x) + skip(x)).

noncomputable def Proofs.FloatModel.flatConvStride2F {ic oc h w kH kW : ℕ} (M : FloatModel) (W : Kernel4 oc ic kH kW) (b : Vec oc) : Vec (ic * (2 * h) * (2 * w)) → Vec (oc * h * w)

The float stride-2 conv: decimate the float stride-1 conv (the float peer of flatConvStride2 = decimateFlat ∘ flatConv).

Equations

• M.flatConvStride2F W b = Proofs.decimateFlat oc h w ∘ M.flatConvF W b

theorem Proofs.FloatModel.flatConvStride2F_close {ic oc h w kH kW : ℕ} (M : FloatModel) (W : Kernel4 oc ic kH kW) (b : Vec oc) (vt va : Vec (ic * (2 * h) * (2 * w))) {w' β a e : ℝ} (hw' : 0 ≤ w') (ha : 0 ≤ a) (he : 0 ≤ e) (hW : ∀ (o : Fin oc) (c : Fin ic) (kh : Fin kH) (kw : Fin kW), |W o c kh kw| ≤ w') (hb : ∀ (o : Fin oc), |b o| ≤ β) (hva : ∀ (k : Fin (ic * (2 * h) * (2 * w))), |va k| ≤ a) (hvte : ∀ (k : Fin (ic * (2 * h) * (2 * w))), |vt k - va k| ≤ e) (k : Fin (oc * h * w)) : |M.flatConvStride2F W b vt k - flatConvStride2 W b va k| ≤ layerBudget M.u (ic * kH * kW) w' β a e

Stride-2 conv forward budget. Decimation only selects output coordinates, so the strided-conv closeness is flatConvF_close evaluated at the decimated coordinate — the same conv-fan-in layerBudget.

noncomputable def Proofs.FloatModel.flatConvStride2XlaF {ic oc h w kH kW : ℕ} (M : FloatModel) (W : Kernel4 oc ic kH kW) (b : Vec oc) : Vec (ic * (2 * h) * (2 * w)) → Vec (oc * h * w)

The float XLA-SAME stride-2 conv: the ODD decimation of the float stride-1 conv (the float peer of flatConvStride2Xla = decimateOddFlat ∘ flatConv, StridedConv.lean). The TF-origin stems (EfficientNet-B0, MobileNetV2).

Equations

• M.flatConvStride2XlaF W b = Proofs.decimateOddFlat oc h w ∘ M.flatConvF W b

theorem Proofs.FloatModel.flatConvStride2XlaF_close {ic oc h w kH kW : ℕ} (M : FloatModel) (W : Kernel4 oc ic kH kW) (b : Vec oc) (vt va : Vec (ic * (2 * h) * (2 * w))) {w' β a e : ℝ} (hw' : 0 ≤ w') (ha : 0 ≤ a) (he : 0 ≤ e) (hW : ∀ (o : Fin oc) (c : Fin ic) (kh : Fin kH) (kw : Fin kW), |W o c kh kw| ≤ w') (hb : ∀ (o : Fin oc), |b o| ≤ β) (hva : ∀ (k : Fin (ic * (2 * h) * (2 * w))), |va k| ≤ a) (hvte : ∀ (k : Fin (ic * (2 * h) * (2 * w))), |vt k - va k| ≤ e) (k : Fin (oc * h * w)) : |M.flatConvStride2XlaF W b vt k - flatConvStride2Xla W b va k| ≤ layerBudget M.u (ic * kH * kW) w' β a e

XLA-SAME stride-2 conv forward budget — flatConvStride2F_close at the odd coordinate: the same conv-fan-in layerBudget, since either decimation only selects outputs.

noncomputable def Proofs.FloatModel.bnPerChannelFlatF {oc m : ℕ} (M : FloatModel) (γ β fμ fistdv : Vec oc) (v : Vec (oc * m)) : Vec (oc * m)

The float per-channel BN: bnForwardF per channel-row, with the per-channel mean fμ c and inverse-stddev fistdv c. The float peer of bnPerChannelFlat (= bnForward per row).

Equations

• M.bnPerChannelFlatF γ β fμ fistdv v = Proofs.Mat.flatten fun (c : Fin oc) => M.bnForwardF (γ c) (β c) (fμ c) (fistdv c) (Proofs.Mat.unflatten v c)

theorem Proofs.FloatModel.bnPerChannelFlat_close_of {oc m : ℕ} (M : FloatModel) {ε emean eistd D S G Bbnd : ℝ} (γ β fμ fistdv : Vec oc) (v : Vec (oc * m)) (hmean : ∀ (c : Fin oc), |fμ c - bnMean m (Mat.unflatten v c)| ≤ emean) (histd : ∀ (c : Fin oc), |fistdv c - bnIstd m (Mat.unflatten v c) ε| ≤ eistd) (hD : ∀ (c : Fin oc) (j : Fin m), |Mat.unflatten v c j - bnMean m (Mat.unflatten v c)| ≤ D) (hSabs : ∀ (c : Fin oc), |bnIstd m (Mat.unflatten v c) ε| ≤ S) (hγ : ∀ (c : Fin oc), |γ c| ≤ G) (hβ : ∀ (c : Fin oc), |β c| ≤ Bbnd) (k : Fin (oc * m)) : |M.bnPerChannelFlatF γ β fμ fistdv v k - bnPerChannelFlat oc m ε γ β v k| ≤ bnNormBudget M.u D S G Bbnd emean eistd

Per-channel BN forward closeness. Each channel-row runs bnForward, so the float per-channel BN is within bnNormBudget of bnPerChannelFlat per entry — bnForward_close_of mapped over channels (uniform per-channel mean/ istd errors and magnitude bounds).

noncomputable def Proofs.FloatModel.gapFlatF {c h w : ℕ} (M : FloatModel) (v : Vec (c * h * w)) : Vec c

The float global-average-pool: per channel, the float mean of the channel's h·w spatial slice (rounded sum, rounded /(h·w)). The float peer of globalAvgPoolFlat.

Equations

• M.gapFlatF v ci = M.div (M.sum fun (s : Fin (h * w)) => Proofs.Tensor3.unflatten v ci (finProdFinEquiv.symm s).1 (finProdFinEquiv.symm s).2) ↑(h * w)

theorem Proofs.FloatModel.gapFlat_close {c h w : ℕ} (M : FloatModel) (v : Vec (c * h * w)) {A : ℝ} (hhw : 0 < h * w) (hA : ∀ (ci : Fin c) (hi : Fin h) (wi : Fin w), |Tensor3.unflatten v ci hi wi| ≤ A) (ci : Fin c) : |M.gapFlatF v ci - globalAvgPoolFlat c h w v ci| ≤ M.u * ((1 + M.u) ^ (h * w + 1) * A) + ((1 + M.u) ^ (h * w + 1) - 1) * A

Global-average-pool closeness. GAP is the per-channel spatial mean, so the float GAP is within the bnMean_close budget of globalAvgPoolFlat per channel (sum_s2 flattens the spatial double sum to the Fin (h·w) slice the mean rounds).

theorem Proofs.globalAvgPoolFlat_eq_bnMean {c h w : ℕ} (v : Vec (c * h * w)) (ci : Fin c) : globalAvgPoolFlat c h w v ci = bnMean (h * w) fun (s : Fin (h * w)) => Tensor3.unflatten v ci (finProdFinEquiv.symm s).1 (finProdFinEquiv.symm s).2

GAP as a per-channel bnMean. globalAvgPoolFlat c h w v ci is the mean of channel ci's spatial slice — bnMean (h·w) of the Fin (h·w)-indexed gather. The reduction gapFlat_close performs inline, exposed so the float-bridge magnitude/input-shift bounds (bnMean_abs_le / bnMean_input_close) apply.