Provedllmlarge-language-modelsformal-proofoptimization

The surrogate loss is at least its floor for nonnegative curvature

For all $\htmlData{mx=1}{a, m, c, x \in \htmlData{mx=0}{\mathbb{R}}}$ :

0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{a} \mathrel{\htmlData{mx=10}{\implies}} \htmlData{mx=2}{c} \mathrel{\htmlData{mx=9}{\leq}} \htmlData{mx=8}{\htmlData{mx=3}{\operatorname{qloss}}(\htmlData{mx=4}{a}, \htmlData{mx=5}{m}, \htmlData{mx=6}{c}, \htmlData{mx=7}{x})}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: a, m, c, x range over real numbers: the statement must hold for every choice. ((a m c x : ℝ))
≤At most: 0 is less than or equal to a. (0 ≤ a)
⟹Implies: If 0 ≤ a, then c ≤ qloss(a, m, c, x). (Between types, A → B is the type of functions from A to B.) (0 ≤ a → c ≤ LLMOptim.qloss a m c x)
qloss: LLMOptim.qloss: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (LLMOptim.qloss)
f(x)Function application: LLMOptim.qloss applied to a, m, c, x. Lean writes f x; papers write f(x). (LLMOptim.qloss a m c x)

theorem opt-qloss-nonneg-curve (a m c x : ℝ) :
    0 ≤ a → c ≤ LLMOptim.qloss a m c x

qloss a m c x ≥ c when a ≥ 0 (inequality form).

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