Document

Blueprint Summary🔗

Overview
Total entries3completed: 3; deps incomplete: 0; sorries: 0; no proof: 0
Ready now0Entries with an actionable next formalization step.
Fully closed3Local code and prerequisite closure are both complete.
Actionable priorities0Entries ready now and already unlocking downstream work.
Missing informal coverage1Entries with Lean code but missing an informal statement or proof block.
Missing informal coverage (1)
Entry index (3)
Definitions1completed: 1; deps incomplete: 0; sorries: 0; no proof: 0
Lemmas1completed: 1; deps incomplete: 0; sorries: 0; no proof: 0
Theorems1completed: 1; deps incomplete: 0; sorries: 0; no proof: 0
Definition Index (1)
Theorem / Proposition / Lemma / Corollary Index (2)
Dependency insights
Statement-used entries1Entries reused in statement dependencies.
Proof-used entries2Entries reused in proof-only dependencies.
Most used in statements (1)
Most used in proofs (2)
Metadata
Owners in use1Distinct owners referenced by the current blueprint entries.
Tags in use3Distinct tags currently attached to blueprint entries.
Owner rollups (1)
  • Split Authorsplit_author
    entries: 1actionable: 0quick wins: 0linked PRs: 0
Tag rollups (3)
  • tag: late
    entries: 1actionable: 0quick wins: 0linked PRs: 0
  • tag: proof
    entries: 1actionable: 0quick wins: 0linked PRs: 0
  • tag: statement
    entries: 1actionable: 0quick wins: 0linked PRs: 0
Metadata audit
Missing owner2
Missing effort2
Untagged2
Missing owner (2)
Missing effort (2)
Untagged (2)
Structure and coverage
Fully closed3Local code and ancestor closure are both complete.
Heaviest prerequisites (1)
  • key_theorem(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 1proof deps: 2direct uses: 0downstream unlocks: 0
    Associated lean decls (1)
No prerequisites (2)
No dependents (1)