Preview Runtime Showcase

Blueprint Summary🔗

Overview
Total entries66completed: 30; deps incomplete: 1; sorries: 7; no proof: 20
Ready now25Entries with an actionable next formalization step.
Fully closed30Local 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 coverage12Entries with Lean code but missing an informal statement or proof block.
Actionable priorities (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 (12)
Entry index (66)
Definitions34completed: 24; deps incomplete: 0; sorries: 3; no proof: 0
Lemmas12completed: 0; deps incomplete: 0; sorries: 0; no proof: 12
Theorems20completed: 6; deps incomplete: 1; sorries: 4; no proof: 8
Axiom-like entries2completed: 0; deps incomplete: 0; sorries: 2; no proof: 0
Lean-only entries1
Informal-only entries24
Definition Index (34)
Theorem / Proposition / Lemma / Corollary Index (32)
By parent groups (4)
Preview group title. (2)
Prepared resource group. (1)
Preview relation group. (2)
Core statements that drive the showcase summary and dependency graph. (2)
Axiom-like Index (2)
Dependency insights
Statement-used entries13Entries reused in statement dependencies.
Proof-used entries2Entries reused in proof-only dependencies.
Tracked parent groups4Grouped health rollups for parents with more than one child entry.
Most used in statements (13)
  • used_target(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 3direct uses: 5downstream unlocks: 7
    Associated lean decls (1)
  • prepared_resource_blank(Theorem)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 4
  • prepared_resource_target(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 4
  • prepared_resource_single(Lemma)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  • 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
  • Show all 3 more statement-used entries
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 (4)
  • 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: used_grouped_consumer stage: proofdownstream unlocks: 0
  • Prepared resource group.prepared_resource_group
    Grouped view over entries sharing the same parent.
    total: 2closed: 0local-only: 0ready: 0blocked: 2incomplete Lean: 0unlock score: 8
    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 owner66
Missing effort65
Untagged65
Missing owner (66)
Missing effort (65)
Untagged (65)
Structure and coverage
Informal-only24Statements with no associated Lean code yet.
Ready to formalize25Entries with an actionable next formalization step.
Formalized, ancestors open1Local Lean work is done, but prerequisite closure is still open.
Fully closed30Local code and ancestor closure are both complete.
Blocked or incomplete10Entries not covered by the highlighted readiness buckets above.
Heaviest prerequisites (17)
  • 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
  • prepared_resource_multiple(Lemma)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 0direct 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
  • Show all 7 more heaviest-prerequisite entries
    • panel_docstring_source(Definition)
      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)
    • prepared_resource_blank(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 4
    • prepared_resource_single(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 4
    • prepared_resource_target(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 4
    • 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_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 (49)
No dependents (52)