Starter Blueprint

Blueprint Summary🔗

Overview
Total entries9completed: 1; deps incomplete: 4; sorries: 1; no proof: 0
Ready now1Entries whose next formalization step is currently unblocked.
Fully closed1Local code and prerequisite closure are both complete.
Actionable priorities1Entries ready now and already unlocking downstream work.
Current blockers1Missing external or incomplete Lean declarations.
Ready next (1)
  • addition_spec(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 4downstream unlocks: 6
Current blockers (1)
Entry index (9)
Definitions4completed: 0; deps incomplete: 1; sorries: 0; no proof: 0
Theorems5completed: 1; deps incomplete: 3; sorries: 1; no proof: 0
Informal-only entries3
Definition Index (4)
Theorem / Proposition / Lemma / Corollary Index (5)
By parent groups (3)
A small exploratory chapter about the Collatz iteration on natural numbers. (1)
Core statements about addition on natural numbers. (2)
Core statements about multiplication on natural numbers. (2)
Dependency insights
Statement-used entries3Entries reused in statement dependencies.
Tracked parent groups3Grouped health rollups for parents with more than one child entry.
Most used in statements (3)
  • addition_spec(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 6
  • multiplication_spec(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
  • collatz_step(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    Associated lean decls (2)
Group health (3)
  • Core statements about addition on natural numbers.addition_core
    Grouped view over entries sharing the same parent.
    total: 4closed: 0local-only: 2ready: 2blocked: 0incomplete Lean: 0unlock score: 6
    Next: addition_spec stage: statementdownstream unlocks: 6
  • A small exploratory chapter about the Collatz iteration on natural numbers.collatz_core
    Grouped view over entries sharing the same parent.
    total: 2closed: 0local-only: 1ready: 1blocked: 0incomplete Lean: 1unlock score: 1
    Next: no ready child currently unlocks downstream work.
  • Core statements about multiplication on natural numbers.multiplication_core
    Grouped view over entries sharing the same parent.
    total: 3closed: 1local-only: 1ready: 0blocked: 1incomplete Lean: 0unlock score: 3
    Next: no ready child currently unlocks downstream work.
Metadata
Owners in use1Distinct owners referenced by the current blueprint entries.
Tags in use5Distinct tags currently attached to blueprint entries.
Owner rollups (1)
  • Project Authorproject_author
    entries: 1actionable: 0quick wins: 0linked PRs: 0
Tag rollups (5)
  • tag: arithmetic
    entries: 2actionable: 0quick wins: 0linked PRs: 0
  • tag: starter
    entries: 2actionable: 0quick wins: 0linked PRs: 0
  • tag: famous
    entries: 1actionable: 0quick wins: 0linked PRs: 0
  • tag: incomplete
    entries: 1actionable: 0quick wins: 0linked PRs: 0
  • tag: playful
    entries: 1actionable: 0quick wins: 0linked PRs: 0
Metadata audit
Missing owner8
Missing effort6
Untagged6
Missing owner (8)
Missing effort (6)
Untagged (6)
Structure and coverage
Informal-only3Statements with no associated Lean code yet.
Ready to formalize1Entries whose next step is currently unblocked.
Formalized, ancestors open4Local Lean work is done, but prerequisite closure is still open.
Fully closed1Local code and ancestor closure are both complete.
Heaviest prerequisites (6)
  • collatz_step(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
    Associated lean decls (2)
  • addition_assoc(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)
  • addition_right_identity(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)
  • collatz_conjecture(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)
  • multiplication_one_right(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)
  • multiplication_spec(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 3
No prerequisites (3)
No dependents (6)
Proof debt hotspots (1)
  • A small exploratory chapter about the Collatz iteration on natural numbers.collatz_core
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 1incomplete decls: 1missing decls: 0total debt: 1