Provedalphamulti-device-learningordered-combine

Reduction to one owner moves the value only along its path

For all $\htmlData{mx=1}{\mathit{target} \in \htmlData{mx=0}{\mathbb{N}}}$ and $\htmlData{mx=1}{t, s \in \htmlData{mx=0}{\operatorname{CombineTree}}}$ , if $\htmlData{mx=0}{s} \mathrel{\htmlData{mx=7}{\in}} \htmlData{mx=6}{\htmlData{mx=1}{\operatorname{deliveryMoves}}(\htmlData{mx=4}{\mathtt{.}(\htmlData{mx=2}{\operatorname{deliverTo}}, \htmlData{mx=3}{\mathit{target}})}, \htmlData{mx=5}{t})}$ , then

\htmlData{mx=0}{\mathit{target}} \mathrel{\htmlData{mx=4}{\in}} \htmlData{mx=3}{\operatorname{leaves}\left(\htmlData{mx=2}{s}\right)}

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: t, s range over CombineTree: the statement must hold for every choice. ((t s : CombineTree))
∈Element of: s is a member of deliveryMoves(.(deliverTo, target), t). (s ∈ deliveryMoves (.deliverTo target) t)
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)
e.fleaves: leaves of s: Lean's dot notation e.leaves means leaves applied to e. (s.leaves)
f(x)Function application: . applied to deliverTo, target. Lean writes f x; papers write f(x). (.deliverTo target)
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)

theorem alpha-delivery-stays-on-path (target : Nat) (t s : CombineTree) (hs : s ∈ deliveryMoves (.deliverTo target) t) :
    target ∈ s.leaves

Under CombineDeliverTo target, every subtree the reduced value is moved into contains the target: the value runs from the root down the tree path to the target's leaf and nowhere else. 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: 38 lines of Lean

Reduction to one owner moves the value only along its path

How it was proved

More proved statements