Provedbaguettealphabfloat16lossless

An FP32 word is recovered exactly from its round-to-nearest-even BF16 word, its low 16 bits, and one tie flag

For all $\htmlData{mx=1}{u, H, L, b \in \htmlData{mx=0}{\mathbb{N}}}$ , if $\htmlData{mx=0}{u} \mathrel{\htmlData{mx=2}{<}} \htmlData{mx=1}{2^{32}}$ , $\htmlData{mx=0}{H} \mathrel{\htmlData{mx=4}{=}} \htmlData{mx=3}{\frac{\htmlData{mx=1}{u}}{\htmlData{mx=2}{2^{16}}}}$ , $\htmlData{mx=0}{L} \mathrel{\htmlData{mx=4}{=}} \htmlData{mx=3}{\htmlData{mx=1}{u} \bmod \htmlData{mx=2}{2^{16}}}$ and $\htmlData{mx=0}{b} \mathrel{\htmlData{mx=19}{=}} \htmlData{mx=18}{\begin{cases} \htmlData{mx=1}{H} & \text{if } \htmlData{mx=2}{L} \mathrel{\htmlData{mx=4}{<}} \htmlData{mx=3}{2^{15}} \\ \htmlData{mx=17}{\begin{cases} \htmlData{mx=6}{\htmlData{mx=5}{H} + 1} & \text{if } \htmlData{mx=7}{2^{15}} \mathrel{\htmlData{mx=9}{<}} \htmlData{mx=8}{L} \\ \htmlData{mx=16}{\begin{cases} \htmlData{mx=10}{H} & \text{if } \htmlData{mx=12}{\htmlData{mx=11}{H} \bmod 2} \mathrel{\htmlData{mx=13}{=}} 0 \\ \htmlData{mx=15}{\htmlData{mx=14}{H} + 1} & \text{otherwise} \end{cases}} & \text{otherwise} \end{cases}} & \text{otherwise} \end{cases}}$ , then

