Summary Triage

Blueprint Summary🔗

Overview
Total entries17completed: 1; deps incomplete: 0; sorries: 1; no proof: 2
Ready now2Entries whose next formalization step is currently unblocked.
Fully closed1Local code and prerequisite closure are both complete.
Actionable priorities12Entries ready now and already unlocking downstream work.
Current blockers2Missing external or incomplete Lean declarations.
Quick wins1Actionable entries with `high` priority and `small` effort.
Ready next (12)
  • «def:triage.12»(Definition)
    Ready for statement work.
    owner: Bob Exampleeffort: smallpriority: hightag: criticaltag: quick-winstage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
    Links: PR
  • «def:triage.01»(Definition)
    Ready for statement work.
    owner: Alice Exampleeffort: smallpriority: lowtag: foundationtag: localstage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 2
    Links: PR
  • «def:triage.02»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 2
  • «def:triage.03»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
  • «def:triage.04»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
  • «def:triage.05»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
  • «def:triage.06»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
  • «def:triage.07»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
  • «def:triage.08»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
  • «def:triage.09»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
  • Show all 2 more priorities
    • «def:triage.10»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
    • «def:triage.11»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
Current blockers (2)
  • «def:blocker.missing»(Definition)
    Missing external Lean declaration: Nat.nope [missing declaration]
  • «def:blocker.sorry»(Definition)
    Declaration with sorry: Verso.VersoBlueprintTests.BlueprintSummaryLinks.Shared.summaryBlockerSorry [theorem/lemma; contains sorry; in proof; refs: 1]
Entry index (17)
Definitions15completed: 1; deps incomplete: 0; sorries: 1; no proof: 0
Theorems2completed: 0; deps incomplete: 0; sorries: 0; no proof: 2
Informal-only entries14
Definition Index (15)
Theorem / Lemma / Corollary Index (2)
By parent groups (1)
Triage group heading. (2)
Dependency insights
Statement-used entries12Entries reused in statement dependencies.
Proof-used entries2Entries reused in proof-only dependencies.
Tracked parent groups1Grouped health rollups for parents with more than one child entry.
Most used in statements (12)
  • «def:triage.01»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 2
  • «def:triage.02»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 2
  • «def:triage.03»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  • «def:triage.04»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  • «def:triage.05»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  • «def:triage.06»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  • «def:triage.07»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  • «def:triage.08»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  • «def:triage.09»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  • «def:triage.10»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  • Show all 2 more statement-used entries
    • «def:triage.11»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «def:triage.12»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Most used in proofs (2)
  • «def:triage.01»(Definition)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 2
  • «def:triage.02»(Definition)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 2
Group health (1)
  • Triage group heading.«triage.group»
    Grouped view over entries sharing the same parent.
    total: 14closed: 0local-only: 0ready: 13blocked: 1incomplete Lean: 0unlock score: 14
    Next: «def:triage.12» priority: highstage: statementdownstream unlocks: 1
Metadata
Quick wins1Actionable entries with `high` priority and `small` effort.
Owners in use2Distinct owners referenced by the current blueprint entries.
Tags in use4Distinct tags currently attached to blueprint entries.
Linked PRs2Entries already linked to a review URL.
Quick wins (1)
  • «def:triage.12»(Definition)
    Ready for statement work.
    owner: Bob Exampleeffort: smallpriority: hightag: criticaltag: quick-winstage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
    Links: PR
Owner rollups (2)
  • Bob Examplebob
    entries: 1actionable: 1quick wins: 1linked PRs: 1
  • Alice Examplealice
    entries: 2actionable: 1quick wins: 0linked PRs: 1
Tag rollups (4)
  • tag: critical
    entries: 2actionable: 1quick wins: 1linked PRs: 1
  • tag: quick-win
    entries: 1actionable: 1quick wins: 1linked PRs: 1
  • tag: foundation
    entries: 1actionable: 1quick wins: 0linked PRs: 1
  • tag: local
    entries: 1actionable: 1quick wins: 0linked PRs: 1
Linked PRs (2)
  • «def:triage.01»(Definition)
    Entry already linked to a review PR.
    owner: Alice Exampleeffort: smallpriority: lowtag: foundationtag: local
    Links: PR
  • «def:triage.12»(Definition)
    Entry already linked to a review PR.
    owner: Bob Exampleeffort: smallpriority: hightag: criticaltag: quick-win
    Links: PR
Metadata audit
Missing owner14
Missing effort14
Untagged14
Missing owner (14)
  • «def:blocker.missing»(Definition)
    Missing owner metadata.
    Associated lean decls (1)
    • Nat.nope
  • «def:blocker.sorry»(Definition)
    Missing owner metadata.
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintSummaryLinks.Shared.summaryBlockerSorry
  • «def:external.summary»(Definition)
    Missing owner metadata.
    Associated lean decls (1)
    • Nat.add
  • «def:triage.02»(Definition)
    Missing owner metadata.
  • «def:triage.03»(Definition)
    Missing owner metadata.
  • «def:triage.04»(Definition)
    Missing owner metadata.
  • «def:triage.05»(Definition)
    Missing owner metadata.
  • «def:triage.06»(Definition)
    Missing owner metadata.
  • «def:triage.07»(Definition)
    Missing owner metadata.
  • «def:triage.08»(Definition)
    Missing owner metadata.
  • Show all 4 more entries missing owner
Missing effort (14)
  • «def:blocker.missing»(Definition)
    Missing effort metadata.
    Associated lean decls (1)
    • Nat.nope
  • «def:blocker.sorry»(Definition)
    Missing effort metadata.
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintSummaryLinks.Shared.summaryBlockerSorry
  • «def:external.summary»(Definition)
    Missing effort metadata.
    Associated lean decls (1)
    • Nat.add
  • «def:triage.02»(Definition)
    Missing effort metadata.
  • «def:triage.03»(Definition)
    Missing effort metadata.
  • «def:triage.04»(Definition)
    Missing effort metadata.
  • «def:triage.05»(Definition)
    Missing effort metadata.
  • «def:triage.06»(Definition)
    Missing effort metadata.
  • «def:triage.07»(Definition)
    Missing effort metadata.
  • «def:triage.08»(Definition)
    Missing effort metadata.
  • Show all 4 more entries missing effort
Untagged (14)
Structure and coverage
Informal-only14Statements with no associated Lean code yet.
Ready to formalize2Entries whose next step is currently unblocked.
Fully closed1Local code and ancestor closure are both complete.
Heaviest prerequisites (2)
  • «thm:triage.main»(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 12statement deps: 12proof deps: 0direct uses: 0downstream unlocks: 0
  • «thm:triage.proof»(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 0proof deps: 2direct uses: 0downstream unlocks: 0
No prerequisites (15)
No dependents (5)
  • «def:blocker.missing»(Definition)
    Associated lean decls (1)
    • Nat.nope
  • «def:external.summary»(Definition)
    Associated lean decls (1)
    • Nat.add
  • «thm:triage.main»(Theorem)
  • «def:blocker.sorry»(Definition)
    Associated lean decls (1)
    • Verso.VersoBlueprintTests.BlueprintSummaryLinks.Shared.summaryBlockerSorry
  • «thm:triage.proof»(Theorem)