Provedalphabaguettenoether-checksumattention
Translation symmetry of softmax: every row of the attention score gradient sums to zero
For all and , if , then
What the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - Fin
- Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Fin) - f(x)Function application
- Fin applied to T. Lean writes f x; papers write f(x). (
Fin T) - ⟹Implies
- If Fin(T), then ℝ. (Between types, A → B is the type of functions from A to B.) (
Fin T → ℝ) - x : TVariables
- P, dP range over Fin T → ℝ: the statement must hold for every choice. (
(P dP : Fin T → ℝ)) - ∑Summation
- Add up P(j) for every j. (
∑ j, P j) - =Equality
- ∑ j, P(j) and 1 are the same. (
∑ j, P j = 1) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - -Subtraction
- dP(j) minus ∑ k, P(k) · dP(k). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
dP j - ∑ k, P k * dP k) - ·Multiplication
- P(k) times dP(k). (
P k * dP k)
theorem nc-score-gradient-row-sums-to-zero {T : ℕ} (P dP : Fin T → ℝ) (hP : ∑ j, P j = 1) :
∑ j, P j * (dP j - ∑ k, P k * dP k) = 0For a probability row P (Σⱼ Pⱼ = 1, causal masking = zeros) and any upstream dP, the score gradient Rⱼ = Pⱼ·(dPⱼ − Σₖ Pₖ dPₖ) has Σⱼ Rⱼ = 0. Softmax is invariant to adding a constant to a row of scores, so its gradient is orthogonal to the all-ones direction (the constraint Kunin et al. derive from symmetry). This is the root of checksums C1 and C3. Part of 'Noether checksums for Baguette's backward kernels'.
How it was proved
- Proved
- 3 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
- 15 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.