Provedalphabaguettenoether-checksumtransport
The pairing checksum can be read after RoPE: ⟨Rᵀdq, q⟩ = ⟨dq, Rq⟩ for each rotary pair
For all :
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- c, s, u₁, u₂, w₁, w₂ range over real numbers: the statement must hold for every choice. (
(c s u₁ u₂ w₁ w₂ : ℝ)) - =Equality
- (c · w₁ + s · w₂) · u₁ + (−s · w₁ + c · w₂) · u₂ and w₁ · (c · u₁ − s · u₂) + w₂ · (s · u₁ + c · u₂) are the same. (
(c * w₁ + s * w₂) * u₁ + (-s * w₁ + c *…) - ·Multiplication
- c times w₁. (
c * w₁) - +Addition
- c · w₁ plus s · w₂. (
c * w₁ + s * w₂) - −xNegation
- The negative of s. (
-s) - -Subtraction
- c · u₁ minus s · u₂. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
c * u₁ - s * u₂)
theorem nc-rope-preserves-pairing (c s u₁ u₂ w₁ w₂ : ℝ) :
(c * w₁ + s * w₂) * u₁ + (-s * w₁ + c * w₂) * u₂ = w₁ * (c * u₁ - s * u₂) + w₂ * (s * u₁ + c * u₂)RoPE's backward applies the transpose rotation, so the pre-rotation pairing ⟨dq_pre, q_pre⟩ equals the post-rotation pairing ⟨dq_post, q_post⟩ (adjointness; holds for any 2×2 map). C3 can therefore be accumulated in whichever kernel already holds the rotated or unrotated tensors. 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
- 12 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.