Foundation Linking Vanishing High Dim Forces D3 Of Arc Acyclic

The dimension theorem

In topology, two closed curves are linked when they cannot be pulled apart without crossing. In three-dimensional space, two circles can be linked like the rings of a chain. The Recognition Science framework's machine-checked library of formal theorems contains a result, forces_D3_of_arcAcyclic, that pins down when this linking behavior is possible.

The theorem states: if for every dimension D from 2 upward, except D = 3, the complement of any embedded arc in the D-sphere has trivial first homology, then any dimension that detects nontrivial linking must be 3. In plainer terms, under the stated condition, the only dimension where a circle can be linked with another circle is dimension 3. The proof in the library checks each dimension separately, ruling out 0 and 1 by low-dimensional arguments and ruling out all higher dimensions by the arc acyclicity assumption.

The condition ArcComplementsAcyclic says that for any smoothly embedded arc in the sphere of dimension D, the first homology group of the complement is zero. This is a strong topological property. The theorem does not assert that this condition holds for all dimensions; it takes it as a hypothesis. The library also proves that the condition itself fails in dimension 2, where the complement of an arc can have nontrivial first homology.

In Recognition Science, this theorem is part of a larger chain that forces three spatial dimensions from the framework's axioms. The framework models physical space as a recognition ledger, a discrete record of events, and derives that the cost of recognition must take a specific form. From that cost function, the framework proves that only three dimensions can support the kind of linking that physical space exhibits. The theorem here is the topological milestone in that chain.

What the theorem does not claim is just as important. It does not prove that the physical world is three-dimensional; that would require bridging the topological result to the physical recognition-to-linking bridge, which remains open. It does not claim that the arc acyclicity condition is true in any particular dimension; that is a separate statement. And it does not say that linking is impossible in all higher dimensions, only that under the stated hypothesis, no dimension other than 3 can detect it.

/-- **The bridge's uniqueness half, conditional on the arc frontier**:
granting arc-complement acyclicity in every dimension `D ≥ 2`, `D ≠ 3`,
nontrivial linking forces `D = 3`.  Dimensions `0` and `1` are the banked
unconditional results (`LinkingVanishingLowDim`). -/
theorem forces_D3_of_arcAcyclic
    (harc : ∀ D, 2 ≤ D → D ≠ 3 → ArcComplementsAcyclic D) :
    ∀ D, DetectsNontrivialLinking D → D = 3 := by
  intro D hdet
  by_contra hne
  match D, hne with
  | 0, _ => exact LinkingVanishingLowDim.not_detects_zero hdet
  | 1, _ => exact LinkingVanishingLowDim.not_detects_one hdet
  | (n + 2), hne =>
      exact not_detects_of_arcAcyclic (n + 2) (by omega) hne
        (harc (n + 2) (by omega) hne) hdet

/-- **The bridge's uniqueness half, conditional on the arc frontier**:
granting arc-complement acyclicity in every dimension `D ≥ 2`, `D ≠ 3`,
nontrivial linking forces `D = 3`.  Dimensions `0` and `1` are the banked
unconditional results (`LinkingVanishingLowDim`). -/
theorem forces_D3_of_arcAcyclic
    (harc : ∀ D, 2 ≤ D → D ≠ 3 → ArcComplementsAcyclic D) :
    ∀ D, DetectsNontrivialLinking D → D = 3 := by
  intro D hdet
  by_contra hne
  match D, hne with
  | 0, _ => exact LinkingVanishingLowDim.not_detects_zero hdet
  | 1, _ => exact LinkingVanishingLowDim.not_detects_one hdet
  | (n + 2), hne =>
      exact not_detects_of_arcAcyclic (n + 2) (by omega) hne
        (harc (n + 2) (by omega) hne) hdet

/-- **The precisely-stated remaining frontier** (Hatcher 2B.1, arc case):
every topological embedding of the unit interval into `S^D` has
`H₁`-acyclic complement.  Classically true for every `D` (compact-support
bisection); this file consumes it as a hypothesis parameter and reduces
`forces_D3` to it. -/
def ArcComplementsAcyclic (D : ℕ) : Prop :=
  ∀ a : C(unitInterval, ↥(Sph D)), Topology.IsEmbedding a →
    CategoryTheory.Limits.IsZero
      (Hgrp (TopCat.of {y : ↥(Sph D) // y ∉ Set.range a}) 1)

What this page does not claim

This theorem does not prove that physical space is three-dimensional; the bridge from topology to physics remains open. This theorem does not assert that the arc acyclicity condition holds in any particular dimension. This theorem does not say that linking is impossible in all dimensions other than three, only that under the stated hypothesis no other dimension can detect it.

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