Provedllmlarge-language-modelsformal-proofposition-encoding

A negative rate flips the sine and keeps the cosine

For all $\htmlData{mx=1}{r, p \in \htmlData{mx=0}{\mathbb{R}}}$ :

\htmlData{mx=4}{\htmlData{mx=0}{\operatorname{pe}}(\htmlData{mx=2}{-\htmlData{mx=1}{r}}, \htmlData{mx=3}{p})} \mathrel{\htmlData{mx=17}{=}} \htmlData{mx=16}{\left( \htmlData{mx=10}{-\htmlData{mx=9}{\htmlData{mx=8}{\htmlData{mx=5}{\operatorname{pe}}(\htmlData{mx=6}{r}, \htmlData{mx=7}{p})}_{1}}}, \htmlData{mx=15}{\htmlData{mx=14}{\htmlData{mx=11}{\operatorname{pe}}(\htmlData{mx=12}{r}, \htmlData{mx=13}{p})}_{2}} \right)}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: r, p range over real numbers: the statement must hold for every choice. ((r p : ℝ))
pe: LLMPE.pe: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (LLMPE.pe)
f(x)Function application: LLMPE.pe applied to −r, p. Lean writes f x; papers write f(x). (LLMPE.pe (-r) p)
=Equality: pe(−r, p) and (−pe(r, p).1, pe(r, p).2) are the same. (LLMPE.pe (-r) p = (-(LLMPE.pe r p).1, (…)
−xNegation: The negative of r. (-r)
(a, b)Tuple: The ordered pair (or tuple) of −pe(r, p).1, pe(r, p).2. ((-(LLMPE.pe r p).1, (LLMPE.pe r p).2))
p₁Component: Component 1 of pe(r, p) (the first). ((LLMPE.pe r p).1)

theorem pe-neg-rate (r p : ℝ) :
    LLMPE.pe (-r) p = (-(LLMPE.pe r p).1, (LLMPE.pe r p).2)

pe (−r) p = (−(pe r p).1, (pe r p).2).

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: 13 lines of Lean