proofs
Provedalphamulti-device-learningparticipant-tree

A hierarchy node's children tile its descendants

For all fanout,role,size∈N\htmlData{mx=1}{\mathit{fanout}, \mathit{role}, \mathit{size} \in \htmlData{mx=0}{\mathbb{N}}}, if 0<treeChildCount⁡(fanout,size)0 \mathrel{\htmlData{mx=4}{<}} \htmlData{mx=3}{\htmlData{mx=0}{\operatorname{treeChildCount}}(\htmlData{mx=1}{\mathit{fanout}}, \htmlData{mx=2}{\mathit{size}})}, then

treeChildCount⁡(fanout,size)≤fanout∧treeChildStart⁡(fanout,role,size,0)=role+1∧(∀i,treeChildStart⁡(fanout,role,size,i+1)=treeChildStart⁡(fanout,role,size,i)+treeChildSize⁡(fanout,size,i))∧treeChildStart⁡(fanout,role,size,treeChildCount⁡(fanout,size))=role+size\begin{aligned} & \htmlData{mx=4}{\htmlData{mx=1}{\operatorname{treeChildCount}}(\htmlData{mx=2}{\mathit{fanout}}, \htmlData{mx=3}{\mathit{size}})} \mathrel{\htmlData{mx=6}{\leq}} \htmlData{mx=5}{\mathit{fanout}} \\ & \htmlData{mx=0}{\land} \htmlData{mx=11}{\htmlData{mx=7}{\operatorname{treeChildStart}}(\htmlData{mx=8}{\mathit{fanout}}, \htmlData{mx=9}{\mathit{role}}, \htmlData{mx=10}{\mathit{size}}, 0)} \mathrel{\htmlData{mx=14}{=}} \htmlData{mx=13}{\htmlData{mx=12}{\mathit{role}} + 1} \\ & \htmlData{mx=0}{\land} \left(\right. \htmlData{mx=15}{\forall} i, \\ & \quad \htmlData{mx=23}{\htmlData{mx=17}{\operatorname{treeChildStart}}(\htmlData{mx=18}{\mathit{fanout}}, \htmlData{mx=19}{\mathit{role}}, \htmlData{mx=20}{\mathit{size}}, \htmlData{mx=22}{\htmlData{mx=21}{i} + 1})} \\ & \quad \quad \htmlData{mx=16}{=} \htmlData{mx=35}{\htmlData{mx=29}{\htmlData{mx=24}{\operatorname{treeChildStart}}(\htmlData{mx=25}{\mathit{fanout}}, \htmlData{mx=26}{\mathit{role}}, \htmlData{mx=27}{\mathit{size}}, \htmlData{mx=28}{i})} + \htmlData{mx=34}{\htmlData{mx=30}{\operatorname{treeChildSize}}(\htmlData{mx=31}{\mathit{fanout}}, \htmlData{mx=32}{\mathit{size}}, \htmlData{mx=33}{i})}} \left.\right) \\ & \htmlData{mx=0}{\land} \htmlData{mx=45}{\htmlData{mx=37}{\operatorname{treeChildStart}}(\htmlData{mx=38}{\mathit{fanout}}, \htmlData{mx=39}{\mathit{role}}, \htmlData{mx=40}{\mathit{size}}, \htmlData{mx=44}{\htmlData{mx=41}{\operatorname{treeChildCount}}(\htmlData{mx=42}{\mathit{fanout}}, \htmlData{mx=43}{\mathit{size}})})} \\ & \quad \htmlData{mx=36}{=} \htmlData{mx=48}{\htmlData{mx=46}{\mathit{role}} + \htmlData{mx=47}{\mathit{size}}} \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
fanout, role, size range over natural numbers: the statement must hold for every choice. ((fanout role size : Nat))
<Less than
0 is strictly smaller than treeChildCount(fanout, size). (0 < treeChildCount fanout size)
≤At most
treeChildCount(fanout, size) is less than or equal to fanout. (treeChildCount fanout size ≤ fanout)
treeChildCount
treeChildCount: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (treeChildCount)
f(x)Function application
treeChildCount applied to fanout, size. Lean writes f x; papers write f(x). (treeChildCount fanout size)
treeChildStart
treeChildStart: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (treeChildStart)
=Equality
treeChildStart(fanout, role, size, 0) and role + 1 are the same. (treeChildStart fanout role size 0 = rol…)
+Addition
role plus 1. (role + 1)
∧And
Both hold: ∀ i, treeChildStart(fanout, role, size, i + 1) = treeChild…, and treeChildStart(fanout, role, size, treeChildCount(fanout, …. ((∀ i, treeChildStart fanout role size (…)
∀For all
The statement after the comma holds for every i. (∀ i, treeChildStart fanout role size (i…)
treeChildSize
treeChildSize: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (treeChildSize)

A node has at most fanout children; the first starts right after the node, each starts where the previous ends, and the last ends where the node's preorder range ends, so a parent certifies coverage with O(fanout) checks (Representation.ParticipantTree). 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
34 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements