Blueprint Graph State Showcase

Blueprint Summary🔗

Overview
Total entries12completed: 3; deps incomplete: 1; sorries: 1; no proof: 4
Ready now2Entries whose next formalization step is currently unblocked.
Fully closed3Local code and prerequisite closure are both complete.
Actionable priorities1Entries ready now and already unlocking downstream work.
Current blockers2Missing external or incomplete Lean declarations.
Missing informal coverage4Entries with Lean code but missing an informal statement or proof block.
Ready next (1)
  • «def:showcase.ready»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 3downstream unlocks: 3
Current blockers (2)
Missing informal coverage (4)
Entry index (12)
Definitions5completed: 2; deps incomplete: 0; sorries: 0; no proof: 0
Lemmas2completed: 0; deps incomplete: 0; sorries: 0; no proof: 2
Theorems5completed: 1; deps incomplete: 1; sorries: 1; no proof: 2
Lean-only entries1
Informal-only entries6
Definition Index (5)
Theorem / Lemma / Corollary Index (7)
Dependency insights
Statement-used entries3Entries reused in statement dependencies.
Proof-used entries2Entries reused in proof-only dependencies.
Most used in statements (3)
  • «def:showcase.base»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 5proof uses: 1direct uses: 6downstream unlocks: 7
    Associated lean decls (1)
  • «def:showcase.ready»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 3
  • «def:showcase.lean_only»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintPreviewWiring.StateShowcase.previewShowcaseLeanOnly
Most used in proofs (2)
Metadata
Metadata audit
Missing owner12
Missing effort12
Untagged12
Missing owner (12)
Missing effort (12)
Untagged (12)
Structure and coverage
Informal-only6Statements with no associated Lean code yet.
Ready to formalize2Entries whose next step is currently unblocked.
Formalized, ancestors open1Local Lean work is done, but prerequisite closure is still open.
Fully closed3Local code and ancestor closure are both complete.
Heaviest prerequisites (9)
No prerequisites (3)
No dependents (9)