9.6. Reading the dependency graph🔗

The graph page draws one node per labelled entry of the correspondence table and one arrow per declared dependency, pointing from prerequisite to dependent. Its edges are hand-declared at the granularity of nodes, so it is coarser than the kernel-level walk above and reviewed rather than measured; this section says what its edges and colours do and do not claim.

An edge records mathematical dependency as the formalization discharges it. Where the paper's proof cites a result whose formal counterpart took a different route, the edge points at the node carrying the formal content and the paper's own citation stays a plain link in the proof text, with the divergence in the register above. Two proofs in the body–pin chapter do this. The proof of Proposition 6.5 cites Corollary 5.4, whose ungrounded statement has no Lean counterpart, so its edge lands on the grounded height theorem that the corollary restates. And the paper closes Section 6.4 by invoking Asimow–Roth to pass from attained maximum rank to generic rigidity in the usual sense; that step belongs to Theorem 1.1, whose edge into the Euclidean equivalence carries it, and not to the assembly lemma, whose Lean form is the maximum-rank statement. The dependencies declared by the eight lean_-prefixed infrastructure nodes carry a technical intent, which keeps them apart from the paper's spine in the node panels. The prefix marks a node with no counterpart in the paper, and two nodes carrying it are not infrastructure: the Euclidean vocabulary and continuous rigidity state mathematics the formalization proves beyond the paper, so their edges are ordinary ones.

The colours come from upstream's coordination vocabulary, computed from the Lean anchors rather than from anything this blueprint asserts. A node fills dark, locally formalized + dependencies complete, exactly when its own anchors and those of every node it transitively depends on resolve, proved, in the pinned environment. Since the formalization is finished, the whole spine from the root theorem down renders that way. The exceptions are deliberate, the nodes with nothing to resolve: the strata chapter's scheme statements, Corollary 5.4, Asimow–Roth, and Theorem 1.1 itself, which carries no anchor on purpose — the anchor belongs to the formal statement, and the route between the two runs through the Euclidean equivalence, which does carry one.

One label on those informal nodes should not be read at face value. A node with no Lean code whose recorded prerequisites are all formalized is labelled ready to formalize, a phrase from the upstream tool's coordination vocabulary for formalizations still in progress. This one is finished, and the label on the Asimow–Roth node is a statement about its recorded prerequisites alone, not about the real cost of formalizing the rank formula and the measure-zero complement that node still states; the strata nodes are deliberately informal whatever their colour. Read ready to formalize here as: informal, with formalized prerequisites. The release line offers no per-node override for that label.