proofs
Provedtwo-precision-attentionenergyquantizationlaw

Base-2 integer exponents: rounding scores to the grid (log 2)ℤ adds at most (log 2)/2 to the tilt

For all s,shat,m,η∈R\htmlData{mx=1}{s, \mathit{shat}, m, \eta \in \htmlData{mx=0}{\mathbb{R}}}, if ∣s−shat∣≤η\htmlData{mx=3}{\left\lvert \htmlData{mx=2}{\htmlData{mx=0}{s} - \htmlData{mx=1}{\mathit{shat}}} \right\rvert} \mathrel{\htmlData{mx=5}{\leq}} \htmlData{mx=4}{\eta} and ∣shat−m⋅log⁡2∣≤log⁡22\htmlData{mx=5}{\left\lvert \htmlData{mx=4}{\htmlData{mx=0}{\mathit{shat}} - \htmlData{mx=3}{\htmlData{mx=1}{m} \cdot \htmlData{mx=2}{\log 2}}} \right\rvert} \mathrel{\htmlData{mx=8}{\leq}} \htmlData{mx=7}{\frac{\htmlData{mx=6}{\log 2}}{2}}, then

∣s−m⋅log⁡2∣≤η+log⁡22\htmlData{mx=5}{\left\lvert \htmlData{mx=4}{\htmlData{mx=0}{s} - \htmlData{mx=3}{\htmlData{mx=1}{m} \cdot \htmlData{mx=2}{\log 2}}} \right\rvert} \mathrel{\htmlData{mx=10}{\leq}} \htmlData{mx=9}{\htmlData{mx=6}{\eta} + \htmlData{mx=8}{\frac{\htmlData{mx=7}{\log 2}}{2}}}
What the notation means · or point at any symbol
RReal numbers
The real numbers: every point on the number line. (ℝ)
x ∈ TVariables
s, shat, m, η range over real numbers: the statement must hold for every choice. ((s shat m η : ℝ))
|x|Absolute value
The size of s − shat without its sign. (|s - shat|)
≤At most
|s − shat| is less than or equal to η. (|s - shat| ≤ η)
-Subtraction
s minus shat. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (s - shat)
·Multiplication
m times log(2). (m * Real.log 2)
logNatural logarithm
The logarithm of 2 to base e: the power e must be raised to to give 2. (Real.log 2)
+Addition
η plus log(2)/2. (η + Real.log 2 / 2)
a/bDivision
log(2) divided by 2. In Lean, dividing by 0 gives 0. (Real.log 2 / 2)

Proposal weights become 2^m — bit shifts instead of exponentials — while accepted keys remain exact samples of the full-precision softmax. Part of 'Two-Precision Exact Attention: low-precision scores as a proposal, full-precision softmax as the exact target'.

How it was proved

Proved
4 October 2026
By
Ajax, with the agent “Baguette math & proofs (Claude Code, 2026-10-03)”
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
12 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements