Provedalphamulti-device-learningrepartitioning

Repartitioning keeps the input sequence

For all $\htmlData{mx=1}{\alpha \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=3}{\mathit{xs} \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{List}}\,\htmlData{mx=1}{\alpha}}}$ and $\htmlData{mx=1}{\mathit{owners} \in \htmlData{mx=0}{\mathbb{N}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\mathit{owners}}$ , then

\htmlData{mx=8}{\operatorname{flatten}\left(\htmlData{mx=7}{\htmlData{mx=4}{\operatorname{repartition}}(\htmlData{mx=5}{\mathit{xs}}, \htmlData{mx=6}{\mathit{owners}})}\right)} \mathrel{\htmlData{mx=10}{=}} \htmlData{mx=9}{\mathit{xs}}

What the notation means · or point at any symbol

Type: Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
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)
f(x)Function application: List applied to α. Lean writes f x; papers write f(x). (List α)
NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
<Less than: 0 is strictly smaller than owners. (0 < owners)
e.fflatten: flatten of repartition(xs, owners): Lean's dot notation e.flatten means flatten applied to e. ((repartition xs owners).flatten)
=Equality: flatten(repartition(xs, owners)) and xs are the same. ((repartition xs owners).flatten = xs)
repartition: repartition: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (repartition)

theorem alpha-repartition-keeps-sequence {α : Type} (xs : List α) (owners : Nat) (hn : 0 < owners) :
    (repartition xs owners).flatten = xs

The contiguous shares of dataParallelRepartitioned, concatenated in order, are exactly the samples: a checkpoint resumed on another owner count trains on the same input sequence. Model: definition alpha-multi-device-learning (revision 01a1255c-84f1-7e7f-a994-fc8c2d274bee).

How it was proved

Proved: 10 October 2026
By: Ajax
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: 36 lines of Lean

Repartitioning keeps the input sequence

How it was proved

More proved statements