Provedalphabaguettealgorithm-ideaa1

Order-free grid accumulation is within n·2⁻ᵏ of the exact sum

For all $\htmlData{mx=1}{n, k \in \htmlData{mx=0}{\mathbb{N}}}$ and $\htmlData{mx=5}{x : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{n}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{R}}}$ :

\htmlData{mx=17}{\left\lvert \htmlData{mx=16}{\htmlData{mx=3}{\sum_{i} \htmlData{mx=2}{\htmlData{mx=0}{x}(\htmlData{mx=1}{i})}} - \htmlData{mx=15}{\frac{\htmlData{mx=12}{\sum_{i} \htmlData{mx=11}{\htmlData{mx=10}{\left\lfloor \htmlData{mx=9}{\htmlData{mx=6}{\htmlData{mx=4}{x}(\htmlData{mx=5}{i})} \cdot \htmlData{mx=8}{2^{\htmlData{mx=7}{k}}}} \right\rfloor}}}}{\htmlData{mx=14}{2^{\htmlData{mx=13}{k}}}}}} \right\rvert} \mathrel{\htmlData{mx=22}{\leq}} \htmlData{mx=21}{\frac{\htmlData{mx=18}{n}}{\htmlData{mx=20}{2^{\htmlData{mx=19}{k}}}}}

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: n, k range over natural numbers: the statement must hold for every choice. ((n k : ℕ))
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 n. Lean writes f x; papers write f(x). (Fin n)
⟹Implies: If Fin(n), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin n → ℝ)
|x|Absolute value: The size of (∑ i, x(i)) − (∑ i, ⌊x(i) · 2^k⌋)/2^k without its sign. (|∑ i, x i - (∑ i, (⌊x i * 2 ^ k⌋ : ℝ)) …)
≤At most: |(∑ i, x(i)) − (∑ i, ⌊x(i) · 2^k⌋)/2^k| is less than or equal to n/2^k. (|∑ i, x i - (∑ i, (⌊x i * 2 ^ k⌋ : ℝ)) …)
∑Summation: Add up x(i) for every i. (∑ i, x i)
-Subtraction: ∑ i, x(i) minus (∑ i, ⌊x(i) · 2^k⌋)/2^k. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (∑ i, x i - (∑ i, (⌊x i * 2 ^ k⌋ : ℝ)) /…)
RReal numbers: The real numbers: every point on the number line. (ℝ)
a/bDivision: ∑ i, ⌊x(i) · 2^k⌋ divided by 2^k. In Lean, dividing by 0 gives 0. ((∑ i, (⌊x i * 2 ^ k⌋ : ℝ)) / 2 ^ k)
(x : T)As real numbers: ⌊x(i) · 2^k⌋ read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((⌊x i * 2 ^ k⌋ : ℝ))
⌊x⌋Floor: The largest integer not above x(i) · 2^k. (⌊x i * 2 ^ k⌋)
·Multiplication: x(i) times 2^k. (x i * 2 ^ k)
aᵇPower: 2 raised to the power k. (2 ^ k)

theorem ord-grid-sum-error-bound (n k : ℕ) (x : Fin n → ℝ) :
    |∑ i, x i - (∑ i, (⌊x i * 2 ^ k⌋ : ℝ)) / 2 ^ k| ≤ n / 2 ^ k

Idea A1. The only rounding in grid accumulation is one floor per term, so the reconstructed sum 2⁻ᵏ·Σ⌊xᵢ·2ᵏ⌋ differs from the exact real sum by at most n·2⁻ᵏ, deterministically and independently of order.

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: 31 lines of Lean

Order-free grid accumulation is within n·2⁻ᵏ of the exact sum

How it was proved

More proved statements