Multiple literate attachments

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 coverage2Entries with Lean code but missing an informal statement or proof block.
Missing informal coverage (2)
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 entries1Entries reused in proof-only dependencies.
Most used in statements (1)
Most used in proofs (1)
Metadata
Owners in use1Distinct owners referenced by the current blueprint entries.
Tags in use1Distinct tags currently attached to blueprint entries.
Owner rollups (1)
  • Split Authorsplit_author
    entries: 1actionable: 0quick wins: 0linked PRs: 0
Tag rollups (1)
  • tag: statement
    entries: 1actionable: 0quick wins: 0linked PRs: 0
Metadata audit
Missing owner2
Missing effort3
Untagged2
Missing owner (2)
Missing effort (3)
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: 1direct uses: 0downstream unlocks: 0
    Associated lean decls (2)
No prerequisites (2)
No dependents (1)