Provedalphamulti-device-learningordered-combine

A wide enough hierarchy is the star's chain

For all $\htmlData{mx=1}{\mathit{fanout}, \mathit{count} \in \htmlData{mx=0}{\mathbb{N}}}$ , if $\htmlData{mx=1}{\htmlData{mx=0}{\mathit{count}} - 1} \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\mathit{fanout}}$ , then

\htmlData{mx=3}{\htmlData{mx=0}{\operatorname{combineHierarchy}}(\htmlData{mx=1}{\mathit{fanout}}, \htmlData{mx=2}{\mathit{count}})} \mathrel{\htmlData{mx=7}{=}} \htmlData{mx=6}{\htmlData{mx=4}{\operatorname{combineChain}}(0, \htmlData{mx=5}{\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: fanout, count range over natural numbers: the statement must hold for every choice. ((fanout count : Nat))
-Subtraction: count minus 1. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (count - 1)
≤At most: count − 1 is less than or equal to fanout. (count - 1 ≤ fanout)
combineHierarchy: combineHierarchy: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (combineHierarchy)
f(x)Function application: combineHierarchy applied to fanout, count. Lean writes f x; papers write f(x). (combineHierarchy fanout count)
=Equality: combineHierarchy(fanout, count) and combineChain(0, count) are the same. (combineHierarchy fanout count = combine…)
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)

theorem alpha-combine-hierarchy-wide-is-chain (fanout count : Nat) (h : count - 1 ≤ fanout) :
    combineHierarchy fanout count = combineChain 0 count

With fan-out at least count - 1 every owner is a child of the root, and nativeCombineHierarchy fanout count is exactly nativeCombineChain 0 count (with Alpha's own fuel). 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: Quot.sound, propext
Proof: 65 lines of Lean

A wide enough hierarchy is the star's chain

How it was proved

More proved statements