Preview Runtime Showcase

Blueprint Summary🔗

Overview
Total entries30completed: 8; deps incomplete: 0; sorries: 5; no proof: 12
Ready now6Entries whose next formalization step is currently unblocked.
Fully closed8Local code and prerequisite closure are both complete.
Actionable priorities3Entries ready now and already unlocking downstream work.
Current blockers6Missing external or incomplete Lean declarations.
Missing informal coverage4Entries with Lean code but missing an informal statement or proof block.
Ready next (3)
  • nested_inner(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 2
  • preview_base(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 2
  • group_target(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
Current blockers (6)
Missing informal coverage (4)
Entry index (30)
Definitions14completed: 6; deps incomplete: 0; sorries: 3; no proof: 0
Lemmas7completed: 0; deps incomplete: 0; sorries: 0; no proof: 7
Theorems9completed: 2; deps incomplete: 0; sorries: 2; no proof: 5
Axiom-like entries2completed: 0; deps incomplete: 0; sorries: 2; no proof: 0
Informal-only entries16
Definition Index (14)
Theorem / Lemma / Corollary Index (16)
By parent groups (2)
Preview group title. (2)
Core statements that drive the showcase summary and dependency graph. (2)
Axiom-like Index (2)
Dependency insights
Statement-used entries7Entries reused in statement dependencies.
Proof-used entries1Entries reused in proof-only dependencies.
Tracked parent groups2Grouped health rollups for parents with more than one child entry.
Most used in statements (7)
  • used_target(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 2
    Associated lean decls (1)
  • nested_inner(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  • preview_base(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  • group_target(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  • lean_code_preview(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    Associated lean decls (1)
  • nested_outer(Theorem)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  • preview_next(Lemma)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Most used in proofs (1)
  • used_target(Definition)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 2
    Associated lean decls (1)
Group health (2)
  • Preview group title.preview_group
    Grouped view over entries sharing the same parent.
    total: 3closed: 0local-only: 0ready: 3blocked: 0incomplete Lean: 0unlock score: 1
    Next: group_target stage: statementdownstream unlocks: 1
  • Core statements that drive the showcase summary and dependency graph.preview_core
    Grouped view over entries sharing the same parent.
    total: 4closed: 1local-only: 0ready: 1blocked: 2incomplete Lean: 0unlock score: 4
    Next: preview_base stage: statementdownstream unlocks: 2
Metadata
Metadata audit
Missing owner30
Missing effort30
Untagged30
Missing owner (30)
Missing effort (30)
Untagged (30)
Structure and coverage
Informal-only16Statements with no associated Lean code yet.
Ready to formalize6Entries whose next step is currently unblocked.
Fully closed8Local code and ancestor closure are both complete.
Heaviest prerequisites (7)
  • preview_final(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  • used_proof(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
  • group_user(Lemma)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  • nested_outer(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  • nested_user(Lemma)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  • preview_next(Lemma)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  • used_statement(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 (23)
No dependents (23)