Preview Runtime Showcase

Blueprint Summary🔗

Overview
Total entries58completed: 26; deps incomplete: 1; sorries: 7; no proof: 17
Ready now10Entries whose next formalization step is currently unblocked.
Fully closed26Local code and prerequisite closure are both complete.
Actionable priorities5Entries ready now and already unlocking downstream work.
Current blockers9Missing external or incomplete Lean declarations.
Missing informal coverage11Entries with Lean code but missing an informal statement or proof block.
Ready next (5)
  • custom_client_external_markdown_metadata(Theorem)
    Ready for proof work.
    effort: smallpriority: mediumtag: externaltag: markdownstage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: ready to formalize
  • used_aux_target(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 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 (9)
Missing informal coverage (11)
Entry index (58)
Definitions29completed: 20; deps incomplete: 0; sorries: 3; no proof: 0
Lemmas10completed: 0; deps incomplete: 0; sorries: 0; no proof: 10
Theorems19completed: 6; deps incomplete: 1; sorries: 4; no proof: 7
Axiom-like entries2completed: 0; deps incomplete: 0; sorries: 2; no proof: 0
Informal-only entries21
Definition Index (29)
Theorem / Proposition / Lemma / Corollary Index (29)
By parent groups (3)
Preview group title. (2)
Preview relation group. (2)
Core statements that drive the showcase summary and dependency graph. (2)
Axiom-like Index (2)
Dependency insights
Statement-used entries9Entries reused in statement dependencies.
Proof-used entries2Entries reused in proof-only dependencies.
Tracked parent groups3Grouped health rollups for parents with more than one child entry.
Most used in statements (9)
  • used_target(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 3direct uses: 5downstream unlocks: 7
    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
  • custom_client_external_markdown_metadata(Theorem)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  • 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
  • used_grouped_proof_panel(Theorem)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    Associated lean decls (1)
Most used in proofs (2)
  • used_target(Definition)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 3statement uses: 2direct uses: 5downstream unlocks: 7
    Associated lean decls (1)
  • used_aux_target(Definition)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 3
Group health (3)
  • 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
  • Preview relation group.preview_relation_group
    Grouped view over entries sharing the same parent.
    total: 2closed: 0local-only: 1ready: 1blocked: 0incomplete Lean: 0unlock score: 1
    Next: no ready child currently unlocks downstream work.
Metadata
Tags in use2Distinct tags currently attached to blueprint entries.
Tag rollups (2)
  • tag: external
    entries: 1actionable: 1quick wins: 0linked PRs: 0
  • tag: markdown
    entries: 1actionable: 1quick wins: 0linked PRs: 0
Metadata audit
Missing owner58
Missing effort57
Untagged57
Missing owner (58)
Missing effort (57)
Untagged (57)
Structure and coverage
Informal-only21Statements with no associated Lean code yet.
Ready to formalize10Entries whose next step is currently unblocked.
Formalized, ancestors open1Local Lean work is done, but prerequisite closure is still open.
Fully closed26Local code and ancestor closure are both complete.
Heaviest prerequisites (12)
  • used_grouped_proof_panel(Theorem)
    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)
  • used_proof_panel(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 0proof deps: 2direct uses: 0downstream unlocks: 0
  • 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
  • custom_client_external_markdown_metadata(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  • custom_client_external_metadata_consumer(Lemma)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct 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
  • Show all 2 more heaviest-prerequisite entries
    • used_grouped_consumer(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
    • 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 (46)
No dependents (48)