Foundation Public Spine Linking Assembly

The linking assembly

In topology, a linking number measures how two closed curves wind around each other, like two interlocked rings that cannot be separated without cutting. In ordinary three-dimensional space, such linking is possible: think of two chain links. In dimensions zero and one, linking is impossible for trivial dimensional reasons. The classical surprise is that in every dimension except three, the space around a curve is topologically simple enough that nontrivial linking cannot occur. Only in dimension three does the complement of a circle contain enough room for genuine linking.

Recognition Science builds its account of space on a ledger: a discrete record of recognition events, where each event is a unit of matching between a system and its environment. From that ledger, the framework's library of machine-checked formal theorems proves that the cost of recognition forces a preferred scaling, and from that scaling it derives a cycle of eight ticks. The public spine is the framework's name for the chain of results that tries to force the number of spatial dimensions from these recognition dynamics alone. The linking assembly is the part of that chain that says: if the ledger detects nontrivial linking, then the dimension must be three.

The assembly establishes this in two steps, both conditional on a frontier assumption about arc complements. The first result, forces_D3_of_arcAcyclic, states that if every dimension other than three has acyclic arc complements, then any dimension that detects nontrivial linking must equal three. The second result, target_of_arcAcyclic, packages that conclusion into the full goal of the public spine: a complete bridge from the detection of linking to the conclusion that space has exactly three dimensions. Both are proved in the machine-checked library, with no reliance on the legacy DimensionForcing.linking_requires_D3 axiom that earlier versions of the framework used.

The condition about arc complements is the frontier: it says that in dimensions two and above four, the space left over after removing an arc is topologically uncomplicated. This is a genuine open mathematical question, not a proved fact. The results are conditional on it. What the assembly does prove unconditionally is the logical structure: given that frontier, the detection of linking forces dimension three, and the bridge is complete. The physical claim that recognition actually detects linking in this way remains open; the assembly establishes the topological theorem, not the physical bridge.

What this changes for a reader is the status of the dimension argument. The framework no longer needs to assert as an axiom that linking requires three dimensions. Instead, that conclusion is a theorem under a stated topological condition, and the condition itself is a precise target for future work. The assembly turns a postulate into a conditional proof, and names exactly what remains to be shown.

/-- The binder's uniqueness half, conditional on the arc-complement
frontier.  Dimensions `0`, `1` are unconditional (`LinkingVanishingLowDim`);
dimensions `2` and `≥ 4` are the Mayer-Vietoris reduction of
`LinkingVanishingHighDim`. -/
theorem forces_D3_of_arcAcyclic
    (harc : ∀ D, 2 ≤ D → D ≠ 3 →
      LinkingVanishingHighDim.ArcComplementsAcyclic D) :
    ∀ D, PublicSpine.DetectsNontrivialLinking D → D = 3 :=
  fun D hdet => LinkingVanishingHighDim.forces_D3_of_arcAcyclic harc D hdet

/-- The binder's uniqueness half, conditional on the arc-complement
frontier.  Dimensions `0`, `1` are unconditional (`LinkingVanishingLowDim`);
dimensions `2` and `≥ 4` are the Mayer-Vietoris reduction of
`LinkingVanishingHighDim`. -/
theorem forces_D3_of_arcAcyclic
    (harc : ∀ D, 2 ≤ D → D ≠ 3 →
      LinkingVanishingHighDim.ArcComplementsAcyclic D) :
    ∀ D, PublicSpine.DetectsNontrivialLinking D → D = 3 :=
  fun D hdet => LinkingVanishingHighDim.forces_D3_of_arcAcyclic harc D hdet

/-- The campaign target, conditional on the arc-complement frontier: a
fully inhabited `AlexanderLinkingBridge`, bypassing the
`DimensionForcing.linking_requires_D3` axiom on the public spine. -/
theorem target_of_arcAcyclic
    (harc : ∀ D, 2 ≤ D → D ≠ 3 →
      LinkingVanishingHighDim.ArcComplementsAcyclic D) :
    PublicSpine.target_D3_from_nonencoding_linking :=
  PublicSpine.bridge_of_forces_D3 (forces_D3_of_arcAcyclic harc)

What this page does not claim

The physical claim that recognition actually detects linking in the world is not established by this module. The arc-complement frontier condition is not proved; it is an open assumption on which the theorems are conditional. The module does not prove that space is three-dimensional without any assumptions; it proves a conditional theorem under the stated frontier.

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