Provedalphamulti-device-learningordered-combine

The star's combine chain is left-deep in role order

For all $\htmlData{mx=1}{\alpha \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=5}{\mathit{op} : \htmlData{mx=0}{\alpha} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=1}{\alpha} \mathrel{\htmlData{mx=3}{\to}} \htmlData{mx=2}{\alpha}}$ , $\htmlData{mx=3}{v : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\alpha}}$ and $\htmlData{mx=1}{\mathit{owner}, \mathit{count} \in \htmlData{mx=0}{\mathbb{N}}}$ :

\begin{aligned} & \htmlData{mx=12}{\htmlData{mx=9}{\operatorname{eval}\left(\htmlData{mx=8}{\htmlData{mx=5}{\operatorname{combineChain}}(\htmlData{mx=6}{\mathit{owner}}, \htmlData{mx=7}{\mathit{count}})}\right)}(\htmlData{mx=10}{\mathit{op}}, \htmlData{mx=11}{v})} \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=32}{\htmlData{mx=21}{\operatorname{foldl}\left(\htmlData{mx=20}{\htmlData{mx=17}{\operatorname{range}}(\htmlData{mx=19}{\htmlData{mx=18}{\mathit{count}} - 1})}\right)}(\htmlData{mx=29}{x, i \mapsto \htmlData{mx=28}{\htmlData{mx=22}{\mathit{op}}(\htmlData{mx=23}{x}, \htmlData{mx=27}{\htmlData{mx=24}{v}(\htmlData{mx=26}{\htmlData{mx=25}{i} + 1})})}}, \htmlData{mx=31}{\htmlData{mx=30}{v}(0)})} \end{aligned}

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)
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))
e.feval: eval of combineChain(owner, count): Lean's dot notation e.eval means eval applied to e. ((combineChain owner count).eval)
=Equality: eval(combineChain(owner, count))(op, v) and foldl(range(count − 1))(x, i ↦ op(x, v(i + 1)), v(0)) are the same. ((combineChain owner count).eval op v = …)
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)
⟹Implies: If α, then α. (Between types, A → B is the type of functions from A to B.) (α → α)
e.ffoldl: foldl of range(count − 1): Lean's dot notation e.foldl means foldl applied to e. ((List.range (count - 1)).foldl)
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)
-Subtraction: count minus 1. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (count - 1)
x ↦ f(x)Function (λ-abstraction): The function sending x, i to op(x, v(i + 1)). Lean writes fun x => …; papers write x ↦ …. (fun x i => op x (v (i + 1)))
+Addition: i plus 1. (i + 1)

theorem alpha-combine-chain-order {α : Type} (op : α → α → α) (v : Nat → α) (owner count : Nat) :
    (combineChain owner count).eval op v = (List.range (count - 1)).foldl (fun x i => op x (v (i + 1))) (v 0)

nativeCombineChain owner count evaluates (((v0 op v1) op v2) op ...) over roles 0..count-1, for any combining operation (Alpha combines binary64 values, which are not associative). Model: definition alpha-multi-device-learning.

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: None
Proof: 28 lines of Lean

The star's combine chain is left-deep in role order

How it was proved

More proved statements