Provedalphabaguettenoether-checksumreview-2

Composed: a zero-sum checksum computed under the standard model never exceeds γ·Σ|aᵢⱼ|

For all $\htmlData{mx=1}{m, n \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=9}{a, \delta : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{m}} \mathrel{\htmlData{mx=8}{\to}} \htmlData{mx=5}{\htmlData{mx=3}{\operatorname{Fin}}\,\htmlData{mx=4}{n}} \mathrel{\htmlData{mx=7}{\to}} \htmlData{mx=6}{\mathbb{R}}}$ and $\htmlData{mx=1}{\gamma \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=5}{\sum_{i} \htmlData{mx=4}{\sum_{j} \htmlData{mx=3}{\htmlData{mx=0}{a}(\htmlData{mx=1}{i}, \htmlData{mx=2}{j})}}} \mathrel{\htmlData{mx=6}{=}} 0$ and $\htmlData{mx=7}{\forall i, j,\ \htmlData{mx=4}{\left\lvert \htmlData{mx=3}{\htmlData{mx=0}{\delta}(\htmlData{mx=1}{i}, \htmlData{mx=2}{j})} \right\rvert} \mathrel{\htmlData{mx=6}{\leq}} \htmlData{mx=5}{\gamma}}$ , then

\htmlData{mx=12}{\left\lvert \htmlData{mx=11}{\sum_{i} \htmlData{mx=10}{\sum_{j} \htmlData{mx=9}{\htmlData{mx=3}{\htmlData{mx=0}{a}(\htmlData{mx=1}{i}, \htmlData{mx=2}{j})} \cdot (\htmlData{mx=8}{1 + \htmlData{mx=7}{\htmlData{mx=4}{\delta}(\htmlData{mx=5}{i}, \htmlData{mx=6}{j})}})}}} \right\rvert} \mathrel{\htmlData{mx=22}{\leq}} \htmlData{mx=21}{\htmlData{mx=13}{\gamma} \cdot \htmlData{mx=20}{\sum_{i} \htmlData{mx=19}{\sum_{j} \htmlData{mx=18}{\left\lvert \htmlData{mx=17}{\htmlData{mx=14}{a}(\htmlData{mx=15}{i}, \htmlData{mx=16}{j})} \right\rvert}}}}

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: m, n range over natural numbers: the statement must hold for every choice. ((m n : ℕ))
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 m. Lean writes f x; papers write f(x). (Fin m)
x : TVariables: a, δ range over Fin m → Fin n → ℝ: the statement must hold for every choice. ((a δ : Fin m → Fin n → ℝ))
=Equality: ∑ i, ∑ j, a(i, j) and 0 are the same. (∑ i, ∑ j, a i j = 0)
∀For all: The statement after the comma holds for every i, j. (∀ i j, |δ i j| ≤ γ)
∑Summation: Add up a(i, j) for every j. (∑ j, a i j)
|x|Absolute value: The size of δ(i, j) without its sign. (|δ i j|)
≤At most: |δ(i, j)| is less than or equal to γ. (|δ i j| ≤ γ)
⟹Implies: If Fin(n), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin n → ℝ)
·Multiplication: a(i, j) times 1 + δ(i, j). (a i j * (1 + δ i j))
RReal numbers: The real numbers: every point on the number line. (ℝ)
+Addition: 1 plus δ(i, j). (1 + δ i j)

theorem nc2-zero-sum-certified-threshold {m n : ℕ} (a δ : Fin m → Fin n → ℝ) (γ : ℝ) (hzero : ∑ i, ∑ j, a i j = 0) (hδ : ∀ i j, |δ i j| ≤ γ) :
    |∑ i, ∑ j, a i j * (1 + δ i j)| ≤ γ * ∑ i, ∑ j, |a i j|

Combines the standard-model residual bound with an exact zero sum (Σᵢⱼ aᵢⱼ = 0, e.g. C1's ΣⱼΣᵢ Rᵢⱼqᵢ). A correctly working kernel's computed checksum satisfies |Σ aᵢⱼ(1+δᵢⱼ)| ≤ γ·Σ|aᵢⱼ|. Exceeding it is a proof of a bug relative to the error model. The kernel can accumulate Σ|aᵢⱼ| alongside the checksum at one extra FMA per term. Part of 'Noether checksums for Baguette's backward kernels' (review pass 2).

How it was proved

Proved: 4 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: 24 lines of Lean

Composed: a zero-sum checksum computed under the standard model never exceeds γ·Σ|aᵢⱼ|

How it was proved

More proved statements