\begin{aligned} & (\htmlData{mx=1}{b} \mathrel{\htmlData{mx=3}{=}} \htmlData{mx=2}{H} \mathbin{\htmlData{mx=8}{\lor}} \htmlData{mx=4}{b} \mathrel{\htmlData{mx=7}{=}} \htmlData{mx=6}{\htmlData{mx=5}{H} + 1}) \\ & \htmlData{mx=0}{\land} \left(\htmlData{mx=9}{L} \mathrel{\htmlData{mx=11}{\neq}} \htmlData{mx=10}{2^{15}} \mathrel{\htmlData{mx=24}{\implies}} \htmlData{mx=12}{u} \mathrel{\htmlData{mx=23}{=}} \htmlData{mx=22}{\htmlData{mx=20}{\left(\htmlData{mx=18}{\htmlData{mx=13}{b} - \left(\htmlData{mx=17}{\begin{cases} 1 & \text{if } \htmlData{mx=14}{2^{15}} \mathrel{\htmlData{mx=16}{<}} \htmlData{mx=15}{L} \\ 0 & \text{otherwise} \end{cases}}\right)}\right) \cdot \htmlData{mx=19}{2^{16}}} + \htmlData{mx=21}{L}}\right) \\ & \htmlData{mx=0}{\land} (\htmlData{mx=25}{L} \mathrel{\htmlData{mx=27}{=}} \htmlData{mx=26}{2^{15}} \mathrel{\htmlData{mx=44}{\implies}} \htmlData{mx=30}{\htmlData{mx=28}{b} - \htmlData{mx=29}{H}} \mathrel{\htmlData{mx=31}{\leq}} 1 \mathbin{\htmlData{mx=43}{\land}} \htmlData{mx=32}{u} \mathrel{\htmlData{mx=42}{=}} \htmlData{mx=41}{\htmlData{mx=39}{(\htmlData{mx=37}{\htmlData{mx=33}{b} - (\htmlData{mx=36}{\htmlData{mx=34}{b} - \htmlData{mx=35}{H}})}) \cdot \htmlData{mx=38}{2^{16}}} + \htmlData{mx=40}{L}}) \\ & \htmlData{mx=0}{\land} (\htmlData{mx=47}{\htmlData{mx=45}{b} \cdot \htmlData{mx=46}{2^{16}}} \mathrel{\htmlData{mx=51}{\leq}} \htmlData{mx=50}{\htmlData{mx=48}{u} + \htmlData{mx=49}{2^{15}}} \mathbin{\htmlData{mx=59}{\land}} \htmlData{mx=52}{u} \mathrel{\htmlData{mx=58}{\leq}} \htmlData{mx=57}{\htmlData{mx=55}{\htmlData{mx=53}{b} \cdot \htmlData{mx=54}{2^{16}}} + \htmlData{mx=56}{2^{15}}}) \end{aligned}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
x ∈ TVariables: u, H, L, b range over natural numbers: the statement must hold for every choice. ((u H L b : ℕ))
<Less than: u is strictly smaller than 2^32. (u < 2 ^ 32)
=Equality: H and u/2^16 are the same. (H = u / 2 ^ 16)
∨Or: At least one holds: b = H, or b = H + 1. (b = H ∨ b = H + 1)
aᵇPower: 2 raised to the power 32. (2 ^ 32)
a/bDivision: u divided by 2^16. In Lean, dividing by 0 gives 0. (u / 2 ^ 16)
modRemainder: The remainder when u is divided by 2^16. (u % 2 ^ 16)
≠Not equal: L and 2^15 are different. (L ≠ 2 ^ 15)
⟹Implies: If L ≠ 2^15, then u = (b − 1 if 2^15 < L, else 0) · 2^16 + L. (Between types, A → B is the type of functions from A to B.) (L ≠ 2 ^ 15 → u = (b - (if 2 ^ 15 < L th…)
·Multiplication: b − 1 if 2^15 < L, else 0 times 2^16. ((b - (if 2 ^ 15 < L then 1 else 0)) * 2…)
-Subtraction: b minus 1 if 2^15 < L, else 0. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (b - (if 2 ^ 15 < L then 1 else 0))
+Addition: H plus 1. (H + 1)
{ a if c; b otherwiseCases (if … then … else): H when H % 2 = 0, and H + 1 otherwise. (if H % 2 = 0 then H else H + 1)
≤At most: b − H is less than or equal to 1. (b - H ≤ 1)
∧And: Both hold: b − H ≤ 1, and u = (b − (b − H)) · 2^16 + L. (b - H ≤ 1 ∧ u = (b - (b - H)) * 2 ^ 16 …)

theorem fp32-from-bf16-plus-low-half-and-tie-flag (u H L b : ℕ) (hu : u < 2 ^ 32) (hH : H = u / 2 ^ 16) (hL : L = u % 2 ^ 16) (hb : b = if L < 2 ^ 15 then H else if 2 ^ 15 < L then H + 1 else if H % 2 = 0 then H else H + 1) :
    (b = H ∨ b = H + 1) ∧ (L ≠ 2 ^ 15 → u = (b - (if 2 ^ 15 < L then 1 else 0)) * 2 ^ 16 + L) ∧ (L = 2 ^ 15 → b - H ≤ 1 ∧ u = (b - (b - H)) * 2 ^ 16 + L) ∧ (b * 2 ^ 16 ≤ u + 2 ^ 15 ∧ u ≤ b * 2 ^ 16 + 2 ^ 15)

For the 33-bit master-weight codec proposed for Baguette, which keeps the BF16 operand bank and drops the FP32 master. Let u < 2^32 be a raw FP32 bit pattern. H = u / 2^16 and L = u mod 2^16 are its high and low halves. b is the round-to-nearest-even of u to its upper 16 bits: H if L < 2^15; H + 1 if L > 2^15; at the tie L = 2^15, H if H is even and H + 1 if it is odd. For finite FP32 values this is exactly the BF16 conversion: BF16 is FP32's upper half, and rounding the magnitude bits carries into the exponent. The statement has four parts. (1) b is H or H + 1. (2) Off the tie, u = (b - c) * 2^16 + L, where c = 1 when L > 2^15 and 0 otherwise, so b and L alone recover u. (3) At the tie L = 2^15, u = (b - f) * 2^16 + L with one flag f = b - H <= 1. (4) The integer residual u - b * 2^16 lies in [-2^15, 2^15]: 65,537 values, one more than 16 bits hold.

How it was proved

Proved: 5 October 2026
By: Ajax
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: Classical.choice, Quot.sound, propext
Proof: 31 lines of Lean

An FP32 word is recovered exactly from its round-to-nearest-even BF16 word, its low 16 bits, and one tie flag

How it was proved

More proved statements