Pith. sign in
module module high

IndisputableMonolith.Foundation.PublicSpineLinkingClosure

show as:
view Lean formalization →

Unconditional closure that nontrivial linking detection forces spatial dimension exactly 3. Low dimensions (0,1) vanish by elementary linking vanishing; dimensions 2 and ≥4 vanish by Mayer–Vietoris reduction of high-dimensional linking vanishing once arc-complement acyclicity is supplied. Anyone citing the RS forcing of D=3 (T8) uses this assembly. The module wires the two imported spines into a single dimension-forcing statement.

claimNontrivial linking detection forces spatial dimension $D=3$. For $D\in\{0,1\}$ linking vanishes by the low-dimensional vanishing theorem. For $D=2$ and $D\ge 4$, linking vanishes by the Mayer–Vietoris reduction of high-dimensional linking vanishing, instantiated with arc-complement acyclicity. Thus the only dimension compatible with nontrivial linking is $D=3$.

background

Recognition Science forces $D=3$ spatial dimensions as step T8 of the unified forcing chain. The geometric content is that a nontrivial linking invariant on the recognition spine can exist only in three dimensions; every other dimension makes the invariant vanish.

This module sits at the public spine of that argument. It imports the arc-complement acyclicity package (homology of the complement of an arc is acyclic in the relevant degrees) and the public spine linking assembly (the packaged low- and high-dimensional vanishing statements, including Mayer–Vietoris reductions). Sibling names forces_D3 and target_D3 mark the forced claim and its dimensional target.

The local setting is pure topological forcing: no dynamical or metric hypotheses beyond the linking and acyclicity data already assembled upstream.

proof idea

The module is an assembly/closure layer, not a fresh calculation. It routes dimensions $0$ and $1$ through the low-dimensional linking-vanishing theorem, and routes dimensions $2$ and $\ge 4$ through the high-dimensional linking-vanishing theorem after Mayer–Vietoris reduction, with arc-complement acyclicity plugged in as the required homology input. The residual case is exactly $D=3$, recorded as the forced dimension. Structure is case-split on dimension plus instantiation of the imported vanishing packages.

why it matters in Recognition Science

This is the unconditional public statement that nontrivial linking forces $D=3$, i.e. the topological half of forcing-chain step T8. Downstream consumers of the RS dimension count cite this closure rather than the separate low- and high-dimensional lemmas. The doc-comment states the split explicitly: low dimensions by LinkingVanishingLowDim, high dimensions by Mayer–Vietoris reduction of LinkingVanishingHighDim plus arc-complement acyclicity. No further used-by edges are recorded at module scope; the payload is the dimension-forcing claim itself inside the Foundation spine.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (2)