Baguette: attention-state slots in the gradient bank are disjoint, clear of the logit gradient, and read before written
For all , if and , then
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
- g, E, B, S, Lg range over natural numbers: the statement must hold for every choice. (
(g E B S Lg : ℕ)) - ≤At most
- S is less than or equal to 4 · B. (
S ≤ 4 * B) - ∀For all
- The statement after the comma holds for every L, M. (
∀ L M : ℕ, 39 ≤ L → L < M → (g + 4 * (E…) - ·Multiplication
- 4 times B. (
4 * B) - <Less than
- L is strictly smaller than M. (
L < M) - ⟹Implies
- If L < M, then g + 4 · (E + (L − 1) · B) + S ≤ g + 4 · (E + (M − 1) · B) …. (Between types, A → B is the type of functions from A to B.) (
L < M → (g + 4 * (E + (L - 1) * B) + S …) - +Addition
- E plus (L − 1) · B. (
E + (L - 1) * B) - -Subtraction
- L minus 1. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
L - 1) - ∧And
- Both hold: g + 4 · E + Lg ≤ g + 4 · (E + (L − 1) · B), and 79 − L < 79 − (L − 1) ∨ 79 < L. (
(g + 4 * E + Lg ≤ g + 4 * (E + (L - 1) …) - ∨Or
- At least one holds: 79 − L < 79 − (L − 1), or 79 < L. (
79 - L < 79 - (L - 1) ∨ 79 < L)
theorem baguette-attention-state-slots-are-safe (g E B S Lg : ℕ) (hS : S ≤ 4 * B) (hLg : Lg ≤ 4 * (38 * B)) :
∀ L M : ℕ, 39 ≤ L → L < M → (g + 4 * (E + (L - 1) * B) + S ≤ g + 4 * (E + (M - 1) * B)) ∧ (g + 4 * E + Lg ≤ g + 4 * (E + (L - 1) * B)) ∧ (79 - L < 79 - (L - 1) ∨ 79 < L)Baguette (Alpha, RTX 3070, recomputed realization) keeps block L's attention state (Q, K, V, attention output, log-sums; S = 12,730,368 bytes) from its forward to its backward in the binary32 gradient slice of block L-1, for L in 39..78. The slot sits at g + 4*(E + (L-1)B), where g is the gradient bank base, E the embedding parameter count and B one block's parameter count (4B = 14,160,384 bytes). The bfloat16 logit gradient (Lg bytes) aliases slices 0..37, starting at g + 4E. This statement shows three things. (1) For 39 <= L < M, slot L ends at or before slot M begins, given S <= 4B. (2) Every slot starts at or after the end of the logit-gradient alias, given Lg <= 438*B. (3) In the descending backward (block 79 first, position 79 - L), block L reads its slot before block L-1, the slot slice's only writer, runs. Exact, schedule-only change: no numerical effect; it removes 120 launches (projection, attention and input-norm replays) from every update.
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
- 16 lines of Lean