Provedalphabaguettebaguette-zrange

One quantized residual step drifts by at most (1+λ)|x' − x| + δ

For all $\htmlData{mx=3}{f : \htmlData{mx=0}{\mathbb{R}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ and $\htmlData{mx=1}{\mathit{lam}, \delta, x, x', q \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=15}{\forall a, b,\ \htmlData{mx=7}{\left\lvert \htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{f}(\htmlData{mx=1}{a})} - \htmlData{mx=5}{\htmlData{mx=3}{f}(\htmlData{mx=4}{b})}} \right\rvert} \mathrel{\htmlData{mx=14}{\leq}} \htmlData{mx=13}{\htmlData{mx=8}{\mathit{lam}} \cdot \htmlData{mx=12}{\left\lvert \htmlData{mx=11}{\htmlData{mx=9}{a} - \htmlData{mx=10}{b}} \right\rvert}}}$ and $\htmlData{mx=5}{\left\lvert \htmlData{mx=4}{\htmlData{mx=0}{q} - \htmlData{mx=3}{\htmlData{mx=1}{f}(\htmlData{mx=2}{x'})}} \right\rvert} \mathrel{\htmlData{mx=7}{\leq}} \htmlData{mx=6}{\delta}$ , then

\htmlData{mx=9}{\left\lvert \htmlData{mx=8}{\htmlData{mx=2}{\htmlData{mx=0}{x'} + \htmlData{mx=1}{q}} - (\htmlData{mx=7}{\htmlData{mx=3}{x} + \htmlData{mx=6}{\htmlData{mx=4}{f}(\htmlData{mx=5}{x})}})} \right\rvert} \mathrel{\htmlData{mx=19}{\leq}} \htmlData{mx=18}{\htmlData{mx=16}{(\htmlData{mx=11}{1 + \htmlData{mx=10}{\mathit{lam}}}) \cdot \htmlData{mx=15}{\left\lvert \htmlData{mx=14}{\htmlData{mx=12}{x'} - \htmlData{mx=13}{x}} \right\rvert}} + \htmlData{mx=17}{\delta}}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
⟹Implies: If ℝ, then ℝ. (Between types, A → B is the type of functions from A to B.) (ℝ → ℝ)
x ∈ TVariables: lam, δ, x, x', q range over real numbers: the statement must hold for every choice. ((lam δ x x' q : ℝ))
∀For all: The statement after the comma holds for every a, b. (∀ a b, |f a - f b| ≤ lam * |a - b|)
+Addition: x' plus q. (x' + q)
|x|Absolute value: The size of f(a) − f(b) without its sign. (|f a - f b|)
≤At most: |f(a) − f(b)| is less than or equal to lam · |a − b|. (|f a - f b| ≤ lam * |a - b|)
f(x)Function application: f applied to a. Lean writes f x; papers write f(x). (f a)
-Subtraction: f(a) minus f(b). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (f a - f b)
·Multiplication: lam times |a − b|. (lam * |a - b|)

theorem bz-lipschitz-one-step (f : ℝ → ℝ) (lam δ x x' q : ℝ) (hf : ∀ a b, |f a - f b| ≤ lam * |a - b|) (hq : |q - f x'| ≤ δ) :
    |(x' + q) - (x + f x)| ≤ (1 + lam) * |x' - x| + δ

If f is λ-Lipschitz and the computed increment q is within δ of f(x'), the quantized step x' + q differs from the exact step x + f(x) by at most (1+λ)|x' − x| + δ. This is the per-layer input to the Grönwall bound. Part of the plan 'Baguette-Z: closed-loop certified integer-state training'.

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

One quantized residual step drifts by at most (1+λ)|x' − x| + δ

How it was proved

More proved statements