ℝ→Float32 bridge: the composition backbone (whole-net certificate)

A whole-net float certificate is a fold of the per-op budgets. FloatClose packages exactly what's needed to fold: on inputs within magnitude A, the float fF is within an error modulus L e of the real f (per coordinate, at input error e), and both real and float outputs are within B (so the next layer's magnitude precondition is met). FloatClose.comp proves this composes — the moduli compose as Lg ∘ Lf, magnitudes thread A → B → C — so a whole net is FloatClose with the composed modulus, no per-net re-proof.

Instances proved here: relu (exact in float, modulus id) and flatConv (modulus = the conv-fan-in layerBudget). The remaining r34 ops are already *_close lemmas and slot in the same way: BN→relu via bnRelu_close (use the operating-point bnIstd_close_at for the eistd, else the budget is vacuous), maxpool via maxPoolFlat_close, the skip via reluAdd_close. The whole-net certificate is then .comp folded over the layer list.

def Proofs.FloatClose {m n : ℕ} (A B : ℝ) (f fF : Vec m → Vec n) (L : ℝ → ℝ) : Prop

A-posteriori-magnitude, proved-error float closeness, built to compose. A bounds the inputs (both real va and float vt), B both outputs; L is the input-error → output-error modulus.

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.FloatClose.comp {m n p : ℕ} {A B C : ℝ} {f fF : Vec m → Vec n} {g gF : Vec n → Vec p} {Lf Lg : ℝ → ℝ} (hf : FloatClose A B f fF Lf) (hg : FloatClose B C g gF Lg) : FloatClose A C (g ∘ f) (gF ∘ fF) (Lg ∘ Lf)

Float-closeness composes — the whole-net certificate backbone. Magnitudes thread A → B → C, error moduli compose Lg ∘ Lf.

theorem Proofs.floatClose_relu {n : ℕ} (A : ℝ) : FloatClose A A (relu n) (relu n) fun (e : ℝ) => e

ReLU is FloatClose with modulus id — exact in float (real = float map), 1-Lipschitz on the inherited error, never grows magnitudes.

