Provedalphamulti-device-learningordered-combine

The combine chain reads every owner once, in order

For all $\htmlData{mx=1}{\mathit{owner}, \mathit{count} \in \htmlData{mx=0}{\mathbb{N}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\mathit{count}}$ , then

\htmlData{mx=8}{\operatorname{leaves}\left(\htmlData{mx=7}{\htmlData{mx=4}{\operatorname{combineChain}}(\htmlData{mx=5}{\mathit{owner}}, \htmlData{mx=6}{\mathit{count}})}\right)} \mathrel{\htmlData{mx=12}{=}} \htmlData{mx=11}{\htmlData{mx=9}{\operatorname{range}}(\htmlData{mx=10}{\mathit{count}})}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
x ∈ TVariables: owner, count range over natural numbers: the statement must hold for every choice. ((owner count : Nat))
<Less than: 0 is strictly smaller than count. (0 < count)
e.fleaves: leaves of combineChain(owner, count): Lean's dot notation e.leaves means leaves applied to e. ((combineChain owner count).leaves)
=Equality: leaves(combineChain(owner, count)) and range(count) are the same. ((combineChain owner count).leaves = Lis…)
combineChain: combineChain: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (combineChain)
f(x)Function application: combineChain applied to owner, count. Lean writes f x; papers write f(x). (combineChain owner count)
range: List.range: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (List.range)

theorem alpha-combine-chain-covers-owners (owner count : Nat) (h : 0 < count) :
    (combineChain owner count).leaves = List.range count

For count > 0 the leaves of nativeCombineChain are exactly 0, 1, ..., count - 1. 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: 32 lines of Lean

The combine chain reads every owner once, in order

How it was proved

More proved statements