Proveddrift-lawdecodesnapshot-reuseattention-compute-law

Tilt normaliser identity: E_{π_s}[e^{t_j − s_j}] = Z_t / Z_s

For all $\htmlData{mx=1}{J \in \htmlData{mx=0}{\operatorname{Type}}}$ and $\htmlData{mx=3}{s, t : \htmlData{mx=0}{J} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{J}}$ and $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Nonempty}}\,\htmlData{mx=1}{J}}$ ):

\begin{aligned} & \htmlData{mx=20}{\sum_{j} \htmlData{mx=19}{\htmlData{mx=10}{\frac{\htmlData{mx=4}{e^{\htmlData{mx=3}{\htmlData{mx=1}{s}(\htmlData{mx=2}{j})}}}}{\htmlData{mx=9}{\sum_{k} \htmlData{mx=8}{e^{\htmlData{mx=7}{\htmlData{mx=5}{s}(\htmlData{mx=6}{k})}}}}}} \cdot \htmlData{mx=18}{e^{\htmlData{mx=17}{\htmlData{mx=13}{\htmlData{mx=11}{t}(\htmlData{mx=12}{j})} - \htmlData{mx=16}{\htmlData{mx=14}{s}(\htmlData{mx=15}{j})}}}}}} \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=31}{\frac{\htmlData{mx=25}{\sum_{k} \htmlData{mx=24}{e^{\htmlData{mx=23}{\htmlData{mx=21}{t}(\htmlData{mx=22}{k})}}}}}{\htmlData{mx=30}{\sum_{k} \htmlData{mx=29}{e^{\htmlData{mx=28}{\htmlData{mx=26}{s}(\htmlData{mx=27}{k})}}}}}} \end{aligned}

What the notation means · or point at any symbol

Type: Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
Fintype: Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fintype)
f(x)Function application: Fintype applied to J. Lean writes f x; papers write f(x). (Fintype J)
Nonempty: Nonempty: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Nonempty)
⟹Implies: If J, then ℝ. (Between types, A → B is the type of functions from A to B.) (J → ℝ)
x : TVariables: s, t range over J → ℝ: the statement must hold for every choice. ((s t : J → ℝ))
=Equality: ∑ j, exp(s(j))/(∑ k, exp(s(k))) · exp(t(j) − s(j)) and (∑ k, exp(t(k)))/(∑ k, exp(s(k))) are the same. (∑ j, (Real.exp (s j) / ∑ k, Real.exp (s…)
RReal numbers: The real numbers: every point on the number line. (ℝ)
·Multiplication: exp(s(j))/(∑ k, exp(s(k))) times exp(t(j) − s(j)). ((Real.exp (s j) / ∑ k, Real.exp (s k)) …)
eˣExponential function: e raised to the power s(j), where e ≈ 2.718. (Real.exp (s j))
a/bDivision: exp(s(j)) divided by ∑ k, exp(s(k)). In Lean, dividing by 0 gives 0. (Real.exp (s j) / ∑ k, Real.exp (s k))
∑Summation: Add up exp(s(k)) for every k. (∑ k, Real.exp (s k))
-Subtraction: t(j) minus s(j). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (t j - s j)

theorem rl-tilt-normaliser-ratio {J : Type} [Fintype J] [Nonempty J] (s t : J → ℝ) :
    ∑ j, (Real.exp (s j) / ∑ k, Real.exp (s k)) * Real.exp (t j - s j) = (∑ k, Real.exp (t k)) / ∑ k, Real.exp (s k)

The old keys' current normaliser is estimable from the snapshot proposal's own draws; needed to combine keys appended since the snapshot with rejection samples of the old keys (Drift Law loop 3). 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: 15 lines of Lean

Tilt normaliser identity: E_{π_s}[e^{t_j − s_j}] = Z_t / Z_s

How it was proved

More proved statements