Blueprint Summary
Overview
Total entries1completed: 1; deps incomplete: 0; sorries: 0; no proof: 0
Ready now0Entries whose next formalization step is currently unblocked.
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)