Pillar 2 · Blueprint Graph
Interactive Dependency DAG
Assumption Ledger Tracking
PlasmaLean Formalization Blueprint & Dependency DAG
Click any node in the directed acyclic graph below to inspect its mathematical statement, exact Lean 4 declaration signature, handbook chapter, and status in the Assumption Ledger. Notice how the entire formalization rests on 3 small Kernel Contracts at the top, validated immediately by Sanity Checks and compiled into the Vacuum-Fixture Certificate.
■ Cyan: Small Kernel Contract
■ Violet: Non-Vacuity Sanity Check
■ Emerald: Compiled Lean 4 Proof
■ Amber: Open Pure-Math Target
Kernel Contract
Node K1
Select a node in the graph
Handbook Chapter: geometry-and-fields.html ↗
Mathematical Formulation
Lean 4 Signature