Proveddrift-lawdecodesnapshot-reuseexactness

Norm threshold for snapshot exactness: if ‖q_t − q_s‖·‖k‖ ≤ η then the key's score tilt |⟨q_t − q_s, k⟩| ≤ η

For all $\htmlData{mx=1}{d \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=5}{u, k : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{d}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{R}}}$ and $\htmlData{mx=1}{\eta \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=12}{\htmlData{mx=5}{\sqrt{\htmlData{mx=4}{\sum_{i} \htmlData{mx=3}{\htmlData{mx=2}{\htmlData{mx=0}{u}(\htmlData{mx=1}{i})}^{2}}}}} \cdot \htmlData{mx=11}{\sqrt{\htmlData{mx=10}{\sum_{i} \htmlData{mx=9}{\htmlData{mx=8}{\htmlData{mx=6}{k}(\htmlData{mx=7}{i})}^{2}}}}}} \mathrel{\htmlData{mx=14}{\leq}} \htmlData{mx=13}{\eta}$ , then

\htmlData{mx=8}{\left\lvert \htmlData{mx=7}{\sum_{i} \htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{u}(\htmlData{mx=1}{i})} \cdot \htmlData{mx=5}{\htmlData{mx=3}{k}(\htmlData{mx=4}{i})}}} \right\rvert} \mathrel{\htmlData{mx=10}{\leq}} \htmlData{mx=9}{\eta}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
Fin: Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fin)
f(x)Function application: Fin applied to d. Lean writes f x; papers write f(x). (Fin d)
⟹Implies: If Fin(d), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin d → ℝ)
x : TVariables: u, k range over Fin d → ℝ: the statement must hold for every choice. ((u k : Fin d → ℝ))
√Square root: The non-negative number whose square is ∑ i, u(i)^2. (Real.sqrt (∑ i, u i ^ 2))
·Multiplication: √(∑ i, u(i)^2) times √(∑ i, k(i)^2). (Real.sqrt (∑ i, u i ^ 2) * Real.sqrt (∑…)
≤At most: √(∑ i, u(i)^2) · √(∑ i, k(i)^2) is less than or equal to η. (Real.sqrt (∑ i, u i ^ 2) * Real.sqrt (∑…)
|x|Absolute value: The size of ∑ i, u(i) · k(i) without its sign. (|∑ i, u i * k i|)
RReal numbers: The real numbers: every point on the number line. (ℝ)
∑Summation: Add up u(i)^2 for every i. (∑ i, u i ^ 2)
aᵇPower: u(i) raised to the power 2. (u i ^ 2)

theorem rl-norm-threshold-tilt {d : ℕ} (u k : Fin d → ℝ) (η : ℝ) (h : Real.sqrt (∑ i, u i ^ 2) * Real.sqrt (∑ i, k i ^ 2) ≤ η) :
    |∑ i, u i * k i| ≤ η

Cauchy–Schwarz. A persistent snapshot is exact by rejection only for keys within the tilt budget; keys appended later with ‖k‖ > η/‖Δq‖ (kept in a norm-ordered heap) must be read exactly each token. Without this split a large-norm new key pushes an acceptance probability above 1 and silently biases the sampler. Part of 'The Drift Law' (persistent-snapshot exactness, loop 3d: keys appended later with large norm).

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

Norm threshold for snapshot exactness: if ‖q_t − q_s‖·‖k‖ ≤ η then the key's score tilt |⟨q_t − q_s, k⟩| ≤ η

How it was proved

More proved statements