Penumbra: Machine-checked proof that every non-Boolean projection through a nucleus produces a universal, irreducible information gap. 162 files, 1,486 declarations, zero sorry. Lean 4 + Mathlib.
information-theory theorem-proving formal-verification mathematical-physics lean4 heyting-algebra machine-checked-proofs nucleus-operator
-
Updated
Mar 17, 2026 - Lean