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
MENTAT Contribution Certificates
Immutable contribution records for the Hossenfelder no-go publication chain. Theory-level certificate points to the original arXiv paper; proof and bridge certificates point to the Lean 4 formalization bundle.
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Ontological EngineerNo-Go Theorem for Poincaré-Invariant Spacetime Networks
Contributor
Sabine Hossenfelder
Munich Center for Mathematical Philosophy, LMU Munich
Hossenfelder's 2015 result (arXiv:1504.06070) establishes that no locally finite network embedded in Minkowski spacetime can be Poincaré-invariant. The key insight: for any nonzero Minkowski interval α, the hyperbola at α is unbounded, so uniform distribution of neighbors on it requires infinitely many nodes in any bounded region.
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Ontological EngineerAxiom-Free Lean 4 Formalization
Contributor
Apoth3osis Labs
R&D Division
Complete machine-checked proof in Lean 4 with zero axioms and zero sorry. The hyperbola unboundedness lemma (hyperbola_infinite_length) is proved constructively via sinh/cosh parameterization against the product norm max(|Δt|,|Δx|), avoiding any appeal to classical real analysis axioms. The main theorem (no_poincare_invariant_locally_finite_network) composes Finset.card bounds against the unboundedness witness.
Builds Upon
MENTAT Contribution Record
BRIDGE
Cross-Level Connection
CONTRIBUTION LEVEL: BRIDGE
Ontological EngineerHeyting Boundary Interpretation and Eichhorn Witness
Contributor
Apoth3osis Labs
R&D Division
The bridge contribution connects the no-go theorem to Heyting algebra logic. A BoundaryNucleus R is Boolean iff R = id; boundary_necessarily_non_boolean shows any nucleus whose carrier lattice admits a PI network must be Boolean, contradicting the no-go. The Eichhorn UV-safe projection provides a concrete non-Boolean witness: topYukawa=1 is screened to 0 because criticalTopYukawa + yukawaGravityShift = −1.03 ≤ 0.
Builds Upon
Governed by MENTAT-CA-001 v1.0 · March 2026
“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune
A janitor who proves a theorem outranks a tenured professor who publishes noise.
Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.
A valid, original framing or conjecture
Formal argument with paper-level rigor
Connecting theory to observable outcomes
Working software the project depends on
Reproducible research with methodology and data
Machine-verified claim checked by a proof assistant
Foundational, load-bearing implementation
Connecting subsystems or knowledge domains end-to-end
Strategic direction & roadmaps
Writing, documentation & papers
Visual, UX & information design
Teaching, tutorials & workshops
Community, outreach & events
Partnerships, governance & policy
Translation, media & accessibility
Ethics, review & quality assurance
Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.