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.
The models are constructed, not assumed: rndP p is round-to-nearest on the
unbounded-exponent p-bit-significand grid (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 uE4M3 = 2⁻⁴.
Two corollaries about the named models:
binary32_e4m3_argmax_preserved: the fp8 argmax-preservation theorem, a corollary about the named hardware models (no∀ M ∀ L).binary32_linear_sgd_descends_concrete: one binary32 SGD step on a concrete linear classifier (2 inputs, 2 classes, all-zero weightsW0) provably decreases the real loss, with the descent smallness conditionshsmall/h1/h2discharged (not assumed) for a concrete(W, x, lr).
What stays trusted: the kernel↔model boundary — FMA contraction, reduction reassociation,
"the GPU behaves like round-to-nearest on this grid". True binary32 also has overflow and a
subnormal floor that rndP idealizes away; no subnormal-aware model is stated. The file declares no axiom and sits inside the ordinary
Proofs/AuditAxioms 3-axiom closure.
rndP and its standard model rndP_err live in RndP.lean.
The FloatModel of the constructed p-bit grid, at any unit roundoff
u ≥ 2⁻¹⁻ᵖ.
Equations
- Proofs.gridModel p u hu = { rnd := Proofs.rndP p, u := u, err := ⋯ }
Instances For
binary32 (IEEE-754 single, fp32 accumulate): the p = 23 grid (24-bit
significand) at unit roundoff u32 = 2⁻²⁴ (the standard-model constant for this grid).
Instances For
fp8 E4M3 (the low-precision leaf): the p = 3 grid (3 mantissa bits) at
unit roundoff uE4M3 = 2⁻⁴, normal-range model.
Instances For
u32 ≤ uE4M3: fp32 is at least as precise as fp8 (2⁻²⁴ ≤ 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).
The fp8 budget at input width 4. The worst-case fp8 logit budget at the MNIST
input dimension (784) is ≤ 61, forcing a > 122 margin; that figure is
≈ 2·uE4M3 · (m·w·a), linear in the input dimension m. The same worst-case budget at
m = 4 is ≤ 1/2. (That the deployed 784-wide net drifts only a measured 0.38 is an
empirical observation, not proved here.)
The matching argmax corollary at the small input: a margin > 1 (vs > 122 at 784)
suffices for the fp8 forward to preserve the prediction.
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
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).