Blueprint Summary
Overview
Total entries1completed: 1; deps incomplete: 0; sorries: 0; no proof: 0
Ready now0Entries with an actionable next formalization step.
Fully closed1Local code and prerequisite closure are both complete.
Actionable priorities0Entries ready now and already unlocking downstream work.
Entry index (1)
Definitions1completed: 1; deps incomplete: 0; sorries: 0; no proof: 0
Definition Index (1)
-
Associated lean decls (1)
Metadata
Metadata audit
Missing owner1
Missing effort1
Untagged1
Missing owner (1)
-
Missing owner metadata.
Associated lean decls (1)
Missing effort (1)
-
Missing effort metadata.
Associated lean decls (1)
Untagged (1)
-
Missing tag metadata.
Associated lean decls (1)
Structure and coverage
Fully closed1Local code and ancestor closure are both complete.
No prerequisites (1)
-
Associated lean decls (1)
No dependents (1)
-
Associated lean decls (1)