Formally verified Hossenfelder no-go theorem for Poincaré-invariant spacetime networks in Lean 4. Axiom-free proof + constructive Heyting boundary non-Booleanity witness from asymptotic safety.
formal-verification quantum-gravity mathlib lean4 no-go-theorem heyting-algebra asymptotic-safety hossenfelder spacetime-networks boundary-nucleus
-
Updated
Mar 14, 2026 - Lean