>_HOSSENFELDER.NOGO

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.

arXiv:1504.06070 GitHub

>_VERIFICATION.SEAL

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.

15 THEOREMS VERIFIED12 MODULES970 LINES0 SORRY

Hossenfelder No-Go • Lean 4 + Mathlib • Apoth3osis Labs

>_KEY.MATHEMATICS

Headline Theorems

QEDno_poincare_invariant_locally_finite_network

\neg\exists\, N,\; \mathrm{LocallyFinite}(N) \wedge \mathrm{PoincareInvariant}(N)

No locally finite network in Minkowski spacetime can be Poincaré-invariant.

QEDhyperbola_infinite_length

\alpha \neq 0 \Longrightarrow \neg\exists\, L,\; \forall d \in \mathcal{H}_\alpha,\; \|(\Delta t, \Delta x)\| \leq L

Nonzero Lorentz hyperbolae are unbounded in the ambient product norm. Proved directly via sinh/cosh parameterization.

QEDeichhorn_nucleus_not_boolean

\neg\, \mathrm{isBoolean}(R_{\mathrm{Eichhorn}})

Constructive proof: the Eichhorn benchmark nucleus is non-Boolean. Concrete singleton witness with screened topYukawa.

QEDboundary_necessarily_non_boolean

\mathrm{BooleanBoundaryBridge}(N) \Longrightarrow \neg\, \mathrm{isBoolean}(N)

Any boundary nucleus satisfying the bridge hypothesis cannot be Boolean.

QEDgap_nonzero_at_boundary

\exists\, a \in L,\; \mathrm{boundaryGap}(N, a) \neq \emptyset

The boundary gap is nonempty — not every element is a fixed point of the nucleus.

>_PAPER.PROOF.CORRESPONDENCE

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

>_PROOF.BLUEPRINT

Proof Modules

Click any module to view its mathematical content and Lean 4 source.

>_DEPENDENCY.GRAPH

Module Dependencies

Hover over a module to trace its imports. No circular dependencies.

Spacetime

Networks

HeytingBoundary

Bridge

>_VERIFIED.C

Verified C Artifacts

Compiled with gcc -std=c11 -Wall -Werror.

C

minkowski_interval.c

Spacetime displacement and Minkowski interval

DOWNLOAD

C

lorentz_group.c

Lorentz boost and hyperbola witness construction

DOWNLOAD

C

locally_finite.c

Network structure and link counting

DOWNLOAD

C

boundary_nucleus.c

Boundary nucleus Booleanity and gap checks

DOWNLOAD

>_SAFE.RUST

Safe Rust Artifacts

cargo build (0 warnings) + cargo test (10 pass).

Rs

spacetime.rs

Minkowski interval, Lorentz boost, hyperbola witness

DOWNLOAD

Rs

network.rs

Spacetime network and uniformity checks

DOWNLOAD

Rs

boundary.rs

Boundary nucleus, Booleanity, Eichhorn projection

DOWNLOAD

Rs

lib.rs

Crate root

DOWNLOAD

Rs

Cargo.toml

Package manifest

DOWNLOAD

>_IPFS.PERMANENT.STORAGE

IPFS Permanent Storage

All artifacts content-addressed and pinned to IPFS.

Lean Proofsbafkreigmez6dafsm4jnelcigrbn662ffn3woro5vwg32os6zkeoxdkrbqu Verified Cbafkreiftuuc7ahzfmln3ptg5n4oj25oxwvf424rc6l42duuljzy5obwapq Safe Rustbafkreibtenaw5trkzhe3b2fuasz36h36vtwklg7flb7qt6laoacc3wiomi ALL (Root)bafybeibzq7f46bqpakbqmi6o6mkn6qlbwmpwbg34nvzyagkuvg65e4egie

>_PROVENANCE.CHAIN

Provenance Chain

1

Paper

Hossenfelder, arXiv:1504.06070 (2015)

2

Lean 4 Proof

12 modules, 15 theorems, 0 sorry, 0 axioms

3

Verified C

4 files compiled with gcc -Wall -Werror

4

Safe Rust

3 modules, 10/10 tests pass, 0 unsafe

5

IPFS Pinned

CID: bafybeibzq7f46bqpakb...

>_RELATED.LINKS

Asymptotic Safety PPC

Related: RG nucleus, calibrated predictions

GitHub Repository

Source code with README and CITATION.cff

arXiv:1504.06070

Hossenfelder's original paper