proofs
Provedalphamulti-device-learningordered-combine

Alpha's hierarchy combine shapes

combineHierarchy⁡(2,5)=.(branch⁡,0,.(branch⁡,0,.(leaf⁡,0),.(branch⁡,1,.(leaf⁡,1),.(leaf⁡,2))),.(branch⁡,3,.(leaf⁡,3),.(leaf⁡,4)))∧combineHierarchy⁡(2,7)=.(branch⁡,0,.(branch⁡,0,.(leaf⁡,0),.(branch⁡,1,.(branch⁡,1,.(leaf⁡,1),.(leaf⁡,2)),.(leaf⁡,3))),.(branch⁡,4,.(branch⁡,4,.(leaf⁡,4),.(leaf⁡,5)),.(leaf⁡,6)))∧combineHierarchy⁡(1,3)=.(branch⁡,0,.(leaf⁡,0),.(branch⁡,1,.(leaf⁡,1),.(leaf⁡,2)))∧combineHierarchy⁡(2,1)=.(leaf⁡,0)\begin{aligned} & \htmlData{mx=3}{\htmlData{mx=2}{\operatorname{combineHierarchy}}(2, 5)} \\ & \quad \htmlData{mx=1}{=} \htmlData{mx=21}{\mathtt{.}(\htmlData{mx=4}{\operatorname{branch}}, 0, \htmlData{mx=14}{\mathtt{.}(\htmlData{mx=5}{\operatorname{branch}}, 0, \htmlData{mx=7}{\mathtt{.}(\htmlData{mx=6}{\operatorname{leaf}}, 0)}, \htmlData{mx=13}{\mathtt{.}(\htmlData{mx=8}{\operatorname{branch}}, 1, \htmlData{mx=10}{\mathtt{.}(\htmlData{mx=9}{\operatorname{leaf}}, 1)}, \htmlData{mx=12}{\mathtt{.}(\htmlData{mx=11}{\operatorname{leaf}}, 2)})})}, \htmlData{mx=20}{\mathtt{.}(\htmlData{mx=15}{\operatorname{branch}}, 3, \htmlData{mx=17}{\mathtt{.}(\htmlData{mx=16}{\operatorname{leaf}}, 3)}, \htmlData{mx=19}{\mathtt{.}(\htmlData{mx=18}{\operatorname{leaf}}, 4)})})} \\ & \htmlData{mx=0}{\land} \htmlData{mx=24}{\htmlData{mx=23}{\operatorname{combineHierarchy}}(2, 7)} \\ & \quad \htmlData{mx=22}{=} \htmlData{mx=50}{\mathtt{.}(\htmlData{mx=25}{\operatorname{branch}}, 0, \htmlData{mx=39}{\mathtt{.}(\htmlData{mx=26}{\operatorname{branch}}, 0, \htmlData{mx=28}{\mathtt{.}(\htmlData{mx=27}{\operatorname{leaf}}, 0)}, \htmlData{mx=38}{\mathtt{.}(\htmlData{mx=29}{\operatorname{branch}}, 1, \htmlData{mx=35}{\mathtt{.}(\htmlData{mx=30}{\operatorname{branch}}, 1, \htmlData{mx=32}{\mathtt{.}(\htmlData{mx=31}{\operatorname{leaf}}, 1)}, \htmlData{mx=34}{\mathtt{.}(\htmlData{mx=33}{\operatorname{leaf}}, 2)})}, \htmlData{mx=37}{\mathtt{.}(\htmlData{mx=36}{\operatorname{leaf}}, 3)})})}, \htmlData{mx=49}{\mathtt{.}(\htmlData{mx=40}{\operatorname{branch}}, 4, \htmlData{mx=46}{\mathtt{.}(\htmlData{mx=41}{\operatorname{branch}}, 4, \htmlData{mx=43}{\mathtt{.}(\htmlData{mx=42}{\operatorname{leaf}}, 4)}, \htmlData{mx=45}{\mathtt{.}(\htmlData{mx=44}{\operatorname{leaf}}, 5)})}, \htmlData{mx=48}{\mathtt{.}(\htmlData{mx=47}{\operatorname{leaf}}, 6)})})} \\ & \htmlData{mx=0}{\land} \htmlData{mx=53}{\htmlData{mx=52}{\operatorname{combineHierarchy}}(1, 3)} \\ & \quad \htmlData{mx=51}{=} \htmlData{mx=63}{\mathtt{.}(\htmlData{mx=54}{\operatorname{branch}}, 0, \htmlData{mx=56}{\mathtt{.}(\htmlData{mx=55}{\operatorname{leaf}}, 0)}, \htmlData{mx=62}{\mathtt{.}(\htmlData{mx=57}{\operatorname{branch}}, 1, \htmlData{mx=59}{\mathtt{.}(\htmlData{mx=58}{\operatorname{leaf}}, 1)}, \htmlData{mx=61}{\mathtt{.}(\htmlData{mx=60}{\operatorname{leaf}}, 2)})})} \\ & \htmlData{mx=0}{\land} \htmlData{mx=65}{\htmlData{mx=64}{\operatorname{combineHierarchy}}(2, 1)} \mathrel{\htmlData{mx=68}{=}} \htmlData{mx=67}{\mathtt{.}(\htmlData{mx=66}{\operatorname{leaf}}, 0)} \end{aligned}
What the notation means · or point at any symbol
combineHierarchy
combineHierarchy: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (combineHierarchy)
f(x)Function application
combineHierarchy applied to 2, 5. Lean writes f x; papers write f(x). (combineHierarchy 2 5)
=Equality
combineHierarchy(2, 5) and .(branch, 0, .(branch, 0, .(leaf, 0), .(branch, 1, .(leaf,… are the same. (combineHierarchy 2 5 = .branch 0 (.bran…)
branch
branch: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (branch)
leaf
leaf: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (leaf)
∧And
Both hold: combineHierarchy(1, 3) = .(branch, 0, .(leaf, 0), .(branch…, and combineHierarchy(2, 1) = .(leaf, 0). (combineHierarchy 1 3 = .branch 0 (.leaf…)

The laws of NativeCombineHierarchyLaws: five owners at fan-out two are (l0 + (l1 + l2)) + (l3 + l4); seven owners have children 1 (roles 1..3) and 4 (roles 4..6); fan-out one over three owners is l0 + (l1 + l2); one owner is its own leaf. 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
25 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements