Proveddrift-lawdecodevariational-cost-lawfirst-principles
Bayes-optimal snapshot proposal: under a drift prior, the least expected second moment for the numerator is (Σ_j e^{s_j}√E[e^{2δ_j}])², attained by r_j ∝ e^{s_j}√E[e^{2δ_j}]
For all , , , and , if , , and (given , and ), then
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) - x ∈ TVariables
- Ω, J range over Type: the statement must hold for every choice. (
(Ω J : 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 Ω. Lean writes f x; papers write f(x). (
Fintype Ω) - 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 Ω, then ℝ. (Between types, A → B is the type of functions from A to B.) (
Ω → ℝ) - ∀For all
- The statement after the comma holds for every ω. (
∀ ω, 0 ≤ lam ω) - ∑Summation
- Add up lam(ω) for every ω. (
∑ ω, lam ω) - =Equality
- ∑ ω, lam(ω) and 1 are the same. (
∑ ω, lam ω = 1) - aᵇPower
- ∑ j, exp(s(j)) · √(∑ ω, lam(ω) · exp(2 · δ(ω, j))) raised to the power 2. (
(∑ j, Real.exp (s j) * Real.sqrt (∑ ω, …) - ∧And
- Both hold: (∑ j, exp(s(j)) · √(∑ ω, lam(ω) · exp(2 · δ(ω, j))))^2 ≤ (…, and (∑ ω, lam(ω) · (∑ j, exp(s(j) + δ(ω, j))^2/(exp(s(j)) · √(…. (
(∑ j, Real.exp (s j) * Real.sqrt (∑ ω, …) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - ≤At most
- 0 is less than or equal to lam(ω). (
0 ≤ lam ω) - <Less than
- 0 is strictly smaller than r(j). (
0 < r j) - eˣExponential function
- e raised to the power s(j), where e ≈ 2.718. (
Real.exp (s j)) - √Square root
- The non-negative number whose square is ∑ ω, lam(ω) · exp(2 · δ(ω, j)). (
Real.sqrt (∑ ω, lam ω * Real.exp (2 * δ…) - ·Multiplication
- 2 times δ(ω, j). (
2 * δ ω j) - a/bDivision
- exp(s(j) + δ(ω, j))^2 divided by r(j). In Lean, dividing by 0 gives 0. (
Real.exp (s j + δ ω j) ^ 2 / r j) - +Addition
- s(j) plus δ(ω, j). (
s j + δ ω j)
theorem drift-bayes-optimal-snapshot-proposal {Ω J : Type} [Fintype Ω] [Fintype J] [Nonempty J] (lam : Ω → ℝ) (s : J → ℝ) (δ : Ω → J → ℝ) (r : J → ℝ) (hlam : ∀ ω, 0 ≤ lam ω) (hlams : ∑ ω, lam ω = 1) (hr : ∀ j, 0 < r j) (hrs : ∑ j, r j = 1) :
(∑ j, Real.exp (s j) * Real.sqrt (∑ ω, lam ω * Real.exp (2 * δ ω j))) ^ 2 ≤ ∑ ω, lam ω * ∑ j, Real.exp (s j + δ ω j) ^ 2 / r j ∧ ∑ ω, lam ω * ∑ j, Real.exp (s j + δ ω j) ^ 2 / (Real.exp (s j) * Real.sqrt (∑ ω', lam ω' * Real.exp (2 * δ ω' j)) / ∑ i, Real.exp (s i) * Real.sqrt (∑ ω', lam ω' * Real.exp (2 * δ ω' i))) = (∑ j, Real.exp (s j) * Real.sqrt (∑ ω, lam ω * Real.exp (2 * δ ω j))) ^ 2Instance of the variational cost law with the mixture over drift outcomes ω (weights λ_ω) and unnormalised current weights e^{s_j + δ_ωj}. The optimal proposal is not the stale row itself but the stale row reweighted by the square root of each key's drift moment E[e^{2δ_j}]. For drift δ_j = d·k_j with random d, this moment grows with the key norm, which is the first-principles reason to treat high-norm keys specially (norm tiering). First-principles reformulation, 2026-10-05.
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
- 72 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.