proofs
Provedalphabaguetteropeattention

RoPE pair rotation: the q·k score depends only on the position difference, and norms are preserved

For all θ,a,b,u1,u2,v1,v2∈R\htmlData{mx=1}{\theta, a, b, u_{1}, u_{2}, v_{1}, v_{2} \in \htmlData{mx=0}{\mathbb{R}}}:

(u1⋅cos⁡(a⋅θ)−u2⋅sin⁡(a⋅θ))⋅(v1⋅cos⁡(b⋅θ)−v2⋅sin⁡(b⋅θ))+(u1⋅sin⁡(a⋅θ)+u2⋅cos⁡(a⋅θ))⋅(v1⋅sin⁡(b⋅θ)+v2⋅cos⁡(b⋅θ))=u1⋅(v1⋅cos⁡((b−a)⋅θ)−v2⋅sin⁡((b−a)⋅θ))+u2⋅(v1⋅sin⁡((b−a)⋅θ)+v2⋅cos⁡((b−a)⋅θ))∧(u1⋅cos⁡(a⋅θ)−u2⋅sin⁡(a⋅θ))2+(u1⋅sin⁡(a⋅θ)+u2⋅cos⁡(a⋅θ))2=u12+u22\begin{aligned} & \htmlData{mx=56}{\htmlData{mx=28}{(\htmlData{mx=14}{\htmlData{mx=7}{\htmlData{mx=2}{u_{1}} \cdot \htmlData{mx=6}{\cos (\htmlData{mx=5}{\htmlData{mx=3}{a} \cdot \htmlData{mx=4}{\theta}})}} - \htmlData{mx=13}{\htmlData{mx=8}{u_{2}} \cdot \htmlData{mx=12}{\sin (\htmlData{mx=11}{\htmlData{mx=9}{a} \cdot \htmlData{mx=10}{\theta}})}}}) \cdot (\htmlData{mx=27}{\htmlData{mx=20}{\htmlData{mx=15}{v_{1}} \cdot \htmlData{mx=19}{\cos (\htmlData{mx=18}{\htmlData{mx=16}{b} \cdot \htmlData{mx=17}{\theta}})}} - \htmlData{mx=26}{\htmlData{mx=21}{v_{2}} \cdot \htmlData{mx=25}{\sin (\htmlData{mx=24}{\htmlData{mx=22}{b} \cdot \htmlData{mx=23}{\theta}})}}})} + \htmlData{mx=55}{(\htmlData{mx=41}{\htmlData{mx=34}{\htmlData{mx=29}{u_{1}} \cdot \htmlData{mx=33}{\sin (\htmlData{mx=32}{\htmlData{mx=30}{a} \cdot \htmlData{mx=31}{\theta}})}} + \htmlData{mx=40}{\htmlData{mx=35}{u_{2}} \cdot \htmlData{mx=39}{\cos (\htmlData{mx=38}{\htmlData{mx=36}{a} \cdot \htmlData{mx=37}{\theta}})}}}) \cdot (\htmlData{mx=54}{\htmlData{mx=47}{\htmlData{mx=42}{v_{1}} \cdot \htmlData{mx=46}{\sin (\htmlData{mx=45}{\htmlData{mx=43}{b} \cdot \htmlData{mx=44}{\theta}})}} + \htmlData{mx=53}{\htmlData{mx=48}{v_{2}} \cdot \htmlData{mx=52}{\cos (\htmlData{mx=51}{\htmlData{mx=49}{b} \cdot \htmlData{mx=50}{\theta}})}}})}} \\ & \quad \htmlData{mx=1}{=} \htmlData{mx=95}{\htmlData{mx=75}{\htmlData{mx=57}{u_{1}} \cdot (\htmlData{mx=74}{\htmlData{mx=65}{\htmlData{mx=58}{v_{1}} \cdot \htmlData{mx=64}{\cos (\htmlData{mx=63}{(\htmlData{mx=61}{\htmlData{mx=59}{b} - \htmlData{mx=60}{a}}) \cdot \htmlData{mx=62}{\theta}})}} - \htmlData{mx=73}{\htmlData{mx=66}{v_{2}} \cdot \htmlData{mx=72}{\sin (\htmlData{mx=71}{(\htmlData{mx=69}{\htmlData{mx=67}{b} - \htmlData{mx=68}{a}}) \cdot \htmlData{mx=70}{\theta}})}}})} + \htmlData{mx=94}{\htmlData{mx=76}{u_{2}} \cdot (\htmlData{mx=93}{\htmlData{mx=84}{\htmlData{mx=77}{v_{1}} \cdot \htmlData{mx=83}{\sin (\htmlData{mx=82}{(\htmlData{mx=80}{\htmlData{mx=78}{b} - \htmlData{mx=79}{a}}) \cdot \htmlData{mx=81}{\theta}})}} + \htmlData{mx=92}{\htmlData{mx=85}{v_{2}} \cdot \htmlData{mx=91}{\cos (\htmlData{mx=90}{(\htmlData{mx=88}{\htmlData{mx=86}{b} - \htmlData{mx=87}{a}}) \cdot \htmlData{mx=89}{\theta}})}}})}} \\ & \htmlData{mx=0}{\land} \htmlData{mx=125}{\htmlData{mx=110}{(\htmlData{mx=109}{\htmlData{mx=102}{\htmlData{mx=97}{u_{1}} \cdot \htmlData{mx=101}{\cos (\htmlData{mx=100}{\htmlData{mx=98}{a} \cdot \htmlData{mx=99}{\theta}})}} - \htmlData{mx=108}{\htmlData{mx=103}{u_{2}} \cdot \htmlData{mx=107}{\sin (\htmlData{mx=106}{\htmlData{mx=104}{a} \cdot \htmlData{mx=105}{\theta}})}}})^{2}} + \htmlData{mx=124}{(\htmlData{mx=123}{\htmlData{mx=116}{\htmlData{mx=111}{u_{1}} \cdot \htmlData{mx=115}{\sin (\htmlData{mx=114}{\htmlData{mx=112}{a} \cdot \htmlData{mx=113}{\theta}})}} + \htmlData{mx=122}{\htmlData{mx=117}{u_{2}} \cdot \htmlData{mx=121}{\cos (\htmlData{mx=120}{\htmlData{mx=118}{a} \cdot \htmlData{mx=119}{\theta}})}}})^{2}}} \\ & \quad \htmlData{mx=96}{=} \htmlData{mx=130}{\htmlData{mx=127}{\htmlData{mx=126}{u_{1}}^{2}} + \htmlData{mx=129}{\htmlData{mx=128}{u_{2}}^{2}}} \end{aligned}
What the notation means · or point at any symbol
RReal numbers
The real numbers: every point on the number line. (ℝ)
x ∈ TVariables
θ, a, b, u₁, u₂, v₁, v₂ range over real numbers: the statement must hold for every choice. ((θ a b u₁ u₂ v₁ v₂ : ℝ))
=Equality
(u₁ · cos(a · θ) − u₂ · sin(a · θ)) · (v₁ · cos(b · θ) − v… and u₁ · (v₁ · cos((b − a) · θ) − v₂ · sin((b − a) · θ)) + u₂ … are the same. ((u₁ * Real.cos (a * θ) - u₂ * Real.sin …)
∧And
Both hold: (u₁ · cos(a · θ) − u₂ · sin(a · θ)) · (v₁ · cos(b · θ) − v…, and (u₁ · cos(a · θ) − u₂ · sin(a · θ))^2 + (u₁ · sin(a · θ) +…. ((u₁ * Real.cos (a * θ) - u₂ * Real.sin …)
-Subtraction
u₁ · cos(a · θ) minus u₂ · sin(a · θ). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (u₁ * Real.cos (a * θ) - u₂ * Real.sin (…)
cosCosine
The cosine of a · θ (radians). (Real.cos (a * θ))
·Multiplication
a times θ. (a * θ)
sinSine
The sine of a · θ (radians). (Real.sin (a * θ))
+Addition
u₁ · sin(a · θ) plus u₂ · cos(a · θ). (u₁ * Real.sin (a * θ) + u₂ * Real.cos (…)
aᵇPower
u₁ · cos(a · θ) − u₂ · sin(a · θ) raised to the power 2. ((u₁ * Real.cos (a * θ) - u₂ * Real.sin …)

Baguette rotates each of its 32 feature pairs per head by angle position·θ_j, with θ_j = 10000^(−2j/64) (groupedDecoderRotaryBase, rotary tables in Build/Graph.alpha). For one pair, a query rotated by position a and a key rotated by position b have the same dot product as the unrotated query against the key rotated by b − a. Rotation also preserves the pair's squared norm. Summed over pairs, attention scores are translation-invariant in position. In the same-position case, inner products such as ⟨dQ, Q⟩ are rotation-invariant, which the deferred-normalization idea uses.

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.

More proved statements