Provedalphabaguettealgorithm-ideaa1

Grid-rounded integer accumulation is independent of summation order

For all $\htmlData{mx=1}{n, k \in \htmlData{mx=0}{\mathbb{N}}}$ , $\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}}}$ and $\htmlData{mx=5}{\sigma \in \htmlData{mx=4}{\htmlData{mx=0}{\operatorname{Perm}}\,\htmlData{mx=3}{\htmlData{mx=1}{\operatorname{Fin}}\,\htmlData{mx=2}{n}}}}$ :

\begin{aligned} & \htmlData{mx=10}{\sum_{i} \htmlData{mx=9}{\left\lfloor \htmlData{mx=8}{\htmlData{mx=5}{\htmlData{mx=1}{x}(\htmlData{mx=4}{\htmlData{mx=2}{\sigma}(\htmlData{mx=3}{i})})} \cdot \htmlData{mx=7}{2^{\htmlData{mx=6}{k}}}} \right\rfloor}} \mathrel{\htmlData{mx=19}{=}} \htmlData{mx=18}{\sum_{i} \htmlData{mx=17}{\left\lfloor \htmlData{mx=16}{\htmlData{mx=13}{\htmlData{mx=11}{x}(\htmlData{mx=12}{i})} \cdot \htmlData{mx=15}{2^{\htmlData{mx=14}{k}}}} \right\rfloor}} \\ & \htmlData{mx=0}{\land} \htmlData{mx=20}{\forall} l_{1}, l_{2} : \htmlData{mx=23}{\htmlData{mx=21}{\operatorname{List}}\,\htmlData{mx=22}{\mathbb{R}}}, \\ & \quad \htmlData{mx=29}{\htmlData{mx=27}{\operatorname{Perm}\left(\htmlData{mx=26}{l_{1}}\right)}\,\htmlData{mx=28}{l_{2}}} \\ & \quad \htmlData{mx=24}{\implies} \htmlData{mx=50}{\operatorname{sum}\left(\htmlData{mx=49}{\htmlData{mx=42}{\operatorname{map}\left(\htmlData{mx=41}{l_{1}}\right)}(\htmlData{mx=48}{y \mapsto \htmlData{mx=47}{\left\lfloor \htmlData{mx=46}{\htmlData{mx=43}{y} \cdot \htmlData{mx=45}{2^{\htmlData{mx=44}{k}}}} \right\rfloor}})}\right)} \mathrel{\htmlData{mx=72}{=}} \htmlData{mx=71}{\operatorname{sum}\left(\htmlData{mx=70}{\htmlData{mx=63}{\operatorname{map}\left(\htmlData{mx=62}{l_{2}}\right)}(\htmlData{mx=69}{y \mapsto \htmlData{mx=68}{\left\lfloor \htmlData{mx=67}{\htmlData{mx=64}{y} \cdot \htmlData{mx=66}{2^{\htmlData{mx=65}{k}}}} \right\rfloor}})}\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: 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 → ℝ)
Perm: Equiv.Perm: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Equiv.Perm)
∑Summation: Add up ⌊x(σ(i)) · 2^k⌋ for every i. (∑ i, ⌊x (σ i) * 2 ^ k⌋)
=Equality: ∑ i, ⌊x(σ(i)) · 2^k⌋ and ∑ i, ⌊x(i) · 2^k⌋ are the same. (∑ i, ⌊x (σ i) * 2 ^ k⌋ = ∑ i, ⌊x i * 2 …)
∧And: Both hold: (∑ i, ⌊x(σ(i)) · 2^k⌋) = (∑ i, ⌊x(i) · 2^k⌋), and ∀ l₁, l₂, Perm(l₂) → sum(map(y ↦ ⌊y · 2^k⌋)) = sum(map(y ↦…. (∑ i, ⌊x (σ i) * 2 ^ k⌋ = ∑ i, ⌊x i * 2 …)
⌊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)
RReal numbers: The real numbers: every point on the number line. (ℝ)
aᵇPower: 2 raised to the power k. (2 ^ k)
∀For all: The statement after the comma holds for every l₁, l₂. (∀ l₁ l₂ : List ℝ, l₁.Perm l₂ → (l₁.map …)
List: List: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (List)
e.fPerm: Perm of l₁: Lean's dot notation e.Perm means Perm applied to e. (l₁.Perm)
e.fsum: sum of map(y ↦ ⌊y · 2^k⌋): Lean's dot notation e.sum means sum applied to e. ((l₁.map (fun y => ⌊y * 2 ^ k⌋)).sum)
e.fmap: map of l₁: Lean's dot notation e.map means map applied to e. (l₁.map)
x ↦ f(x)Function (λ-abstraction): The function sending y to ⌊y · 2^k⌋. Lean writes fun x => …; papers write x ↦ …. (fun y => ⌊y * 2 ^ k⌋)

theorem ord-grid-sum-order-free (n k : ℕ) (x : Fin n → ℝ) (σ : Equiv.Perm (Fin n)) :
    ∑ i, ⌊x (σ i) * 2 ^ k⌋ = ∑ i, ⌊x i * 2 ^ k⌋ ∧ ∀ l₁ l₂ : List ℝ, l₁.Perm l₂ → (l₁.map (fun y => ⌊y * 2 ^ k⌋)).sum = (l₂.map (fun y => ⌊y * 2 ^ k⌋)).sum

Idea A1 (order-free exact accumulation). Once each term is rounded once onto the dyadic grid 2⁻ᵏ (⌊x·2ᵏ⌋), the integer sum is the same under any permutation of the terms (first conjunct) and for any reordered list, i.e. any arrival order of tile partials or atomics (second conjunct). Floating-point sums lack this; it is what lets a scheduler change grids/splits without changing checkpoint bits.

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

Grid-rounded integer accumulation is independent of summation order

How it was proved

More proved statements