Documentation

LeanMlir.Proofs.Float.FloatComposeBridge

ℝ→Float32 bridge: per-op FloatClose instances for the conv-net op set #

FloatClose (FloatClose.lean): 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 composes two — the moduli compose as Lg ∘ Lf, magnitudes thread A → B → C.

Instances proved here: floatClose_flatConv (modulus = the conv-fan-in layerBudget), the pools (floatClose_maxPool, floatClose_maxPool3s2, floatClose_gap) and the skips (floatClose_addResidual, floatClose_residualBlock). A whole-net bound would be .comp of these; none is assembled in the repo.

source
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') (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.

source
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).

source
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.

source
theorem Proofs.floatClose_gap {c h w : ℕ} (M : FloatModel) {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.

source
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 skip of floatClose_residualBlock without its ReLU. 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). fun v j => F v j + v j is residual F (Residual.lean) by definition, so this lemma serves that spelling too.

source
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 B + A + u·(B + A) of the real relu(F(x)+x); output magnitude (1+u)(B+A). The defining ResNet op: floatClose_addResidual then floatClose_relu.