proofs
Proveddrift-lawcounterexamplereview-response

Counterexample: for rows (0.9,0.1) and (0.1,0.9) with equal prior the normalised optimum is 41/25 = 1.64, but the unnormalised optimiser at scale L = 1000 has normalised cost ≥ 4

(4110012+4110012=4125)∧41100⋅(1000081+810000011000081)+41100⋅(1000081+8100000181000001)≥4\begin{aligned} & \left(\htmlData{mx=8}{\htmlData{mx=4}{\frac{\htmlData{mx=2}{\htmlData{mx=1}{\frac{41}{100}}}}{\htmlData{mx=3}{\frac{1}{2}}}} + \htmlData{mx=7}{\frac{\htmlData{mx=5}{\frac{41}{100}}}{\htmlData{mx=6}{\frac{1}{2}}}}} \mathrel{\htmlData{mx=10}{=}} \htmlData{mx=9}{\frac{41}{25}}\right) \\ & \htmlData{mx=0}{\land} \htmlData{mx=27}{\htmlData{mx=19}{\htmlData{mx=13}{\htmlData{mx=12}{\frac{41}{100}}} \cdot \left(\htmlData{mx=18}{\frac{\htmlData{mx=16}{\htmlData{mx=14}{\sqrt{1000081}} + \htmlData{mx=15}{\sqrt{81000001}}}}{\htmlData{mx=17}{\sqrt{1000081}}}}\right)} + \htmlData{mx=26}{\htmlData{mx=20}{\frac{41}{100}} \cdot \left(\htmlData{mx=25}{\frac{\htmlData{mx=23}{\htmlData{mx=21}{\sqrt{1000081}} + \htmlData{mx=22}{\sqrt{81000001}}}}{\htmlData{mx=24}{\sqrt{81000001}}}}\right)}} \\ & \quad \htmlData{mx=11}{\geq} 4 \end{aligned}
What the notation means · or point at any symbol
∧And
Both hold: 41/100/(1/2) + 41/100/(1/2) = 41/25, and 41/100 · ((√(1000081) + √(81000001))/√(1000081)) + 41/100 …. (((41 / 100 : ℝ) / (1 / 2) + (41 / 100) …)
(x : T)As real numbers
41/100 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((41 / 100 : ℝ))
+Addition
41/100/(1/2) plus 41/100/(1/2). ((41 / 100 : ℝ) / (1 / 2) + (41 / 100) /…)
=Equality
41/100/(1/2) + 41/100/(1/2) and 41/25 are the same. ((41 / 100 : ℝ) / (1 / 2) + (41 / 100) /…)
a/bDivision
41 divided by 100. In Lean, dividing by 0 gives 0. (41 / 100)
·Multiplication
41/100 times (√(1000081) + √(81000001))/√(1000081). ((41 / 100 : ℝ) * ((Real.sqrt 1000081 + …)
≥At least
41/100 · ((√(1000081) + √(81000001))/√(1000081)) + 41/100 … is greater than or equal to 4. ((41 / 100 : ℝ) * ((Real.sqrt 1000081 + …)
√Square root
The non-negative number whose square is 1000081. (Real.sqrt 1000081)

Machine-checked instance of the external reviewer's shift-invariance test (2026-10-05). Representing the two rows by unnormalised weights (9,1) and L·(1,9) leaves both softmax rows unchanged, yet the optimiser of the unnormalised second moment, r ∝ (√((81+L²)/2), √((1+81L²)/2)), tends to (0.1, 0.9) and its normalised cost 0.41(2 + y/x + x/y) with x = √1000081, y = √81000001 exceeds 4. An optimiser for normalised attention cannot change when the attention rows do not.

How it was proved

Proved
5 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
34 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements