Foundation Public Spine K1 Cheat Must Fail

The cheat witness

The recognition framework, a system that derives physical structure from a forced cost of retaining a discrete record of events, needs a bridge between its abstract proofs and the physical claim that space has three dimensions. That bridge is a formal statement about nontrivial linking in the homology of circle complements, a precise topological condition. The file K1CheatMustFail.lean exists to prove the bridge cannot be faked by a shortcut.

Two cheats are documented, each a named theorem that must fail to compile. The first, encoding_plugin_must_fail, tries to claim that the sphere admits circle linking by unfolding to a trivial arithmetic fact, (3:ℤ) - 2 = 1. The second, empty_detector_must_fail, attempts to build the bridge using a detector that always returns false. Both are type errors: the first cannot elaborate as a complement-homology nonvanishing, the second refers to a field that no longer exists. The file is deliberately excluded from any import graph; a gate script checks it exists and names the cheats, but never builds it.

The lesson the module encodes is that in proposition-land, you cannot firewall by predicate identity. An earlier fix tried to use a name firewall to exclude the encoding, but by funext and propext any honest detector is equal to the encoding predicate, so the firewall excluded exactly the real bridge. Only content-typing holds: the bridge must be a fixed definition on genuine singular homology of circle-complement subspaces, not a choosable structure field.

In plain language: the framework's library of machine-checked formal theorems proves that three-dimensional space is forced, but that proof must connect to a real topological condition. This file is the guard that says the connection cannot be simulated by a cheap arithmetic trick or an empty function. If this file ever builds green, the binder has been weakened, and that is treated as a gate failure.

/-- DO_NOT_BUILD: encoding plug-in. Must fail with a type mismatch. -/
theorem encoding_plugin_must_fail : DetectsNontrivialLinking 3 :=
  D3_admits_circle_linking

/-- DO_NOT_BUILD: old empty-detector cheat. Must fail: no such field. -/
theorem empty_detector_must_fail : Nonempty AlexanderLinkingBridge :=
  ⟨{ h1 := CircleWindingChain.circleH1ZIsoInt_holds
     detects_nontrivial_linking := fun _ => False
     forces_D3 := fun _ h => h.elim }⟩

What this page does not claim

This module does not prove that three-dimensional space is forced; it only guards the bridge that would connect to that proof. The file does not establish that the cheats are logically impossible, only that they fail to type-check under the current binder. No claim is made here about the physical recognition-to-linking bridge, which remains open.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PublicSpine/K1CheatMustFail.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: