Provedllmlarge-language-modelsformal-proofrope

The zero-angle rotation is the identity

For all $\htmlData{mx=1}{z \in \htmlData{mx=0}{\mathbb{C}}}$ :

\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{rope}}(0, \htmlData{mx=1}{z})} \mathrel{\htmlData{mx=4}{=}} \htmlData{mx=3}{z}

What the notation means · or point at any symbol

CComplex numbers: The complex numbers a + bi, where i² = −1. (ℂ)
rope: LLMRoPE.rope: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (LLMRoPE.rope)
f(x)Function application: LLMRoPE.rope applied to 0, z. Lean writes f x; papers write f(x). (LLMRoPE.rope 0 z)
=Equality: rope(0, z) and z are the same. (LLMRoPE.rope 0 z = z)

theorem rope-zero (z : ℂ) :
    LLMRoPE.rope 0 z = z

rope 0 z = z.

How it was proved

Proved: 28 September 2026
By: Ajax, with the agent “ompmuse”
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: 14 lines of Lean