The binary32 / E4M3 rounding models, CONSTRUCTED (zero axioms) #
The whole FloatBridge suite is ∀ M : FloatModel, … — abstract over any rounding
operator satisfying the standard relative-error model |rnd x − x| ≤ u·|x|. This file
provides the named hardware-precision inhabitants binary32 / fp8E4M3.
Historically it did so via two explicit axioms (ieeeRnd/ieeeRnd_err — "a rounding
operator at unit roundoff u satisfying the standard model exists"), quarantined from
the zero-axiom Proofs suite. Those axioms are now DISCHARGED (post_audit_roadmap §2):
rndP p is round-to-nearest on the unbounded-exponent p-bit-significand grid —
exactly the idealization the old axiom's docstring said it modeled ("the ∀x form
abstracts away overflow and the subnormal floor") — and rndP_err PROVES the standard
model |rndP p x − x| ≤ 2⁻¹⁻ᵖ·|x| (Higham §2.2) from Mathlib alone: scale into the
binade via Int.zpow_log_le_self, |t − round t| ≤ 1/2, unscale. binary32 = the
p = 23 grid at u32 = 2⁻²⁴; fp8E4M3 = the p = 3 grid at u_e4m3 = 2⁻⁴.
With the named models in hand, the 2026-06 audit's gaps 2 and 3 stay realized:
- gap 2 —
binary32_e4m3_argmax_preserved: the fp8 argmax-preservation theorem, an unconditional corollary about the named hardware models (no∀ M ∀ L). - gap 3 —
binary32_linear_sgd_descends_concrete: one binary32 SGD step on a concrete linear classifier provably decreases the real loss, with the descent smallness conditionshsmall/h1/h2discharged (not assumed) for a concrete(W, x, lr).
WHAT THE DISCHARGE DOES NOT BUY (kept honest): the kernel↔model boundary — FMA
contraction, reduction reassociation, "the GPU behaves like round-to-nearest on this
grid" — remains trusted exactly as before (planning/archive/floatbridge_certificate_gaps.md);
true binary32 also has overflow and a subnormal floor rndP idealizes away
(FloatSubnormalBridge models the latter hypothesis-style). The trust moves from "an
operator with this bound exists" (mathematically mild — id satisfies it at any u ≥ 0)
to a CONCRETE, inspectable operator with the bound proved. The win is hygiene and
inspectability: the repo now contains zero axiom declarations anywhere, and this file
sits inside the ordinary Proofs/AuditAxioms 3-axiom closure like everything else.
Round-to-nearest on the unbounded-exponent p-bit-significand grid.
For x ≠ 0 with binade exponent e = Int.log 2 |x| (i.e. 2^e ≤ |x| < 2^(e+1)),
round x to the nearest multiple of 2^(e−p) — a significand of p fractional
bits, every exponent available. This is IEEE round-to-nearest minus overflow and
subnormals, the standard-model idealization.
Equations
Instances For
The standard model, PROVED (formerly the ieeeRnd_err axiom):
|rndP p x − x| ≤ 2⁻¹⁻ᵖ·|x|. The grid spacing at x is 2^(e−p), nearest-rounding
contributes half a step 2^(e−p−1), and 2^e ≤ |x| turns that into the relative
bound. Mathlib-only: Int.zpow_log_le_self + abs_sub_round.
The FloatModel of the constructed p-bit grid, at any unit roundoff
u ≥ 2⁻¹⁻ᵖ (formerly ieeeModel, whose rnd was the axiom).
Equations
- Proofs.gridModel p u hu = { rnd := Proofs.rndP p, u := u, u_nonneg := ⋯, err := ⋯ }
Instances For
binary32 (IEEE-754 single, fp32 accumulate): the p = 23 grid (24-bit
significand) at unit roundoff u32 = 2⁻²⁴ — the bound is tight for the grid.
Instances For
fp8 E4M3 (the low-precision leaf): the p = 3 grid (3 mantissa bits) at
unit roundoff u_e4m3 = 2⁻⁴, normal-range model.
Instances For
u32 ≤ u_e4m3: fp32 is at least as precise as fp8 (2⁻²⁴ ≤ 2⁻⁴).
Gap 2: the fp8 guarantee for the named hardware models. For the certified
MNIST-linear classifier evaluated with an fp32 accumulate (binary32) / fp8-E4M3 leaf
(fp8E4M3) mixed forward, with trained |W| ≤ 3/5, |b| ≤ 1, pixels |x| ≤ 1:
whenever the exact-ℝ logit margin at the top class k exceeds 122, the deployed
fp8 forward keeps k as the strict argmax. This is linear_e4m3_argmax_preserved
instantiated at the concrete models — no ∀ M ∀ L, no axiom: the models are the
constructed rndP grids (bare 3-axiom closure under #print axioms).
Gap 2, the "loose 122" is a fan-in artifact. The worst-case fp8 logit budget at
the MNIST input dimension (784) is ≤ 61, forcing a > 122 margin. That figure is
≈ 2·u_e4m3 · (m·w·a) — linear in the input dimension m. At a small input
(m = 4) the same worst-case budget is already ≤ 1/2, so a margin of just > 1
certifies the prediction. This makes precise why the deployed net (errors not aligned,
activations far below the m·w·a ceiling) needs only the measured 0.38 drift, not
61: the bound scales with realized fan-in, not the worst-case 784.
The matching argmax corollary at the small input: a margin > 1 (vs > 122 at 784)
suffices for the fp8 forward to preserve the prediction.
The rounding of 0 is 0 (forced by the relative-error model at x = 0).
A rounded dot product against the all-zero vector is 0.
A concrete minimal linear classifier: 2 inputs, 2 classes, all-zero weights,
one-hot input, label 0. The all-zero weights make the exact and float forward both
0, the softmax uniform 1/2, and every gradient sum an exact rational — so the
descent smallness conditions reduce to checkable arithmetic. (A satisfiability
witness for the descent hypotheses, in the spirit of CnnConcrete. The
NON-degenerate sibling is TrainedLinearDescent.trained_linear_sgd_descends_concrete
— the same theorem at TRAINED weights and a real misclassified input.)
Instances For
Gap 3: one binary32 SGD step provably decreases the real loss, with the descent
smallness conditions discharged (not assumed). The step uses the actual
float-computed gradient binary32.linearFloatGrad; the conclusion bounds the real
cross-entropy after the step by the real cross-entropy before minus lr·‖∇‖²/2. All
of hsmall/h1/h2 are proved for the concrete (W0, x0, lr = 1/100). Axiom-free:
binary32 is the constructed rndP 23 grid (bare triple surfaced below).