Each box is a declaration whose docstring refers to a result in the paper. Arrows point from a lemma to the results whose proof uses it, so the two main theorems are at the top. Click a box to see the paper reference, the statement in Lean (proof hidden), and its dependencies among the displayed results. Edges follow compiled constant references through helpers; the elaborated types include every inherited hypothesis.
Section 5 (Theorems 3.4, 5.1) Lemma 4.7 / Prop. 4.8 ground state (Remark 2.3) other lemmas
Full catalog of all statements: STATEMENTS.html.