proofs
Provedalphamulti-device-learningpartitioning

Alpha's per-owner state sizes

ownedStateBytes⁡(2,4,1,1,0)=40∧ownedStateBytes⁡(2,4,1,0,0)=48∧replicatedStateBytes⁡(2,2)=56∧ownedStateBytes⁡(2,4,2,1,2)=64∧ownedStateBytes⁡(2,4,2,0,2)=72∧replicatedStateBytes⁡(2,6)=88\begin{aligned} & \htmlData{mx=2}{\htmlData{mx=1}{\operatorname{ownedStateBytes}}(2, 4, 1, 1, 0)} \mathrel{\htmlData{mx=3}{=}} 40 \\ & \htmlData{mx=0}{\land} \htmlData{mx=5}{\htmlData{mx=4}{\operatorname{ownedStateBytes}}(2, 4, 1, 0, 0)} \mathrel{\htmlData{mx=6}{=}} 48 \\ & \htmlData{mx=0}{\land} \htmlData{mx=8}{\htmlData{mx=7}{\operatorname{replicatedStateBytes}}(2, 2)} \mathrel{\htmlData{mx=9}{=}} 56 \\ & \htmlData{mx=0}{\land} \htmlData{mx=11}{\htmlData{mx=10}{\operatorname{ownedStateBytes}}(2, 4, 2, 1, 2)} \mathrel{\htmlData{mx=12}{=}} 64 \\ & \htmlData{mx=0}{\land} \htmlData{mx=14}{\htmlData{mx=13}{\operatorname{ownedStateBytes}}(2, 4, 2, 0, 2)} \mathrel{\htmlData{mx=15}{=}} 72 \\ & \htmlData{mx=0}{\land} \htmlData{mx=17}{\htmlData{mx=16}{\operatorname{replicatedStateBytes}}(2, 6)} \mathrel{\htmlData{mx=18}{=}} 88 \end{aligned}
What the notation means · or point at any symbol
ownedStateBytes
ownedStateBytes: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (ownedStateBytes)
f(x)Function application
ownedStateBytes applied to 2, 4, 1, 1, 0. Lean writes f x; papers write f(x). (ownedStateBytes 2 4 1 1 0)
=Equality
ownedStateBytes(2, 4, 1, 1, 0) and 40 are the same. (ownedStateBytes 2 4 1 1 0 = 40)
replicatedStateBytes
replicatedStateBytes: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (replicatedStateBytes)
∧And
Both hold: ownedStateBytes(2, 4, 2, 0, 2) = 72, and replicatedStateBytes(2, 6) = 88. (ownedStateBytes 2 4 2 0 2 = 72 ∧ replic…)

The laws of DataParallelContract: one owner of four over two coordinates holds 40 bytes for partitioned momentum (48 with replicated parameters, 56 fully replicated) and 64 for partitioned Adam (72, 88). 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
None
Proof
22 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements