4. How to read the status🔗

Nodes that link a real declaration with (lean := "PropertyKindCalculus.…") report their proved status straight from the checked, sorry-free core. The nodes that link none are the authoring steps of the write once, correctly recipe: they say how a model is composed, and carry nothing to prove. The headline deliverables are tagged capstone, and the status summary at the end reports the current counts. The blueprint dependency graph drawn beside that summary is the graph of these nodes and their uses edges — a picture of this document, and not one of the graphs the calculus itself defines; those are named and kept apart in the capstone chapter, and every term of the calculus is fixed by the dictionary.