Hossenfelder No-GoSpacetime Network Impossibility
No locally finite network in Minkowski spacetime can be Poincaré-invariant. This project provides an axiom-free Lean 4 formalization of Hossenfelder's no-go theorem (arXiv:1504.06070) with a constructive Heyting boundary interpretation connecting the impossibility to non-Boolean logic via the Eichhorn asymptotic-safety benchmark.
Can a discrete spacetime network be both locally finite and Poincaré-invariant? Hossenfelder proved the answer is no: the Lorentz group's non-compactness forces any invariant distribution on a Minkowski hyperbola to require infinitely many neighbors in every bounded region. We formalize this constructively and connect it to Heyting algebra logic: the boundary nucleus of any such network must be non-Boolean, and the Eichhorn UV-safe screening provides a concrete witness.
Hossenfelder's original argument targets discrete approaches to quantum gravity — causal sets, spin foams, loop quantum gravity — showing a fundamental tension between discreteness and Lorentz symmetry. If you want a locally finite network, you cannot have Poincaré invariance; if you want PI, your network must be non-local.
Our formalization makes this precise in Lean 4 without any classical axioms. The hyperbola unboundedness lemma uses explicit sinh/cosh parameterization rather than appealing to real analysis axioms, keeping the entire proof constructive.
The novel contribution is the Heyting boundary interpretation. We show that the no-go theorem implies a structural constraint on lattice logic: the boundary nucleus R of any spacetime admitting a PI network must act as the identity (Boolean). Since the Eichhorn UV-safe screening provides a concrete non-identity nucleus, the boundary is necessarily non-Boolean.
This bridges discrete quantum gravity impossibility results to constructive algebraic logic — a connection not present in Hossenfelder's original paper.
Formal Verification Certificate
Axiom-free formalization. The theorem layer uses zero classical axioms and zero sorry. All 15 theorems are kernel-checked by the Lean 4 type checker.
Hossenfelder No-Go • Lean 4 + Mathlib • Apoth3osis Labs