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.

Formally verified asymptotic safety for quantum gravity in Lean 4. RG flow as a nucleus operator, calibrated particle-physics prediction bounds, and constructive dark-matter exclusion.

Lean 4 formalization of Bennett's Stack Theory proving hard bounds on delegation in multi-layer intelligence architectures, with novel Heyting nucleus bridge theorems

Verified INT8 Quantization Gap Analysis via Heyting Algebra Nuclei — Lean 4 proofs connecting qReLU nucleus operators to the Hossenfelder no-go theorem