Secure Messaging

Blueprint Summary🔗

Overview
Total entries23completed: 5; deps incomplete: 4; sorries: 0; no proof: 9
Ready now0Entries whose next formalization step is currently unblocked.
Fully closed5Local 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 (23)
Definitions13completed: 5; deps incomplete: 3; sorries: 0; no proof: 0
Theorems10completed: 0; deps incomplete: 1; sorries: 0; no proof: 9
Informal-only entries14
Definition Index (13)
Theorem / Proposition / Lemma / Corollary Index (10)
By parent groups (5)
Sparse Post-Quantum Ratchet (SPQR) ( ). (2)
Opp-UniKEM-CKA. (2)
Opp-RKEM-CKA. (2)
ML-KEM Braid ( ). (2)
Opp-BiKEM-CKA. (2)
Dependency insights
Statement-used entries13Entries reused in statement dependencies.
Tracked parent groups7Grouped health rollups for parents with more than one child entry.
Most used in statements (13)
Group health (7)
  • SCKA.cka_protocols_scka
    Grouped view over entries sharing the same parent.
    total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 42
    Next: no ready child currently unlocks downstream work.
  • Unchunked SPQR core.spqr_unchunked_core
    Grouped view over entries sharing the same parent.
    total: 2closed: 0local-only: 2ready: 0blocked: 0incomplete Lean: 0unlock score: 8
    Next: no ready child currently unlocks downstream work.
  • ML-KEM Braid ( ).cka_protocols_mlkem_braid
    Grouped view over entries sharing the same parent.
    total: 4closed: 1local-only: 0ready: 0blocked: 3incomplete Lean: 0unlock score: 5
    Next: no ready child currently unlocks downstream work.
  • Opp-BiKEM-CKA.cka_protocols_opp_bikem_cka
    Grouped view over entries sharing the same parent.
    total: 3closed: 0local-only: 0ready: 0blocked: 3incomplete Lean: 0unlock score: 2
    Next: no ready child currently unlocks downstream work.
  • Opp-RKEM-CKA.cka_protocols_opp_rkem_cka
    Grouped view over entries sharing the same parent.
    total: 3closed: 0local-only: 0ready: 0blocked: 3incomplete Lean: 0unlock score: 2
    Next: no ready child currently unlocks downstream work.
  • Opp-UniKEM-CKA.cka_protocols_opp_unikem_cka
    Grouped view over entries sharing the same parent.
    total: 3closed: 0local-only: 2ready: 0blocked: 1incomplete Lean: 0unlock score: 2
    Next: no ready child currently unlocks downstream work.
  • Sparse Post-Quantum Ratchet (SPQR) ( ).cka_protocols_spqr
    Grouped view over entries sharing the same parent.
    total: 3closed: 0local-only: 0ready: 0blocked: 3incomplete Lean: 0unlock score: 2
    Next: no ready child currently unlocks downstream work.
Metadata
Metadata audit
Missing owner23
Missing effort23
Untagged23
Missing owner (23)
Missing effort (23)
Untagged (23)
Structure and coverage
Informal-only14Statements with no associated Lean code yet.
Formalized, ancestors open4Local Lean work is done, but prerequisite closure is still open.
Fully closed5Local code and ancestor closure are both complete.
Heaviest prerequisites (22)
No prerequisites (1)
No dependents (10)