proofs
Provedalphamulti-device-learningordered-combine

Reduction to one owner reaches that owner

For all target,o∈N\htmlData{mx=1}{\mathit{target}, o \in \htmlData{mx=0}{\mathbb{N}}} and l,r∈CombineTree⁡\htmlData{mx=1}{l, r \in \htmlData{mx=0}{\operatorname{CombineTree}}}, if target∈leaves⁡(branch⁡(o,l,r))\htmlData{mx=0}{\mathit{target}} \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⁡(target)∈deliveryMoves⁡(.(deliverTo⁡,target),.(branch⁡,o,l,r))\begin{aligned} & \htmlData{mx=3}{\htmlData{mx=1}{\operatorname{leaf}}(\htmlData{mx=2}{\mathit{target}})} \\ & \quad \htmlData{mx=0}{\in} \htmlData{mx=13}{\htmlData{mx=4}{\operatorname{deliveryMoves}}(\htmlData{mx=7}{\mathtt{.}(\htmlData{mx=5}{\operatorname{deliverTo}}, \htmlData{mx=6}{\mathit{target}})}, \htmlData{mx=12}{\mathtt{.}(\htmlData{mx=8}{\operatorname{branch}}, \htmlData{mx=9}{o}, \htmlData{mx=10}{l}, \htmlData{mx=11}{r})})} \end{aligned}
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
target, o range over natural numbers: the statement must hold for every choice. ((target o : 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)
∈Element of
target is a member of leaves(branch(o, l, r)). (target ∈ (CombineTree.branch o l r).lea…)
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)
deliverTo
deliverTo: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (deliverTo)

For a branch whose leaves include the target, CombineDeliverTo target moves the reduced value into the target's leaf. 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
60 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements