Provedalphabaguettebaguette-zschedule

Any two-way split of an integer reduction recombines exactly

For all $\htmlData{mx=1}{n \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=5}{q : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{n}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{Z}}}$ and $\htmlData{mx=5}{s \in \htmlData{mx=4}{\htmlData{mx=0}{\operatorname{Finset}}\,\htmlData{mx=3}{\htmlData{mx=1}{\operatorname{Fin}}\,\htmlData{mx=2}{n}}}}$ :

\htmlData{mx=10}{\htmlData{mx=4}{\sum_{i \in \htmlData{mx=0}{s}} \htmlData{mx=3}{\htmlData{mx=1}{q}(\htmlData{mx=2}{i})}} + \htmlData{mx=9}{\sum_{i \in \htmlData{mx=5}{\operatorname{s^c}}} \htmlData{mx=8}{\htmlData{mx=6}{q}(\htmlData{mx=7}{i})}}} \mathrel{\htmlData{mx=15}{=}} \htmlData{mx=14}{\sum_{i} \htmlData{mx=13}{\htmlData{mx=11}{q}(\htmlData{mx=12}{i})}}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
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 → ℤ)
Finset: Finset: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Finset)
∑Summation: Add up q(i) for each i in s. (∑ i ∈ s, q i)
+Addition: ∑ i, q(i) plus ∑ i, q(i). (∑ i ∈ s, q i + ∑ i ∈ sᶜ, q i)
=Equality: (∑ i, q(i)) + (∑ i, q(i)) and ∑ i, q(i) are the same. (∑ i ∈ s, q i + ∑ i ∈ sᶜ, q i = ∑ i, q i)
ZIntegers: The integers …, −2, −1, 0, 1, 2, …. (ℤ)
sᶜ: sᶜ: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (sᶜ)

theorem bz-two-way-split-invariance {n : ℕ} (q : Fin n → ℤ) (s : Finset (Fin n)) :
    ∑ i ∈ s, q i + ∑ i ∈ sᶜ, q i = ∑ i, q i

Σ_{i∈s} q + Σ_{i∉s} q = Σ q for every subset s: tree-shaped reductions of any shape agree. Part of the plan 'Baguette-Z: closed-loop certified integer-state training'.

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

Any two-way split of an integer reduction recombines exactly

How it was proved

More proved statements