theorem Proofs.floatClose_flatConv {ic oc h w kH kW : ℕ} (M : FloatModel) (W : Kernel4 oc ic kH kW) (b : Vec oc) {w' β A : ℝ} (hw' : 0 ≤ w') (hβ : 0 ≤ β) (hA : 0 ≤ A) (hn : 0 < ic * h * w) (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| ≤ β) : FloatClose A (FloatModel.layerAct (ic * kH * kW) w' β A + FloatModel.layerBudget M.u (ic * kH * kW) w' β A 0) (flatConv W b) (M.flatConvF W b) fun (e : ℝ) => FloatModel.layerBudget M.u (ic * kH * kW) w' β A e

Convolution is FloatClose with modulus the conv-fan-in layerBudget. Real output ≤ layerAct; float output ≤ layerAct + layerBudget(e=0) (the extra rounding) — that sum is the propagated magnitude B.

theorem Proofs.floatClose_dense {m n : ℕ} (M : FloatModel) (W : Mat m n) (b : Vec n) {w' β A : ℝ} (hw' : 0 ≤ w') (hβ : 0 ≤ β) (hA : 0 ≤ A) (hm : 0 < m) (hW : ∀ (i : Fin m) (j : Fin n), |W i j| ≤ w') (hb : ∀ (j : Fin n), |b j| ≤ β) : FloatClose A (FloatModel.layerAct m w' β A + FloatModel.layerBudget M.u m w' β A 0) (dense W b) (M.dense W b) fun (e : ℝ) => FloatModel.layerBudget M.u m w' β A e

Dense layer is FloatClose with modulus the fan-in layerBudget (the dense analogue of floatClose_flatConv). Real output ≤ layerAct; float output ≤ that

• the fresh-input rounding layerBudget(e=0). The SE excite/reduce denses and the classifier head are this instance; the ViT MLP denses reuse it too.

theorem Proofs.floatClose_reluConv {ic oc h w kH kW : ℕ} (M : FloatModel) (W : Kernel4 oc ic kH kW) (b : Vec oc) {w' β A : ℝ} (hw' : 0 ≤ w') (hβ : 0 ≤ β) (hA : 0 ≤ A) (hn : 0 < ic * h * w) (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| ≤ β) : FloatClose A (FloatModel.layerAct (ic * kH * kW) w' β A + FloatModel.layerBudget M.u (ic * kH * kW) w' β A 0) (relu (oc * h * w) ∘ flatConv W b) (relu (oc * h * w) ∘ M.flatConvF W b) ((fun (e : ℝ) => e) ∘ fun (e : ℝ) => FloatModel.layerBudget M.u (ic * kH * kW) w' β A e)

Demo: a conv→relu unit is FloatClose — (conv).comp (relu) folds the conv layerBudget modulus and ReLU's id. A 2-conv chain relu∘conv∘relu∘conv is two more .comps; the whole r34 net is this fold over its layer list (with the BN/maxpool/skip instances slotted in).

theorem Proofs.floatClose_maxPool {c h w : ℕ} (A : ℝ) : FloatClose A A (maxPoolFlat c h w) (maxPoolFlat c h w) fun (e : ℝ) => e

MaxPool is FloatClose with modulus id — exact in float, 1-Lipschitz, never grows magnitudes (maxPoolFlat_close / maxPoolFlat_abs_le).

theorem Proofs.floatClose_maxPool3s2 {c h w : ℕ} (A : ℝ) : FloatClose A A (maxPool3s2Flat c h w) (maxPool3s2Flat c h w) fun (e : ℝ) => e

⭐ He et al.'s 3×3/s2 stem pool is FloatClose — the peer of floatClose_maxPool, and identical in shape: a max is EXACT (it selects an existing cell, so the modulus is id and the magnitude is unchanged) whatever the window size. The overlap that makes the backward accumulate is invisible here, because the forward at one output still reads one cell. planning/archive/rsb_a3_r50_verified.md §4b.

theorem Proofs.floatClose_gap {c h w : ℕ} (M : FloatModel) {A : ℝ} (hA0 : 0 ≤ A) (hhw : 0 < h * w) : FloatClose A (A + (M.u * ((1 + M.u) ^ (h * w + 1) * A) + ((1 + M.u) ^ (h * w + 1) - 1) * A)) (globalAvgPoolFlat c h w) M.gapFlatF fun (e : ℝ) => M.u * ((1 + M.u) ^ (h * w + 1) * A) + ((1 + M.u) ^ (h * w + 1) - 1) * A + e

Global-average-pool is FloatClose — Vec (c·h·w) → Vec c, the SE squeeze. GAP is a per-channel bnMean (globalAvgPoolFlat_eq_bnMean), so the real output never exceeds the input magnitude A (bnMean_abs_le) and is 1-Lipschitz in the input (bnMean_input_close, the spatial mean averages the per-coordinate error back to e); the float roundoff is gapFlat_close's budget gb. Output magnitude A + gb, modulus e ↦ gb + e.

theorem Proofs.floatClose_cifarStage {ic c h w : ℕ} (M : FloatModel) (W₁ : Kernel4 c ic 3 3) (b₁ : Vec c) (W₂ : Kernel4 c c 3 3) (b₂ : Vec c) {w' β A : ℝ} (hw' : 0 ≤ w') (hβ : 0 ≤ β) (hA : 0 ≤ A) (hn1 : 0 < ic * (2 * h) * (2 * w)) (hn2 : 0 < c * (2 * h) * (2 * w)) (hW₁ : ∀ (o : Fin c) (cc : Fin ic) (kh kw : Fin 3), |W₁ o cc kh kw| ≤ w') (hb₁ : ∀ (o : Fin c), |b₁ o| ≤ β) (hW₂ : ∀ (o cc : Fin c) (kh kw : Fin 3), |W₂ o cc kh kw| ≤ w') (hb₂ : ∀ (o : Fin c), |b₂ o| ≤ β) : ∃ (B : ℝ) (L : ℝ → ℝ), FloatClose A B (maxPoolFlat c h w ∘ relu (c * (2 * h) * (2 * w)) ∘ flatConv W₂ b₂ ∘ relu (c * (2 * h) * (2 * w)) ∘ flatConv W₁ b₁) (maxPoolFlat c h w ∘ relu (c * (2 * h) * (2 * w)) ∘ M.flatConvF W₂ b₂ ∘ relu (c * (2 * h) * (2 * w)) ∘ M.flatConvF W₁ b₁) L

THE FOLD: a whole CIFAR stage is FloatClose. conv→relu→conv→relu→maxpool folded through .comp into a single certificate — there exist a propagated magnitude B and an error modulus L (the composition of the two conv layerBudgets through the three id moduli) with the whole float stage within L e of the real stage at input error e. No bespoke proof: the five per-op FloatClose facts chained. The whole r34 net is this same fold at scale (with the BN/skip instances slotted in). ⚠ The ∃ B L closes the modulus, so on its own this statement says only that both maps are bounded on the box.

theorem Proofs.floatClose_residualBlock {m : ℕ} (M : FloatModel) {A B : ℝ} {F FF : Vec m → Vec m} {LF : ℝ → ℝ} (hF : FloatClose A B F FF LF) : FloatClose A (B + A + M.u * (B + A)) (fun (v : Vec m) => relu m fun (j : Fin m) => F v j + v j) (fun (v : Vec m) => relu m fun (j : Fin m) => M.add (FF v j) (v j)) fun (e : ℝ) => M.u * (B + LF e + A + e) + (LF e + e)

Residual block relu(F(x) + x) is FloatClose — the branching combinator (the skip reuses the input, so it's not a plain .comp). Given the body F FloatClose A B, the block's float (rounded skip-add) is within reluAdd_close's budget of the real relu(F(x)+x); output magnitude (1+u)(B+A). The defining ResNet op.

theorem Proofs.floatClose_addResidual {m : ℕ} (M : FloatModel) {A B : ℝ} {F FF : Vec m → Vec m} {LF : ℝ → ℝ} (hF : FloatClose A B F FF LF) : FloatClose A (B + A + M.u * (B + A)) (fun (v : Vec m) (j : Fin m) => F v j + v j) (fun (v : Vec m) (j : Fin m) => M.add (FF v j) (v j)) fun (e : ℝ) => M.u * (B + LF e + A + e) + (LF e + e)

Additive residual F(x) + x (no trailing activation) is FloatClose — the MBConv / transformer skip, the no-ReLU cousin of floatClose_residualBlock. The rounded skip-add fl(FF(x) ⊕ x) is within add_close's budget of the real F(x) + x; output magnitude (1+u)(B+A).

theorem Proofs.floatClose_resBlock {c h w : ℕ} (M : FloatModel) (W₁ W₂ : Kernel4 c c 3 3) (b₁ b₂ : Vec c) {w' β A : ℝ} (hw' : 0 ≤ w') (hβ : 0 ≤ β) (hA : 0 ≤ A) (hn : 0 < c * h * w) (hW₁ : ∀ (o cc : Fin c) (kh kw : Fin 3), |W₁ o cc kh kw| ≤ w') (hb₁ : ∀ (o : Fin c), |b₁ o| ≤ β) (hW₂ : ∀ (o cc : Fin c) (kh kw : Fin 3), |W₂ o cc kh kw| ≤ w') (hb₂ : ∀ (o : Fin c), |b₂ o| ≤ β) : ∃ (B : ℝ) (L : ℝ → ℝ), FloatClose A B (fun (v : Vec (c * h * w)) => relu (c * h * w) fun (j : Fin (c * h * w)) => (flatConv W₂ b₂ ∘ relu (c * h * w) ∘ flatConv W₁ b₁) v j + v j) (fun (v : Vec (c * h * w)) => relu (c * h * w) fun (j : Fin (c * h * w)) => M.add ((M.flatConvF W₂ b₂ ∘ relu (c * h * w) ∘ M.flatConvF W₁ b₁) v j) (v j)) L

THE RESIDUAL FOLD: a (no-BN) ResNet basic block is FloatClose. Body conv₂ → relu → conv₁ folded via .comp, then wrapped by the residual combinator into relu(F(x) + x) — one certificate for the whole block, skip included. The r34 identity block is this with BN inserted (the BN→relu FloatClose instance is the remaining wrap). ⚠ Same caveat as floatClose_cifarStage.

theorem Proofs.floatClose_bnRelu {m : ℕ} (M : FloatModel) {ε γ β emean eistd D S G Bbnd A : ℝ} (fμ fistdv : Vec m → ℝ) (hn : 0 < m) (hε : 0 < ε) (hγ : |γ| ≤ G) (hβ : |β| ≤ Bbnd) (hmean : ∀ (v : Vec m), (∀ (k : Fin m), |v k| ≤ A) → |fμ v - bnMean m v| ≤ emean) (histd : ∀ (v : Vec m), (∀ (k : Fin m), |v k| ≤ A) → |fistdv v - bnIstd m v ε| ≤ eistd) (hD : ∀ (v : Vec m), (∀ (k : Fin m), |v k| ≤ A) → ∀ (j : Fin m), |v j - bnMean m v| ≤ D) (hSabs : ∀ (v : Vec m), (∀ (k : Fin m), |v k| ≤ A) → |bnIstd m v ε| ≤ S) : FloatClose A (G * (D * S) + Bbnd + bnNormBudget M.u D S G Bbnd emean eistd) (fun (v : Vec m) => relu m (bnForward m ε γ β v)) (fun (v : Vec m) => relu m (M.bnForwardF γ β (fμ v) (fistdv v) v)) fun (e : ℝ) => FloatModel.bnReluBudget M.u D S G Bbnd emean eistd A e ε

BN→relu is FloatClose (per-example, training-mode). The float BN computes its stats from the input via the supplied fμ/fistdv (within emean/eistd of the true stats on the magnitude domain — discharged by bnMean_close / bnVar_close + bnIstd_close_at when instantiated). Error from bnRelu_close (rounding + input-shift); float-output magnitude from bnForward_close_of. With this + floatClose_flatConv + the residual combinator, the r34 identity block folds entirely through .comp.

theorem Proofs.floatClose_bn {m : ℕ} (M : FloatModel) {ε γ β emean eistd D S G Bbnd A : ℝ} (fμ fistdv : Vec m → ℝ) (hn : 0 < m) (hε : 0 < ε) (hγ : |γ| ≤ G) (hβ : |β| ≤ Bbnd) (hmean : ∀ (v : Vec m), (∀ (k : Fin m), |v k| ≤ A) → |fμ v - bnMean m v| ≤ emean) (histd : ∀ (v : Vec m), (∀ (k : Fin m), |v k| ≤ A) → |fistdv v - bnIstd m v ε| ≤ eistd) (hD : ∀ (v : Vec m), (∀ (k : Fin m), |v k| ≤ A) → ∀ (j : Fin m), |v j - bnMean m v| ≤ D) (hSabs : ∀ (v : Vec m), (∀ (k : Fin m), |v k| ≤ A) → |bnIstd m v ε| ≤ S) : FloatClose A (G * (D * S) + Bbnd + bnNormBudget M.u D S G Bbnd emean eistd) (fun (v : Vec m) => bnForward m ε γ β v) (fun (v : Vec m) => M.bnForwardF γ β (fμ v) (fistdv v) v) fun (e : ℝ) => FloatModel.bnReluBudget M.u D S G Bbnd emean eistd A e ε

BN alone (no activation) is FloatClose — floatClose_bnRelu with the trailing ReLU dropped, error from bnStep_close (rounding bnForward_close_of

• input-shift bnForward_input_close), same bnReluBudget modulus (ReLU only shrinks, so removing it leaves the budget unchanged). The BN-before-swish steps in EfficientNet's MBConv (and BN-before-GELU positions generally) are this instance.

theorem Proofs.floatClose_id {m : ℕ} (A : ℝ) : FloatClose A A id id id

The identity map is FloatClose (modulus id).

theorem Proofs.floatClose_iterate {m : ℕ} {A : ℝ} {f fF : Vec m → Vec m} {L : ℝ → ℝ} (hf : FloatClose A A f fF L) (n : ℕ) : FloatClose A A f^[n] fF^[n] L^[n]

THE FINAL FOLD: a magnitude-stable block iterated n times is FloatClose. A dim-preserving block that is FloatClose A A f fF L (its activations stay within the a-posteriori bound A — BN keeps them O(1), as the probe confirms) composes with itself to any depth: f^[n] is FloatClose A A with modulus L^[n]. This is r34's within-stage depth (n = 3,4,6,3); the whole net is these iterates .comp-joined with the stem / downsamples / GAP / dense. The depth-generic whole-net certificate — no per-depth re-proof.

theorem Proofs.floatClose_r34_stages {m : ℕ} {A : ℝ} {blk blkF : Vec m → Vec m} {L : ℝ → ℝ} (hblk : FloatClose A A blk blkF L) : FloatClose A A blk^[3] blkF^[3] L^[3] ∧ FloatClose A A blk^[4] blkF^[4] L^[4] ∧ FloatClose A A blk^[6] blkF^[6] L^[6] ∧ FloatClose A A blk^[3] blkF^[3] L^[3]

r34's four stages, folded. Given an identity block that is magnitude-stable FloatClose A A (the a-posteriori-bounded regime), the [3,4,6,3] block stack of each stage is FloatClose A A — the four floatClose_iterate instances at r34's depths. The full r34_float_close is these .comp the stem / strided downsamples / GAP / dense (each its own FloatClose instance).

theorem Proofs.floatClose_residual {m : ℕ} (M : FloatModel) {A B : ℝ} {F FF : Vec m → Vec m} {LF : ℝ → ℝ} (hF : FloatClose A B F FF LF) : FloatClose A (B + A + M.u * (B + A)) (residual F) (fun (v : Vec m) (j : Fin m) => M.add (FF v j) (v j)) fun (e : ℝ) => M.u * (B + LF e + A + e) + (LF e + e)

Additive residual residual f = f(x) + x is FloatClose — the MBConv / transformer skip in the Residual.lean API (residual = biPath f id, defeq to floatClose_addResidual's fun v j => F v j + v j).