Provedalphabaguettenoether-checksumattention

The query kernel's D = ⟨dO, O⟩ equals the key kernel's Σₖ Pₖ⟨dO, Vₖ⟩

For all $\htmlData{mx=1}{T, D \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=5}{P : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{T}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{R}}}$ , $\htmlData{mx=5}{\mathit{dO} : \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=9}{V : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{T}} \mathrel{\htmlData{mx=8}{\to}} \htmlData{mx=5}{\htmlData{mx=3}{\operatorname{Fin}}\,\htmlData{mx=4}{D}} \mathrel{\htmlData{mx=7}{\to}} \htmlData{mx=6}{\mathbb{R}}}$ :

\begin{aligned} & \htmlData{mx=14}{\sum_{k} \htmlData{mx=13}{\htmlData{mx=3}{\htmlData{mx=1}{P}(\htmlData{mx=2}{k})} \cdot \left(\htmlData{mx=12}{\sum_{c} \htmlData{mx=11}{\htmlData{mx=6}{\htmlData{mx=4}{\mathit{dO}}(\htmlData{mx=5}{c})} \cdot \htmlData{mx=10}{\htmlData{mx=7}{V}(\htmlData{mx=8}{k}, \htmlData{mx=9}{c})}}}\right)}} \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=28}{\sum_{c} \htmlData{mx=27}{\htmlData{mx=17}{\htmlData{mx=15}{\mathit{dO}}(\htmlData{mx=16}{c})} \cdot \left(\htmlData{mx=26}{\sum_{k} \htmlData{mx=25}{\htmlData{mx=20}{\htmlData{mx=18}{P}(\htmlData{mx=19}{k})} \cdot \htmlData{mx=24}{\htmlData{mx=21}{V}(\htmlData{mx=22}{k}, \htmlData{mx=23}{c})}}}\right)}} \end{aligned}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
x ∈ TVariables: T, D range over natural numbers: the statement must hold for every choice. ((T D : ℕ))
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 T. Lean writes f x; papers write f(x). (Fin T)
⟹Implies: If Fin(T), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin T → ℝ)
=Equality: ∑ k, P(k) · (∑ c, dO(c) · V(k, c)) and ∑ c, dO(c) · (∑ k, P(k) · V(k, c)) are the same. (∑ k, P k * (∑ c, dO c * V k c) = ∑ c, d…)
RReal numbers: The real numbers: every point on the number line. (ℝ)
∑Summation: Add up dO(c) · V(k, c) for every c. (∑ c, dO c * V k c)
·Multiplication: dO(c) times V(k, c). (dO c * V k c)

theorem nc-flash-d-identity {T D : ℕ} (P : Fin T → ℝ) (dO : Fin D → ℝ) (V : Fin T → Fin D → ℝ) :
    ∑ k, P k * (∑ c, dO c * V k c) = ∑ c, dO c * (∑ k, P k * V k c)

Σₖ Pₖ·⟨dO, Vₖ⟩ = ⟨dO, Σₖ Pₖ Vₖ⟩ = ⟨dO, O⟩. Baguette's query and key backward kernels may form the row statistic in either way; this identity is why both must agree, and a wrong V buffer in one kernel breaks it. Part of 'Noether checksums for Baguette's backward kernels'.

How it was proved

Proved: 3 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

The query kernel's D = ⟨dO, O⟩ equals the key kernel's Σₖ Pₖ⟨dO, Vₖ⟩

How it was proved

More proved statements