Provedalphamulti-device-learningpartitioning

Coordinate ownership i mod n fits every owner's state

For all $\htmlData{mx=1}{k, \mathit{owners} \in \htmlData{mx=0}{\mathbb{N}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\mathit{owners}}$ , then

\begin{aligned} & (\htmlData{mx=7}{\forall c,\ \htmlData{mx=4}{\htmlData{mx=1}{\operatorname{coordinateOwner}}(\htmlData{mx=2}{\mathit{owners}}, \htmlData{mx=3}{c})} \mathrel{\htmlData{mx=6}{<}} \htmlData{mx=5}{\mathit{owners}}}) \\ & \htmlData{mx=0}{\land} \left(\htmlData{mx=20}{\forall c,\ \htmlData{mx=8}{c} \mathrel{\htmlData{mx=10}{<}} \htmlData{mx=9}{k} \mathrel{\htmlData{mx=19}{\implies}} \htmlData{mx=13}{\frac{\htmlData{mx=11}{c}}{\htmlData{mx=12}{\mathit{owners}}}} \mathrel{\htmlData{mx=18}{<}} \htmlData{mx=17}{\htmlData{mx=14}{\operatorname{perOwner}}(\htmlData{mx=15}{k}, \htmlData{mx=16}{\mathit{owners}})}}\right) \\ & \htmlData{mx=0}{\land} \left(\right. \htmlData{mx=21}{\forall} c, d, \\ & \quad \htmlData{mx=26}{\htmlData{mx=23}{\operatorname{coordinateOwner}}(\htmlData{mx=24}{\mathit{owners}}, \htmlData{mx=25}{c})} \mathrel{\htmlData{mx=31}{=}} \htmlData{mx=30}{\htmlData{mx=27}{\operatorname{coordinateOwner}}(\htmlData{mx=28}{\mathit{owners}}, \htmlData{mx=29}{d})} \\ & \quad \htmlData{mx=22}{\implies} \htmlData{mx=34}{\frac{\htmlData{mx=32}{c}}{\htmlData{mx=33}{\mathit{owners}}}} \mathrel{\htmlData{mx=38}{=}} \htmlData{mx=37}{\frac{\htmlData{mx=35}{d}}{\htmlData{mx=36}{\mathit{owners}}}} \\ & \quad \htmlData{mx=22}{\implies} \htmlData{mx=39}{c} \mathrel{\htmlData{mx=41}{=}} \htmlData{mx=40}{d} \left.\right) \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: k, owners range over natural numbers: the statement must hold for every choice. ((k owners : Nat))
<Less than: 0 is strictly smaller than owners. (0 < owners)
∀For all: The statement after the comma holds for every c. (∀ c, coordinateOwner owners c < owners)
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)
f(x)Function application: coordinateOwner applied to owners, c. Lean writes f x; papers write f(x). (coordinateOwner owners c)
∧And: Both hold: ∀ c, c < k → c/owners < perOwner(k, owners), and ∀ c, d, coordinateOwner(owners, c) = coordinateOwner(owner…. ((∀ c, c < k → c / owners < perOwner k o…)
⟹Implies: If c < k, then c/owners < perOwner(k, owners). (Between types, A → B is the type of functions from A to B.) (c < k → c / owners < perOwner k owners)
a/bDivision: c divided by owners. In Lean, dividing by 0 gives 0. (c / owners)
perOwner: perOwner: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (perOwner)
=Equality: coordinateOwner(owners, c) and coordinateOwner(owners, d) are the same. (coordinateOwner owners c = coordinateOw…)

theorem alpha-coordinate-ownership-fits (k owners : Nat) (hn : 0 < owners) :
    (∀ c, coordinateOwner owners c < owners) ∧ (∀ c, c < k → c / owners < perOwner k owners) ∧ (∀ c d, coordinateOwner owners c = coordinateOwner owners d → c / owners = d / owners → c = d)

Every coordinate has an owner among the owners, its word index within the owner's state is below the per-owner capacity ceil(k / owners), and two coordinates of one owner never share a word. 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: 28 lines of Lean

Coordinate ownership i mod n fits every owner's state

How it was proved

More proved statements