proofs
Provedalphamulti-device-learningordered-combine

Replication reaches every owner

For all o∈N\htmlData{mx=1}{o \in \htmlData{mx=0}{\mathbb{N}}}, l,r∈CombineTree⁡\htmlData{mx=1}{l, r \in \htmlData{mx=0}{\operatorname{CombineTree}}} and owner∈N\htmlData{mx=1}{\mathit{owner} \in \htmlData{mx=0}{\mathbb{N}}}, if owner∈leaves⁡(branch⁡(o,l,r))\htmlData{mx=0}{\mathit{owner}} \mathrel{\htmlData{mx=12}{\in}} \htmlData{mx=11}{\operatorname{leaves}\left(\htmlData{mx=10}{\htmlData{mx=6}{\operatorname{branch}}(\htmlData{mx=7}{o}, \htmlData{mx=8}{l}, \htmlData{mx=9}{r})}\right)}, then

leaf⁡(owner)∈deliveryMoves⁡(.replicateAll (.branch o l r))\htmlData{mx=5}{\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{leaf}}(\htmlData{mx=1}{\mathit{owner}})} \mathrel{\htmlData{mx=4}{\in}} \htmlData{mx=3}{\operatorname{deliveryMoves}}(\mathtt{.replicateAll\ (.branch\ o\ l\ r)})}
What the notation means · or point at any symbol
NNatural numbers
The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
CombineTree
CombineTree: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (CombineTree)
x ∈ TVariables
l, r range over CombineTree: the statement must hold for every choice. ((l r : CombineTree))
∈Element of
owner is a member of leaves(branch(o, l, r)). (owner ∈ (CombineTree.branch o l r).leav…)
leaf
CombineTree.leaf: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (CombineTree.leaf)
e.fleaves
leaves of branch(o, l, r): Lean's dot notation e.leaves means leaves applied to e. ((CombineTree.branch o l r).leaves)
branch
CombineTree.branch: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (CombineTree.branch)
f(x)Function application
CombineTree.branch applied to o, l, r. Lean writes f x; papers write f(x). (CombineTree.branch o l r)
deliveryMoves
deliveryMoves: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (deliveryMoves)

CombineReplicateAll moves the reduced value into every leaf of a branch. 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
propext
Proof
40 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements