Foundation Public Spine K1 Cheat Must Fail Encoding Plugin Must Fail

A failed shortcut

In formal mathematics, a theorem is only as strong as the definitions it rests on. The Recognition Science library contains a file that is designed to fail: it holds two attempted proofs that are deliberately built to be rejected by the machine. The first, encoding_plugin_must_fail, tries to prove that a 3-sphere admits a certain kind of circle linking by reducing the claim to the arithmetic statement 3 - 2 = 1. This does not work. The claim is about genuine homology of a circle-complement subspace, a topological fact, and the arithmetic encoding simply does not elaborate as such. The machine reports a type mismatch.

The second attempted proof, empty_detector_must_fail, tries to inhabit the bridge structure with a detector that always returns false. This also fails, because the detector is no longer a choosable field; the structure is fixed to a real definition on singular homology. The old cheat is not even expressible. The file is kept out of the import graph on purpose, and a gate script checks that it exists and names the cheats without building it. If this file ever builds green, the binder has been weakened and the gate fails.

In Recognition Science, the point is not that the arithmetic encoding is false. The point is that a theorem must be about what it claims to be about. The framework models physical recognition events, and its bridge from geometry to number must be a real content-typing, not a name firewall or a predicate identity. The failed file is a witness: it shows what the framework does not accept as a shortcut, and it keeps the path honest.

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

The file does not prove that the arithmetic encoding is false in general. The file does not establish that the circle-linking bridge itself is impossible. The file does not claim that the framework's three-dimensional forcing is invalid.

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: