Proveddrift-lawdecodesnapshot-reuseattention-compute-law

Chord bound for exp: e^x ≤ 1 + (e − 1)x on [0, 1]

For all $\htmlData{mx=1}{x \in \htmlData{mx=0}{\mathbb{R}}}$ , if $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{x}$ and $\htmlData{mx=0}{x} \mathrel{\htmlData{mx=1}{\leq}} 1$ , then

\htmlData{mx=1}{e^{\htmlData{mx=0}{x}}} \mathrel{\htmlData{mx=7}{\leq}} \htmlData{mx=6}{1 + \htmlData{mx=5}{(\htmlData{mx=3}{\htmlData{mx=2}{e^{1}} - 1}) \cdot \htmlData{mx=4}{x}}}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: 0 is less than or equal to x. (0 ≤ x)
eˣExponential function: e raised to the power x, where e ≈ 2.718. (Real.exp x)
+Addition: 1 plus (exp(1) − 1) · x. (1 + (Real.exp 1 - 1) * x)
·Multiplication: exp(1) − 1 times x. ((Real.exp 1 - 1) * x)
-Subtraction: exp(1) minus 1. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (Real.exp 1 - 1)

theorem rl-exp-chord (x : ℝ) (h0 : 0 ≤ x) (h1 : x ≤ 1) :
    Real.exp x ≤ 1 + (Real.exp 1 - 1) * x

Convexity of exp between 0 and 1; converts the snapshot rejection cost e^{2η} into a linear bound in the drift. Part of 'The Drift Law: decode K/V traffic is set by how far the query drifts' (exact snapshot reuse at decode).

How it was proved

Proved: 5 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: 14 lines of Lean

Chord bound for exp: e^x ≤ 1 + (e − 1)x on [0, 1]

How it was proved

More proved statements