Foundation Public Spine K1 Cheat Must Fail Empty Detector Must Fail

The empty detector guard

In a machine-checked library of formal theorems, a declaration named empty_detector_must_fail is a guard, not a theorem. It is part of a file that the library's build system must reject. The declaration attempts to prove that a certain mathematical structure, the AlexanderLinkingBridge, exists. That bridge is meant to connect a physical claim about three-dimensional space to a formal statement about linking in the complement of a circle. The old cheat was to fill the bridge's detector field with a function that always returns False, an empty detector that claims to detect nontrivial linking but actually detects nothing. The new declaration shows that this cheat is no longer expressible: the detector is no longer a choosable field of the structure, so the attempted proof fails with an unknown-field error.

The broader lesson is about how the framework handles logical firewalls. Earlier, the library tried to block cheats by naming a predicate not_encoding and requiring the detector to be different from an arithmetic encoding. But in the logical system used, any honest detector is provably equal to that encoding predicate, so the firewall excluded the real bridge. The empty detector exploited this by being vacuously different. The current binder fixes this by changing the structure itself: the detector is now a fixed definition on genuine singular homology of circle-complement subspaces, not a field the user can fill. The empty detector cannot even be written, because there is no field to fill.

This declaration does not prove that the bridge exists. It does not prove that three-dimensional space is forced, nor that the physical recognition-to-linking bridge holds. It only establishes that a specific old cheat fails to build. The file is kept out of the import graph; the gate checks that the file exists and names the cheats, but does not build it. If this file ever built green, that would signal that the binder had been weakened. The declaration is a negative test, a canary, not a positive result.

/-- 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 }⟩

/-- 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 }⟩

/-- 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 declaration does not prove that the AlexanderLinkingBridge exists. This declaration does not prove that three-dimensional space is forced. This declaration does not prove that the physical recognition-to-linking bridge holds.

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: