The mixed-precision conv as a FloatClose — the whole-net bf16 bound #
FloatModel.conv_close_mixed bounds one bf16-mixed convolution against exact ℝ at
an exactly-represented input. That is not enough to compose: a net feeds each layer the
previous layer's already-perturbed output, so what a fold needs is an error modulus — a map
from inherited input error to output error — plus a magnitude bound to thread forward. That pair
is FloatClose (FloatComposeBridge.lean), and this file supplies its mixed-precision conv instance.
⭐⭐ The composition backbone is PRECISION-AGNOSTIC, and that is the whole reason this is
small. FloatClose A B f fF L says nothing about how fF rounds — only that it stays within
L e of f. So floatClose_relu, floatClose_bn, floatClose_maxPool3s2, floatClose_gap,
floatClose_residualBlock, floatClose_iterate and FloatClose.comp apply to a bf16 conv
UNCHANGED. One new instance buys the entire existing fold (the [3,4,6,3] assembly it once
fed, Resnet34WholeFloatBridge, was deleted with the whole-net budgets on 2026-09-08).
What genuinely had to be proved here, none of which the e = 0 bound gives:
convFanS_le— the data-dependentΣ|kernel·window|replaced by the closed formn·w·A, so the budget is a formula in dims and norms rather than in the input.conv2d_sub_abs_le— the REAL conv isn·w-Lipschitz in its input. This is the term that carries a predecessor's error through the layer, and it has no analogue ate = 0.convMixedBudget/convMixed_close_prop— the two combined, at an input that is both perturbed (E) and magnitude-bounded (A).
⚠ The budget is evaluated at A + E, not A. The float conv runs on the PERTURBED input, so
its own rounding scales with the perturbed magnitude; only the real conv sees A. Writing A
there would understate the bound — the unsound direction.
▶ n = ic·kH·kW throughout, and the fan-in amplification rides uacc (fp32) while uleaf
(bf16) enters flat — the §9.3 separation that makes this non-vacuous at R50's n = 4608.
The window inherits the input's magnitude bound — the padded branch is 0, which needs
0 ≤ A rather than the hypothesis.
⭐ The window inherits the input's PERTURBATION. The padding branch is the same branch for
both tensors (it depends only on the indices), so it contributes |0 - 0| = 0 ≤ E.
The data-dependent fan-in sum, bounded by dims and norms. conv_close_mixed scales
everything by convFanS W x o hi wi = Σ|kernel·window|; this replaces it by n·w·A, which
is what turns that theorem into a budget a fold can carry.
⭐⭐ conv2d is n·w-Lipschitz. THE term with no analogue at e = 0: it is how a
predecessor layer's error reaches this layer's output. The bias cancels (it is the same in
both), so the difference is one dot product against the window difference.
convBr as a function of the two roundoffs alone — the same bracket, with the FloatModels
peeled off so a concrete instance evaluates by norm_num.
Equations
Instances For
⭐⭐ The mixed-precision conv budget — the layerBudget peer, and the object this whole
file exists to produce. Four terms:
uacc * (… + β)— the f32 bias add,uleaf * (1+br) * …— the bf16 store of the accumulator (the bf16-TYPED conv result, forced by the only emit shape that reaches tensor cores; §9.2),br * …— the dot itself, fan-innamplified at the ACCUMULATE precision,n·w·E— the inherited error, carried through by the real conv's Lipschitz constant.
⚠ The first three are evaluated at A + E, not A: the float conv runs on the PERTURBED
input, so its own rounding scales with the perturbed magnitude. Only the fourth term is
linear in E alone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
⭐⭐ Mixed-precision convolution against exact ℝ at a PERTURBED input. The composable
peer of conv_close_mixed, which is this at E = 0 and with the data-dependent convFanS
left in place.
Two steps: the float conv is conv_close_mixed at its OWN input xt (whose magnitude is
A + E), and the real conv moves from xt to xa by conv2d_sub_abs_le.
Vec-space mixed-precision conv — the bf16 peer of FloatModel.flatConvF, in the flat
space the ResNet composition actually lives in.
Equations
- M.flatConvMixed L W b v = (M.convMixed L W b (Proofs.Tensor3.unflatten v)).flatten
Instances For
The Vec-space propagating bound — convMixed_close_prop transported through
flatten/unflatten, exactly as flatConvF_close transports convF_close.
⭐⭐⭐ THE INSTANCE: a bf16-mixed convolution is FloatClose. Magnitude A in, real
output ≤ layerAct and float output ≤ layerAct + convMixedBudget(E := 0) out; error
modulus E ↦ convMixedBudget … E.
▶ This is the ONLY thing the whole-net bf16 bound needed. Everything the f32 fold already
has — floatClose_relu, floatClose_bn, floatClose_maxPool3s2, floatClose_gap,
floatClose_residualBlock, floatClose_iterate, FloatClose.comp — is stated on
FloatClose and therefore applies to this verbatim.
The per-layer error GAIN — the coefficient of the inherited error E in
convMixedBudget. This is the number that compounds: a d-layer stack multiplies its
input error by gain^d, so the gain, not the additive constant, is what decides whether a
composed bound says anything.
Equations
- Proofs.convMixedGain uacc uleaf n w = ↑n * w * (1 + Proofs.convBrR uacc uleaf n + uleaf * (1 + Proofs.convBrR uacc uleaf n) + uacc * ((1 + uleaf) * (1 + Proofs.convBrR uacc uleaf n)))
Instances For
⭐ convMixedBudget is AFFINE in the inherited error, with slope convMixedGain. So
composing d of these is gain^d on the input error plus a geometric sum of the additive
terms — the shape every composed forward-error bound has.
The f32 peer, for comparison. layerBudget is affine in E too, with slope
m·w·(1+u)^(m+2). ▶ Both slopes are fan-in · weight-bound times a factor that is
1 + O(roundoff), which is the point of the next comment.
⭐⭐ THE HONEST READING, and it is the useful result of this file.
Both gains factor as n·w · (1 + ε):
- f32:
ε = (1+u_acc)^(n+2) − 1, which atu_acc = 2⁻²⁴,n = 4608is 2.7e-4; - bf16-mixed:
ε ≈ br + u_leaf(1+br) + u_acc(1+u_leaf)(1+br), which atu_leaf = 2⁻⁸is 1.20e-2 — dominated bybr's flat leaf term, exactly as §9.3 found for one layer.
▶ So bf16 does NOT change the whole-net bound's growth RATE — it changes a 1+ε factor.
(1.012043/1.000275)^d over d conv layers: 1.52× at R34's 36 and 1.86× at R50's 53.
Under a factor of two on the certificate, for a 1.41×/1.55× speedup. (Arithmetic outside
Lean, quoted as illustration; the affine decomposition above is what is proved.)
⚠⚠ AND BOTH BOUNDS ARE VACUOUS IN ABSOLUTE TERMS, which this file will not pretend
otherwise. The shared n·w factor is ≫ 1 at any real layer (n = 4608, w' ≈ 0.05 gives
~230), so gain^53 is astronomical for the f32 bound and the bf16 one alike. That is a
property of worst-case forward-error analysis composed depth-first — every term assumes the
adversarial sign — not a property of bf16, and the f32 whole-net bridges the repo carried
until 2026-09-08 had exactly the same factor. ▶ What is meaningful here is the
RATIO: bf16's certificate is ~2× the f32 certificate, not exponentially worse. Anyone
wanting a non-vacuous absolute number needs a different analysis (probabilistic rounding,
or a bound that exploits BN's renormalisation at each layer), not a tighter conv lemma.
conv→relu in bf16 is FloatClose — the bf16 peer of floatClose_reluConv, and the
proof is the same one line, because floatClose_relu never asked what precision fed it.
⭐ Two bf16 convs chained — the .comp of two mixed-precision layers, moduli composing.
This is the inductive step of any depth; nothing about it is conv-specific or R50-specific.
⭐⭐ R50's [3,4,6,3] stage fold, in bf16 — and it is floatClose_r34_stages verbatim.
ResNet-50 has the SAME stage depths as ResNet-34; the two differ in what a block contains
(three convs with a 1×1 bottleneck vs two 3×3s), not in how many blocks a stage stacks. So
the depth fold needs no R50-specific theorem — only an R50 block instance, which is what
floatClose_flatConvMixed now makes constructible in bf16.
▶ Stated here under the same magnitude-stability hypothesis the f32 fold uses: a block whose
activations stay within A (which is what BN buys, and what the a-posteriori probe checks).