theorem Proofs.Tensor3.sum_flatten {c h w : ℕ} (T : Tensor3 c h w) : ∑ k : Fin (c * h * w), T.flatten k = ∑ i : Fin c, ∑ j : Fin h, ∑ l : Fin w, T i j l

Summing a flattened Tensor3 is the triple sum.

theorem Proofs.Tensor3.flatten_mul {c h w : ℕ} (A B : Tensor3 c h w) (k : Fin (c * h * w)) : A.flatten k * B.flatten k = flatten (fun (i : Fin c) (j : Fin h) (l : Fin w) => A i j l * B i j l) k

Flattening commutes with a pointwise product: both sides look up the same index.

noncomputable def Proofs.convWindow3 {ic h w : ℕ} (kH kW : ℕ) (x : Tensor3 ic h w) (hi : Fin h) (wi : Fin w) : Tensor3 ic kH kW

The kH × kW receptive field conv2d reads at output pixel (hi, wi), zero outside — conv2d's own if hpad … branch, lifted out so the conv's fan-in is a Tensor3.

⚠⚠ The 3 suffix is NOT decoration — it is what makes this file importable. SgdDescentCnn.lean already declares Proofs.convWindow for the SAME receptive field at the FLAT type Vec (ic*kH*kW). Two constants cannot share a full name, so while this one was also called convWindow the two could not coexist in one environment: lake build LeanMlir failed outright at import … ConvMixedFloatBridge failed, environment already contains 'Proofs.convWindow', which is exactly the import a whole-net bound has to make. ▶ The Tensor3 shape is deliberate and stays — conv2d_eq_flat_dot needs Tensor3.sum_flatten — so the name moved rather than the type.

Equations

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

noncomputable def Proofs.convSlice {ic oc kH kW : ℕ} (W : Kernel4 oc ic kH kW) (o : Fin oc) : Tensor3 ic kH kW

The output channel's kernel slice, as a Tensor3.

Equations

• Proofs.convSlice W o c kh kw = W o c kh kw

theorem Proofs.conv2d_eq_flat_dot {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (x : Tensor3 ic h w) (o : Fin oc) (hi : Fin h) (wi : Fin w) : conv2d W b x o hi wi = b o + ∑ k : Fin (ic * kH * kW), (convSlice W o).flatten k * (convWindow3 kH kW x hi wi).flatten k

⭐ A convolution output is a DOT PRODUCT of length ic·kH·kW over the flattened receptive field. This is the whole reason conv_close_mixed is not a new hard theorem: it lets the conv reuse dot_close_mixed_uniform at that fan-in.

noncomputable def Proofs.convBr (M L : FloatModel) (n : ℕ) : ℝ

The Higham-style bracket dot_close_mixed_uniform produces at fan-in n: fan-in amplification rides the ACCUMULATE precision M.u, the leaf precision contributes a flat per-leaf term.

Equations

• Proofs.convBr M L n = ((1 + M.u) ^ (n + 1) - 1) * (1 + L.u) ^ 2 + (2 * L.u + L.u ^ 2)

noncomputable def Proofs.convFanS {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (x : Tensor3 ic h w) (o : Fin oc) (hi : Fin h) (wi : Fin w) : ℝ

Σ|kernel·window| over the receptive field — the magnitude the bound scales.

Equations

• Proofs.convFanS W x o hi wi = ∑ k : Fin (ic * kH * kW), |(Proofs.convSlice W o).flatten k * (Proofs.convWindow3 kH kW x hi wi).flatten k|

noncomputable def Proofs.FloatModel.convMixed (M L : FloatModel) {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (x : Tensor3 ic h w) : Tensor3 oc h w

The mixed-precision convolution, as the emitted graph computes it. Operands rounded to the leaf precision L and accumulated at M (dotMixed), the accumulator then rounded to L again — the bf16-typed result, i.e. the store — and only then the bias added at M.

⚠ The second L.rnd is what distinguishes this from denseMixed, and it is not optional: BatchableOp.convBf16 must give the convolution a bf16-typed result or XLA deletes the casts and runs the whole conv in f32. The store is a consequence of the only emit shape that reaches the tensor cores, so the error model has to carry it.

Equations

• M.convMixed L W b x o hi wi = M.add (L.rnd (M.dotMixed L (Proofs.convSlice W o).flatten (Proofs.convWindow3 kH kW x hi wi).flatten)) (b o)

theorem Proofs.FloatModel.conv_close_mixed (M L : FloatModel) {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (x : Tensor3 ic h w) (o : Fin oc) (hi : Fin h) (wi : Fin w) : |M.convMixed L W b x o hi wi - conv2d W b x o hi wi| ≤ M.u * ((1 + L.u) * (1 + convBr M L (ic * kH * kW)) * convFanS W x o hi wi + |b o|) + L.u * (1 + convBr M L (ic * kH * kW)) * convFanS W x o hi wi + convBr M L (ic * kH * kW) * convFanS W x o hi wi

⭐⭐ Mixed-precision convolution forward error. Three terms, one per rounding the emitted graph performs: the dot (convBr, fan-in ic·kH·kW), the bf16 STORE of the accumulator (L.u), and the f32 bias add (M.u).

▶ It is dot_close_mixed_uniform instantiated at the conv's fan-in, because a convolution output IS a dot product over its flattened receptive field (conv2d_eq_flat_dot). The fan-in wall therefore still sits at 1/M.u = 2²⁴ and not at the leaf precision — the same reason bf16-mixed is non-vacuous for dense.