Secure Messaging

Blueprint Summary🔗

Overview
Total entries4completed: 0; deps incomplete: 0; sorries: 0; no proof: 1
Ready now0Entries whose next formalization step is currently unblocked.
Fully closed0Local code and prerequisite closure are both complete.
Actionable priorities1Entries ready now and already unlocking downstream work.
Ready next (1)
  • prf_prng_scheme(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 3downstream unlocks: 3
Entry index (4)
Definitions3completed: 0; deps incomplete: 0; sorries: 0; no proof: 0
Theorems1completed: 0; deps incomplete: 0; sorries: 0; no proof: 1
Informal-only entries4
Definition Index (3)
Theorem / Proposition / Lemma / Corollary Index (1)
By parent groups (1)
PRF-PRNG from PRP and PRG. (1)
Dependency insights
Statement-used entries3Entries reused in statement dependencies.
Tracked parent groups2Grouped health rollups for parents with more than one child entry.
Most used in statements (3)
  • prf_prng_scheme(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
  • prf_prng_from_prp_prg_spec(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  • prf_prng_security(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Group health (2)
  • Pseudorandom Function-Generator (PRF-PRNG).prf_prng
    Grouped view over entries sharing the same parent.
    total: 2closed: 0local-only: 0ready: 1blocked: 1incomplete Lean: 0unlock score: 4
    Next: prf_prng_scheme stage: statementdownstream unlocks: 3
  • PRF-PRNG from PRP and PRG.prf_prng_prf_prng_from_prp_prg
    Grouped view over entries sharing the same parent.
    total: 2closed: 0local-only: 0ready: 0blocked: 2incomplete Lean: 0unlock score: 1
    Next: no ready child currently unlocks downstream work.
Metadata
Metadata audit
Missing owner4
Missing effort4
Untagged4
Missing owner (4)
Missing effort (4)
Untagged (4)
Structure and coverage
Informal-only4Statements with no associated Lean code yet.
Heaviest prerequisites (3)
  • prf_prng_from_prp_prg_security(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  • prf_prng_from_prp_prg_spec(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  • prf_prng_security(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
No prerequisites (1)
No dependents (1)