Provedalphamulti-device-learningpartitioning

Assembly records only actual owners and refuses two owners

For all $\htmlData{mx=1}{\alpha \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=1}{k \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=5}{\mathit{offers} : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\htmlData{mx=1}{\operatorname{Offer}}\,\htmlData{mx=2}{\alpha}}}$ , $\htmlData{mx=1}{t \in \htmlData{mx=0}{\operatorname{CombineTree}}}$ and $\htmlData{mx=3}{\mathit{result} \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Offer}}\,\htmlData{mx=1}{\alpha}}}$ , if $\htmlData{mx=6}{\htmlData{mx=0}{\operatorname{evalRefusing}}(\htmlData{mx=3}{\htmlData{mx=1}{\operatorname{assembleSelect}}(\htmlData{mx=2}{k})}, \htmlData{mx=4}{\mathit{offers}}, \htmlData{mx=5}{t})} \mathrel{\htmlData{mx=10}{=}} \htmlData{mx=9}{\htmlData{mx=7}{\operatorname{some}}(\htmlData{mx=8}{\mathit{result}})}$ , then

\begin{aligned} & (\htmlData{mx=24}{\forall i,\ \htmlData{mx=5}{\htmlData{mx=3}{\operatorname{owned}\left(\htmlData{mx=2}{\mathit{result}}\right)}(\htmlData{mx=4}{i})} \mathrel{\htmlData{mx=7}{=}} \htmlData{mx=6}{\operatorname{true}} \mathrel{\htmlData{mx=23}{\iff}} \htmlData{mx=22}{\exists o \in \htmlData{mx=21}{\operatorname{leaves}\left(\htmlData{mx=20}{t}\right)},\ \htmlData{mx=16}{\htmlData{mx=14}{\operatorname{owned}\left(\htmlData{mx=13}{\htmlData{mx=11}{\mathit{offers}}(\htmlData{mx=12}{o})}\right)}(\htmlData{mx=15}{i})} \mathrel{\htmlData{mx=18}{=}} \htmlData{mx=17}{\operatorname{true}}}}) \\ & \htmlData{mx=0}{\land} \htmlData{mx=55}{\forall i,\ \htmlData{mx=25}{i} \mathrel{\htmlData{mx=27}{<}} \htmlData{mx=26}{k} \mathrel{\htmlData{mx=54}{\implies}} \htmlData{mx=52}{\operatorname{length}\left(\htmlData{mx=51}{\htmlData{mx=40}{\operatorname{filter}}(\htmlData{mx=50}{o \mapsto \htmlData{mx=49}{\htmlData{mx=47}{\operatorname{owned}\left(\htmlData{mx=46}{\htmlData{mx=44}{\mathit{offers}}(\htmlData{mx=45}{o})}\right)}(\htmlData{mx=48}{i})}})}\right)} \mathrel{\htmlData{mx=53}{\leq}} 1} \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)
⟹Implies: If Nat, then Offer(α). (Between types, A → B is the type of functions from A to B.) (Nat → Offer α)
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)
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)
=Equality: evalRefusing(assembleSelect(k), offers, t) and some(result) are the same. (evalRefusing (assembleSelect k) offers …)
∧And: Both hold: ∀ i, owned(i) = true ↔ (∃ o, owned(offers(o))(i) = true), and ∀ i, i < k → length(filter(o ↦ owned(offers(o))(i))) ≤ 1. ((∀ i, result.owned i = true ↔ ∃ o ∈ t.l…)
∀For all: The statement after the comma holds for every i. (∀ i, result.owned i = true ↔ ∃ o ∈ t.le…)
Offer: Offer: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Offer)
f(x)Function application: Offer applied to α. Lean writes f x; papers write f(x). (Offer α)
e.fowned: owned of result: Lean's dot notation e.owned means owned applied to e. (result.owned)
⟺If and only if: owned(i) = true holds exactly when ∃ o, owned(offers(o))(i) = true holds. (result.owned i = true ↔ ∃ o ∈ t.leaves,…)
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)
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)
∃There exists: At least one o makes the statement after the comma true. (∃ o ∈ t.leaves, (offers o).owned i = tr…)
e.fleaves: leaves of t: Lean's dot notation e.leaves means leaves applied to e. (t.leaves)
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)
<Less than: i is strictly smaller than k. (i < k)
e.flength: length of filter(o ↦ owned(offers(o))(i)): Lean's dot notation e.length means length applied to e. ((t.leaves.filter (fun o => (offers o).o…)
≤At most: length(filter(o ↦ owned(offers(o))(i))) is less than or equal to 1. ((t.leaves.filter (fun o => (offers o).o…)
filter: t.leaves.filter: 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.filter)
x ↦ f(x)Function (λ-abstraction): The function sending o to owned(offers(o))(i). Lean writes fun x => …; papers write x ↦ …. (fun o => (offers o).owned i)

theorem alpha-assembly-refuses-overlap-and-uncovered {α : Type} (k : Nat) (offers : Nat → Offer α) (t : CombineTree) (result : Offer α) (h : evalRefusing (assembleSelect k) offers t = some result) :
    (∀ i, result.owned i = true ↔ ∃ o ∈ t.leaves, (offers o).owned i = true) ∧ ∀ i, i < k → (t.leaves.filter (fun o => (offers o).owned i)).length ≤ 1

Whenever the selection combine succeeds, a coordinate is marked owned exactly when some leaf owns it (so a coordinate nobody owns stays unmarked and the coverage check refuses), and no coordinate below k has two owners among the leaves (two owners refuse: data-parallel-assembly-overlap). 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: Classical.choice, Quot.sound, propext
Proof: 85 lines of Lean

Assembly records only actual owners and refuses two owners

How it was proved

More proved statements