Provedalphabaguettenoether-checksumreview-2

Floating-point threshold from the standard model: |Σ aᵢⱼ(1+δᵢⱼ) − Σ aᵢⱼ| ≤ γ·Σ|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=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

\begin{aligned} & \htmlData{mx=20}{\left\lvert \htmlData{mx=19}{\htmlData{mx=12}{\sum_{i} \htmlData{mx=11}{\sum_{j} \htmlData{mx=10}{\htmlData{mx=4}{\htmlData{mx=1}{a}(\htmlData{mx=2}{i}, \htmlData{mx=3}{j})} \cdot (\htmlData{mx=9}{1 + \htmlData{mx=8}{\htmlData{mx=5}{\delta}(\htmlData{mx=6}{i}, \htmlData{mx=7}{j})}})}}} - \htmlData{mx=18}{\sum_{i} \htmlData{mx=17}{\sum_{j} \htmlData{mx=16}{\htmlData{mx=13}{a}(\htmlData{mx=14}{i}, \htmlData{mx=15}{j})}}}} \right\rvert} \\ & \quad \htmlData{mx=0}{\leq} \htmlData{mx=29}{\htmlData{mx=21}{\gamma} \cdot \htmlData{mx=28}{\sum_{i} \htmlData{mx=27}{\sum_{j} \htmlData{mx=26}{\left\lvert \htmlData{mx=25}{\htmlData{mx=22}{a}(\htmlData{mx=23}{i}, \htmlData{mx=24}{j})} \right\rvert}}}} \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: 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 → ℝ))
∀For all: The statement after the comma holds for every i, j. (∀ i j, |δ i j| ≤ γ)
-Subtraction: ∑ i, ∑ j, a(i, j) · (1 + δ(i, j)) minus ∑ i, ∑ j, a(i, j). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (∑ i, ∑ j, a i j * (1 + δ i j) - ∑ i, ∑ …)
∑Summation: Add up a(i, j) · (1 + δ(i, j)) for every j. (∑ j, a i j * (1 + δ 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-standard-model-residual-bound {m n : ℕ} (a δ : Fin m → Fin n → ℝ) (γ : ℝ) (hδ : ∀ i j, |δ i j| ≤ γ) :
    |∑ i, ∑ j, a i j * (1 + δ i j) - ∑ i, ∑ j, a i j| ≤ γ * ∑ i, ∑ j, |a i j|

Under the standard rounding model (each product enters the computed sum with relative error |δ| ≤ γ, e.g. Higham's γₙ for an n-term FP32 accumulation of BF16 products), a checksum whose exact value is Σaᵢⱼ is computed within γ·Σ|aᵢⱼ|. For zero-sum checksums (C1), this gives the certified threshold of nc-certified-threshold-rule with aⱼ = Σᵢ|aᵢⱼ|. The floating-point model itself is assumed, not formalized. 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: 22 lines of Lean

Floating-point threshold from the standard model: |Σ aᵢⱼ(1+δᵢⱼ) − Σ aᵢⱼ| ≤ γ·Σ|aᵢⱼ|

How it was proved

More proved statements