Blueprint Summary
Overview
Total entries10completed: 9; deps incomplete: 0; sorries: 0; no proof: 1
Ready now0Entries whose next formalization step is currently unblocked.
Fully closed9Local code and prerequisite closure are both complete.
Actionable priorities0Entries ready now and already unlocking downstream work.
Missing informal coverage5Entries with Lean code but missing an informal statement or proof block.
Missing informal coverage (5)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
Entry index (10)
Definitions2completed: 2; deps incomplete: 0; sorries: 0; no proof: 0
Theorems8completed: 7; deps incomplete: 0; sorries: 0; no proof: 1
Informal-only entries1
Definition Index (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
Theorem / Proposition / Lemma / Corollary Index (8)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
Dependency insights
Statement-used entries6Entries reused in statement dependencies.
Proof-used entries2Entries reused in proof-only dependencies.
Most used in statements (6)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
Most used in proofs (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 4
Associated lean decls (1)
Metadata
Metadata audit
Missing owner10
Missing effort10
Untagged10
Missing owner (10)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Missing effort (10)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Untagged (10)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Structure and coverage
Informal-only1Statements with no associated Lean code yet.
Fully closed9Local code and ancestor closure are both complete.
Heaviest prerequisites (6)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
No prerequisites (4)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
No dependents (3)
-
Associated lean decls (1)
-
Associated lean decls (1)