Provedalphamulti-device-learningpartitioning

Assembly by selection gathers every coordinate from its owner

For all $\htmlData{mx=1}{\alpha \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=1}{k, \mathit{owners} \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=5}{\mathit{value} : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=1}{\mathbb{N}} \mathrel{\htmlData{mx=3}{\to}} \htmlData{mx=2}{\alpha}}$ , $\htmlData{mx=1}{t \in \htmlData{mx=0}{\operatorname{CombineTree}}}$ and $\htmlData{mx=1}{\mathit{nodup} \in \htmlData{mx=0}{\operatorname{Nodup}}}$ :

\begin{aligned} & \htmlData{mx=0}{\exists} \mathit{result}, \\ & \quad \htmlData{mx=21}{\htmlData{mx=3}{\operatorname{evalRefusing}}(\htmlData{mx=6}{\htmlData{mx=4}{\operatorname{assembleSelect}}(\htmlData{mx=5}{k})}, \htmlData{mx=19}{o \mapsto \htmlData{mx=18}{\left\langle \htmlData{mx=9}{\htmlData{mx=7}{\mathit{value}}(\htmlData{mx=8}{o})}, \htmlData{mx=17}{i \mapsto \htmlData{mx=13}{\htmlData{mx=10}{\operatorname{coordinateOwner}}(\htmlData{mx=11}{\mathit{owners}}, \htmlData{mx=12}{i})} \mathrel{\htmlData{mx=16}{=}} \htmlData{mx=15}{\mathtt{=}(\htmlData{mx=14}{o})}} \right\rangle}}, \htmlData{mx=20}{t})} \\ & \quad \quad \htmlData{mx=2}{=} \htmlData{mx=24}{\htmlData{mx=22}{\operatorname{some}}(\htmlData{mx=23}{\mathit{result}})} \\ & \quad \htmlData{mx=1}{\land} \htmlData{mx=25}{\forall} i, \\ & \quad \quad \htmlData{mx=32}{\htmlData{mx=30}{\operatorname{owned}\left(\htmlData{mx=29}{\mathit{result}}\right)}(\htmlData{mx=31}{i})} \\ & \quad \quad \quad \htmlData{mx=27}{=} \htmlData{mx=42}{\htmlData{mx=33}{\operatorname{decide}}(\htmlData{mx=37}{\htmlData{mx=34}{\operatorname{coordinateOwner}}(\htmlData{mx=35}{\mathit{owners}}, \htmlData{mx=36}{i})} \mathrel{\htmlData{mx=41}{\in}} \htmlData{mx=40}{\operatorname{leaves}\left(\htmlData{mx=39}{t}\right)})} \\ & \quad \quad \htmlData{mx=26}{\land} \left(\right. \htmlData{mx=48}{\htmlData{mx=46}{\operatorname{owned}\left(\htmlData{mx=45}{\mathit{result}}\right)}(\htmlData{mx=47}{i})} \mathrel{\htmlData{mx=50}{=}} \htmlData{mx=49}{\operatorname{true}} \\ & \quad \quad \htmlData{mx=43}{\implies} \htmlData{mx=55}{\htmlData{mx=53}{\operatorname{value}\left(\htmlData{mx=52}{\mathit{result}}\right)}(\htmlData{mx=54}{i})} \mathrel{\htmlData{mx=63}{=}} \htmlData{mx=62}{\htmlData{mx=56}{\mathit{value}}(\htmlData{mx=60}{\htmlData{mx=57}{\operatorname{coordinateOwner}}(\htmlData{mx=58}{\mathit{owners}}, \htmlData{mx=59}{i})}, \htmlData{mx=61}{i})} \left.\right) \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: k, owners range over natural numbers: the statement must hold for every choice. ((k owners : 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)
Nodup: t.leaves.Nodup: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (t.leaves.Nodup)
∃There exists: At least one result makes the statement after the comma true. (∃ result, evalRefusing (assembleSelect …)
⟹Implies: If Nat, then α. (Between types, A → B is the type of functions from A to B.) (Nat → α)
evalRefusing: evalRefusing: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (evalRefusing)
assembleSelect: assembleSelect: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (assembleSelect)
f(x)Function application: assembleSelect applied to k. Lean writes f x; papers write f(x). (assembleSelect k)
⟨a, b⟩Anonymous constructor: Builds a structure (a pair, a subtype element, …) from value(o), i ↦ coordinateOwner(owners, i) = =(o). (⟨value o, fun i => coordinateOwner owne…)
x ↦ f(x)Function (λ-abstraction): The function sending i to coordinateOwner(owners, i) = =(o). Lean writes fun x => …; papers write x ↦ …. (fun i => coordinateOwner owners i == o)
coordinateOwner: coordinateOwner: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (coordinateOwner)
=Equality: coordinateOwner(owners, i) and =(o) are the same. (coordinateOwner owners i == o)
some: some: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (some)
∀For all: The statement after the comma holds for every i. (∀ i, result.owned i = decide (coordinat…)
e.fowned: owned of result: Lean's dot notation e.owned means owned applied to e. (result.owned)
∧And: Both hold: owned(i) = decide(coordinateOwner(owners, i) ∈ t.leaves), and owned(i) = true → value(i) = value(coordinateOwner(owners,…. (result.owned i = decide (coordinateOwne…)
decide: decide: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (decide)
∈Element of: coordinateOwner(owners, i) is a member of t.leaves. (coordinateOwner owners i ∈ t.leaves)
e.fleaves: leaves of t: Lean's dot notation e.leaves means leaves applied to e. (t.leaves)
true: true: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (true)
e.fvalue: value of result: Lean's dot notation e.value means value applied to e. (result.value)

theorem alpha-assembly-by-selection-exact {α : Type} (k owners : Nat) (value : Nat → Nat → α) (t : CombineTree) (nodup : t.leaves.Nodup) :
    ∃ result, evalRefusing (assembleSelect k) (fun o => ⟨value o, fun i => coordinateOwner owners i == o⟩) t = some result ∧ ∀ i, result.owned i = decide (coordinateOwner owners i ∈ t.leaves) ∧ (result.owned i = true → result.value i = value (coordinateOwner owners i) i)

When each offer's ownership mask marks exactly the coordinates i with i mod owners equal to the offering owner and the combine tree's leaves are distinct, the selection combine (dpoSelect) never refuses, marks a coordinate owned exactly when its owner is a leaf, and then holds that owner's value. 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: 57 lines of Lean

Assembly by selection gathers every coordinate from its owner

How it was proved

More proved statements