Foundation Public Spine Detects Nontrivial Linking Three

The three-dimensional witness

In ordinary topology, a circle embedded in three-dimensional space can be linked with another circle: think of two interlocked rings that cannot be pulled apart without breaking one. The declaration detectsNontrivialLinking_three is the machine-checked statement that this phenomenon actually occurs in dimension three. It asserts that there exists a way to place a circle (a one-dimensional sphere) inside a three-dimensional sphere such that the circle is embedded, and the space left over after removing the circle has a nontrivial first homology group. That homology group, roughly the abelian invariant counting holes, is not zero, which is the formal signature that the circle is genuinely linked with something in the complement.

The proof constructs the example explicitly. It uses the standard unknot complement retract: remove a standard circle from the three-sphere, and the remaining space retracts onto a circle, whose first homology is the integers. This gives the nonzero homology directly. The same construction fails in dimensions zero and one, where the theorem not_detectsNontrivialLinking_zero and not_detectsNontrivialLinking_one state that no such linked embedding exists. The contrast is what makes the three-dimensional case special: it is the first dimension where nontrivial linking appears.

In the Recognition Science framework, this single fact becomes a load-bearing step. The framework's library proves a stronger statement: if any dimension D admits nontrivial linking of this kind, then D must equal three. That is the theorem D3_of_bridge, which takes the existence of a linking bridge as a hypothesis and concludes the dimension is exactly three. The bridge itself, called AlexanderLinkingBridge, is fully inhabited: it packages the three-dimensional witness together with the vanishing results in low dimensions and the exclusion of all higher dimensions via excision arguments. The axioms used are exactly the three standard ones of the underlying type theory, with no framework-specific postulates added.

What the declaration does not claim is just as important. It does not assert that physical space is three-dimensional; that would require an additional bridge from recognition events to topological linking, which remains open. It does not claim that every circle in three dimensions is linked, only that at least one linked embedding exists. And it does not derive the eight-tick cycle or the number 2^3 from this fact alone; those require the additional periodicity result CubePeriodEight, which is proved separately. The declaration is a precise topological witness, not a complete theory of dimension.

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

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

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

theorem D3_of_bridge (B : AlexanderLinkingBridge) :
    ∀ D, DetectsNontrivialLinking D → D = 3 :=
  B.forces_D3

What this page does not claim

The declaration does not assert that physical space is three-dimensional; that bridge from recognition to linking remains open. It does not claim that every circle in three dimensions is linked, only that at least one linked embedding exists. It does not derive the eight-tick cycle or the number 2^3 from this fact alone.

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: