External Markup Source Showcase

Blueprint Summary🔗

Overview
Total entries18completed: 9; deps incomplete: 0; sorries: 0; no proof: 9
Ready now6Entries whose next formalization step is currently unblocked.
Fully closed9Local code and prerequisite closure are both complete.
Actionable priorities0Entries ready now and already unlocking downstream work.
Missing informal coverage7Entries with Lean code but missing an informal statement or proof block.
Missing informal coverage (7)
Entry index (18)
Definitions2completed: 2; deps incomplete: 0; sorries: 0; no proof: 0
Lemmas6completed: 0; deps incomplete: 0; sorries: 0; no proof: 6
Theorems10completed: 7; deps incomplete: 0; sorries: 0; no proof: 3
Informal-only entries3
Definition Index (2)
Theorem / Proposition / Lemma / Corollary Index (16)
Dependency insights
Statement-used entries1Entries reused in statement dependencies.
Most used in statements (1)
Metadata
Tags in use10Distinct tags currently attached to blueprint entries.
Tag rollups (10)
  • tag: external-source
    entries: 7actionable: 0quick wins: 0linked PRs: 0
  • tag: bodyless
    entries: 4actionable: 0quick wins: 0linked PRs: 0
  • tag: markdown-only
    entries: 2actionable: 0quick wins: 0linked PRs: 0
  • tag: mixed-markup
    entries: 2actionable: 0quick wins: 0linked PRs: 0
  • tag: native-body
    entries: 2actionable: 0quick wins: 0linked PRs: 0
  • tag: multi-page
    entries: 1actionable: 0quick wins: 0linked PRs: 0
  • tag: raw-label
    entries: 1actionable: 0quick wins: 0linked PRs: 0
  • tag: reviewed
    entries: 1actionable: 0quick wins: 0linked PRs: 0
  • tag: selected-markdown
    entries: 1actionable: 0quick wins: 0linked PRs: 0
  • tag: tex-only
    entries: 1actionable: 0quick wins: 0linked PRs: 0
Metadata audit
Missing owner18
Missing effort18
Untagged11
Missing owner (18)
  • «Chapter4:Theorem4.2.1»(Theorem)
    Missing owner metadata.
    Associated lean decls (1)
    • Nat.add
  • «ImportedPaper:Definition2.3»(Definition)
    Missing owner metadata.
    tag: external-sourcetag: tex-onlytag: bodyless
    Associated lean decls (1)
  • «ImportedPaper:Proposition2.4»(Theorem)
    Missing owner metadata.
    tag: external-sourcetag: multi-pagetag: bodyless
    Associated lean decls (2)
  • «ImportedPaper:Theorem2.1.SelectedMarkdown»(Theorem)
    Missing owner metadata.
    tag: external-sourcetag: mixed-markuptag: selected-markdowntag: bodyless
    Associated lean decls (1)
  • «ImportedPaper:Theorem2.1»(Theorem)
    Missing owner metadata.
    tag: external-sourcetag: markdown-onlytag: bodyless
    Associated lean decls (2)
  • «ImportedPaper:Theorem2.2»(Theorem)
    Missing owner metadata.
    tag: external-sourcetag: markdown-onlytag: raw-label
    Associated lean decls (1)
  • «external.bodyless.lean»(Theorem)
    Missing owner metadata.
    Associated lean decls (2)
    • Nat.add
    • Nat.mul
  • «external.duplicate»(Lemma)
    Missing owner metadata.
  • «external.markdown.witness»(Lemma)
    Missing owner metadata.
  • «external.markup»(Theorem)
    Missing owner metadata.
  • Show all 8 more entries missing owner
    • «external.multi»(Lemma)
      Missing owner metadata.
    • «external.sourced.witness»(Theorem)
      Missing owner metadata.
    • «external.source»(Lemma)
      Missing owner metadata.
    • «external.summary»(Lemma)
      Missing owner metadata.
    • «external.unlabeled.anchor»(Theorem)
      Missing owner metadata.
    • «external.witness»(Lemma)
      Missing owner metadata.
    • «showcase.native.rewrite»(Theorem)
      Missing owner metadata.
      tag: external-sourcetag: native-bodytag: reviewed
      Associated lean decls (1)
    • «showcase.visible.attachments»(Definition)
      Missing owner metadata.
      tag: external-sourcetag: mixed-markuptag: native-body
      Associated lean decls (1)
Missing effort (18)
  • «Chapter4:Theorem4.2.1»(Theorem)
    Missing effort metadata.
    Associated lean decls (1)
    • Nat.add
  • «ImportedPaper:Definition2.3»(Definition)
    Missing effort metadata.
    tag: external-sourcetag: tex-onlytag: bodyless
    Associated lean decls (1)
  • «ImportedPaper:Proposition2.4»(Theorem)
    Missing effort metadata.
    tag: external-sourcetag: multi-pagetag: bodyless
    Associated lean decls (2)
  • «ImportedPaper:Theorem2.1.SelectedMarkdown»(Theorem)
    Missing effort metadata.
    tag: external-sourcetag: mixed-markuptag: selected-markdowntag: bodyless
    Associated lean decls (1)
  • «ImportedPaper:Theorem2.1»(Theorem)
    Missing effort metadata.
    tag: external-sourcetag: markdown-onlytag: bodyless
    Associated lean decls (2)
  • «ImportedPaper:Theorem2.2»(Theorem)
    Missing effort metadata.
    tag: external-sourcetag: markdown-onlytag: raw-label
    Associated lean decls (1)
  • «external.bodyless.lean»(Theorem)
    Missing effort metadata.
    Associated lean decls (2)
    • Nat.add
    • Nat.mul
  • «external.duplicate»(Lemma)
    Missing effort metadata.
  • «external.markdown.witness»(Lemma)
    Missing effort metadata.
  • «external.markup»(Theorem)
    Missing effort metadata.
  • Show all 8 more entries missing effort
    • «external.multi»(Lemma)
      Missing effort metadata.
    • «external.sourced.witness»(Theorem)
      Missing effort metadata.
    • «external.source»(Lemma)
      Missing effort metadata.
    • «external.summary»(Lemma)
      Missing effort metadata.
    • «external.unlabeled.anchor»(Theorem)
      Missing effort metadata.
    • «external.witness»(Lemma)
      Missing effort metadata.
    • «showcase.native.rewrite»(Theorem)
      Missing effort metadata.
      tag: external-sourcetag: native-bodytag: reviewed
      Associated lean decls (1)
    • «showcase.visible.attachments»(Definition)
      Missing effort metadata.
      tag: external-sourcetag: mixed-markuptag: native-body
      Associated lean decls (1)
Untagged (11)
  • «Chapter4:Theorem4.2.1»(Theorem)
    Missing tag metadata.
    Associated lean decls (1)
    • Nat.add
  • «external.bodyless.lean»(Theorem)
    Missing tag metadata.
    Associated lean decls (2)
    • Nat.add
    • Nat.mul
  • «external.duplicate»(Lemma)
    Missing tag metadata.
  • «external.markdown.witness»(Lemma)
    Missing tag metadata.
  • «external.markup»(Theorem)
    Missing tag metadata.
  • «external.multi»(Lemma)
    Missing tag metadata.
  • «external.sourced.witness»(Theorem)
    Missing tag metadata.
  • «external.source»(Lemma)
    Missing tag metadata.
  • «external.summary»(Lemma)
    Missing tag metadata.
  • «external.unlabeled.anchor»(Theorem)
    Missing tag metadata.
  • Show all 1 more untagged entries
    • «external.witness»(Lemma)
      Missing tag metadata.
Structure and coverage
Informal-only3Statements with no associated Lean code yet.
Ready to formalize6Entries whose next step is currently unblocked.
Fully closed9Local code and ancestor closure are both complete.
Heaviest prerequisites (2)
  • «ImportedPaper:Proposition2.4»(Theorem)
    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 (2)
  • «showcase.native.rewrite»(Theorem)
    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)
No prerequisites (16)
No dependents (17)