Blueprint Preview Wiring

Blueprint Summary🔗

Overview
Total entries2completed: 0; deps incomplete: 0; sorries: 0; no proof: 1
Ready now0Entries whose next formalization step is currently unblocked.
Fully closed0Local code and prerequisite closure are both complete.
Actionable priorities1Entries ready now and already unlocking downstream work.
Ready next (1)
  • «def:preview.base»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
Entry index (2)
Definitions1completed: 0; deps incomplete: 0; sorries: 0; no proof: 0
Lemmas1completed: 0; deps incomplete: 0; sorries: 0; no proof: 1
Informal-only entries2
Definition Index (1)
Theorem / Lemma / Corollary Index (1)
Dependency insights
Statement-used entries1Entries reused in statement dependencies.
Most used in statements (1)
  • «def:preview.base»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Metadata
Metadata audit
Missing owner2
Missing effort2
Untagged2
Missing owner (2)
Missing effort (2)
Untagged (2)
Structure and coverage
Informal-only2Statements with no associated Lean code yet.
Heaviest prerequisites (1)
  • «lem:preview.next»(Lemma)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
No prerequisites (1)
No dependents (1)