Hossenfelder No-Go Theorem
Axiom-free Lean 4 proof that no Poincaré-invariant locally finite network exists in Minkowski spacetime, with constructive Heyting boundary non-Booleanity witness.
MODULES
12
Lean 4 source files
THEOREMS
15
Machine-checked
AXIOMS
0
Fully proved
SORRY
0
Complete verification
Formal Verification Certificate
Every theorem in this project has been machine-checked by the Lean 4 kernel. No axiom is assumed without proof. No gap exists in the verification chain.
Hossenfelder No-Go • Lean 4 + Mathlib • Apoth3osis Labs
Headline Theorems
No locally finite network in Minkowski spacetime can be Poincaré-invariant.
Nonzero Lorentz hyperbolae are unbounded in the ambient product norm. Proved directly via sinh/cosh parameterization.
Constructive proof: the Eichhorn benchmark nucleus is non-Boolean. Concrete singleton witness with screened topYukawa.
Any boundary nucleus satisfying the bridge hypothesis cannot be Boolean.
The boundary gap is nonempty — not every element is a fixed point of the nucleus.
Paper ↔ Proof Correspondence
Every section of the original paper is covered by verified Lean 4 modules.
| PAPER | PROOF MODULE | STATUS |
|---|---|---|
| §1 Introduction | MinkowskiInterval.lean | PROVED |
| §2 Spacetime Symmetries | LorentzGroup.lean | PROVED |
| §3 Network Structure | LocallyFinite.lean | PROVED |
| §4 Main Theorem | NoGoTheorem.lean | PROVED |
| §5 Heyting Boundary | BoundaryNucleus.lean + GapNonZero.lean | PROVED |
| §6 Dynamic Gap | DynamicGap.lean + BandConstraint.lean | PROVED |
| §7 AS Bridge | NucleusConnection.lean | PROVED |
“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.
Proof Modules
Click any module to view its mathematical content and Lean 4 source.
Module Dependencies
Hover over a module to trace its imports. No circular dependencies.
Verified C Artifacts
Compiled with gcc -std=c11 -Wall -Werror.
Safe Rust Artifacts
cargo build (0 warnings) + cargo test (10 pass).
IPFS Permanent Storage
All artifacts content-addressed and pinned to IPFS.
Provenance Chain
Paper
Hossenfelder, arXiv:1504.06070 (2015)
Lean 4 Proof
12 modules, 15 theorems, 0 sorry, 0 axioms
Verified C
4 files compiled with gcc -Wall -Werror
Safe Rust
3 modules, 10/10 tests pass, 0 unsafe
IPFS Pinned
CID: bafybeibzq7f46bqpakb...