Foundation Public Spine Not Detects Nontrivial Linking One

A one-dimensional limit

Imagine trying to tie a knot in a piece of string that is confined to a line. The string cannot cross itself, so it cannot loop around anything; the only possible configuration is a straight segment. This is the intuition behind a formal result in the Recognition Science framework's machine-checked library of formal theorems: in one dimension, a circle cannot be embedded in a way that creates a nontrivial link. The declaration not_detectsNontrivialLinking_one proves that the sphere of dimension 1 does not detect nontrivial linking.

The statement is a theorem, not a definition or a hypothesis. It is proved in the framework's library, which is a collection of formal theorems verified by a computer. The theorem states that there is no embedding of a circle into a one-dimensional sphere such that the complement has nonzero first homology. In plain terms, the space left over after removing the circle from the line has no holes that would indicate a link. This is a topological fact, independent of any physical interpretation.

The result is part of a larger structure. The framework also proves that dimension zero has the same property, and that dimension three does detect nontrivial linking. Together, these statements help establish a boundary: linking is possible in three dimensions but not in lower ones. The one-dimensional case is the simplest nontrivial check in this sequence.

In Recognition Science, this theorem is a building block. The framework models physical structure through a discrete record of events, called a ledger, and uses topological properties to derive constraints on spatial dimensions. The one-dimensional result is a necessary step in showing that only three dimensions support the kind of linking that the framework associates with physical space. The theorem itself does not claim anything about physics; it is a pure mathematical statement about embeddings and homology.

What the theorem does not claim is equally important. It does not say that a one-dimensional space cannot contain any structure at all; it only rules out nontrivial linking. It does not say that the framework's physical model is correct; the bridge from topology to physics is a separate, open question. The theorem is a precise, limited result, and its value lies in what it excludes.

/-- **Vanishing at D = 1** (R3a of campaign P-d3link): an embedded circle in
S¹ is surjective (stereographic projection + connectedness), so the complement
is empty and its H₁ vanishes. -/
theorem not_detectsNontrivialLinking_one : ¬ DetectsNontrivialLinking 1 :=
  LinkingVanishingLowDim.not_detects_one

/-- **Non-encoding detector (panel K1, corrected 2026-07-08).** Some embedded
circle in S^D has homologically nontrivial complement: the real linking
obstruction, stated on the Mathlib object itself.

History: the first binder used an abstract `detects : ℕ → Prop` field plus a
`not_encoding` name-firewall. That was broken both ways: the empty detector
`fun _ => False` inhabited it trivially (verified: the probe built), and by
`funext`+`propext` any honest detector is *equal* to the encoding predicate,
so the firewall excluded exactly the real bridge. Content-typing is the only
non-gameable form. -/
def DetectsNontrivialLinking (D : ℕ) : Prop :=
  ∃ f : C(TopCat.sphere.{0} 1, TopCat.sphere.{0} D),
    Topology.IsEmbedding f ∧
      ¬ CategoryTheory.Limits.IsZero (linkingComplementH1 D f)

/-- **Vanishing at D = 0** (R3a of campaign P-d3link): every subspace of the
two-point S⁰ is totally disconnected, so complement H₁ vanishes for any map. -/
theorem not_detectsNontrivialLinking_zero : ¬ DetectsNontrivialLinking 0 :=
  LinkingVanishingLowDim.not_detects_zero

/-- **The detection half is proved** (R2 of campaign P-d3link, 2026-07-17):
the flat unknot `z ↦ (z,0,0)` embeds S¹ in S³, and its complement retracts
onto the core circle `(0,0,w)`, so `H₁(S¹;ℤ) ≅ ℤ` (proved,
`circleH1ZIsoInt_holds`) is a retract of the complement's first homology,
which therefore is not zero. Real Mathlib singular homology throughout; no
arithmetic encoding anywhere in the proof
(`Foundation/UnknotComplementRetract.lean`). -/
theorem detectsNontrivialLinking_three : DetectsNontrivialLinking 3 :=
  ⟨UnknotComplementRetract.unknot, UnknotComplementRetract.unknot_isEmbedding,
    UnknotComplementRetract.unknotComplementH1_ne_zero
      CircleWindingChain.circleH1ZIsoInt_holds⟩

What this page does not claim

The theorem does not claim that a one-dimensional space is empty or structureless, only that it lacks nontrivial linking. The theorem does not establish any physical consequence; the bridge from topology to physics is a separate open question. The theorem does not prove that three dimensions are the only ones where linking occurs, only that it does occur there.

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.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: