Proveddrift-lawdecodeself-certifyingexactness
Snapshot reuse cost, self-certified: E_{π_s}[w²]/E_{π_s}[w]² = Z_s Z_{2t−s} / Z_t² for weights w = e^{t−s} drawn from a snapshot row π_s
For all and (given and ):
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))^2)/(∑ … and (∑ k, exp(s(k))) · (∑ k, exp(2 · t(k) − s(k)))/(∑ k, exp(t… are the same. (
(∑ j, (Real.exp (s j) / ∑ k, Real.exp (…) - 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))^2. (
(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)) - aᵇPower
- exp(t(j) − s(j)) raised to the power 2. (
Real.exp (t j - s j) ^ 2) - -Subtraction
- t(j) minus s(j). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
t j - s j)
theorem rl-snis-reuse-cost-identity {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) ^ 2) / (∑ j, (Real.exp (s j) / ∑ k, Real.exp (s k)) * Real.exp (t j - s j)) ^ 2 = (∑ k, Real.exp (s k)) * (∑ k, Real.exp (2 * t k - s k)) / (∑ k, Real.exp (t k)) ^ 2The ratio the self-certificate measures from snapshot draws equals the exact reuse cost 1 + χ²(π_t‖π_s), the Fisher-Cover tilt cost. Snapshot SNIS made unbiased by MLMC therefore needs no worst-case tilt certificate: the draws certify the cost, and the snapshot is refreshed when it crosses a threshold. Closes the Drift Law exactness gap exposed by norm-product looseness on trained models (arXiv 2609.06327). Part of 'The Drift Law' (certificate-free exact variant: snapshot SNIS + MLMC with a self-certified cost).
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
- 26 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.