Pith. sign in
module module high

IndisputableMonolith.Verification.DimensionLinking

show as:
view Lean formalization →

Verification layer that records the Alexander-duality computation for an embedded circle in the D-sphere: the reduced first cohomology of the complement is isomorphic to the reduced cohomology of S^1 in degree D-2, hence nontrivial exactly when D=3. Cited by the T6–T8 spine audit when checking that spatial dimension is forced rather than postulated. The module mostly packages the Foundation.AlexanderDuality bridge and supplies explicit odd-dimension witnesses.

claimFor an embedded circle $K \subset S^D$, reduced Alexander duality gives $\widetilde{H}_1(S^D \setminus K) \cong \widetilde{H}^{D-2}(S^1)$. The right-hand side is nontrivial if and only if $D=3$, so nontrivial circle linking in the $D$-sphere forces $D=3$. The module also records odd-dimensional witness data for $D \in \{3,5,7,9\}$ used in sector and linking arguments.

background

Recognition Science forces spatial dimension at tier T8 of the UnifiedForcingChain. The topological engine is Alexander duality on spheres: non-trivial linking of an embedded circle exists in $S^D$ precisely when the complement carries a nontrivial reduced $H_1$.

Upstream, Foundation.AlexanderDuality replaces the old tautology "admits circle linking iff $D=3$" by a bridge predicate grounded in reduced cohomology degree (Hatcher, Algebraic Topology, Thm 3.44): $\widetilde{H}_1(S^D \setminus K) \cong \widetilde{H}^{D-2}(S^1)$, which is $\mathbb{Z}$ exactly at $D=3$.

This verification module sits one layer above that foundation. It re-exports the circle case, names the $H_1$ isomorphism, and packages loop-loop linking and same-sector parity constraints together with concrete witnesses at odd dimensions $D=3,5,7,9$.

proof idea

Not a single theorem: a thin verification façade over the cohomology argument already proved in Foundation.AlexanderDuality. The core claim is delegated to the predicate that $S^D$ admits nontrivial circle linking iff the dual degree $D-2$ hits the nontrivial reduced cohomology of $S^1$, i.e. iff $D=3$.

Sibling declarations then specialize: the $H_1$ complement isomorphism, the implication from loop-loop linking to $D=3$, a parity constraint that same-sector data force odd dimension, and explicit witness constructions (including reconstruction and an allowed-set characterization) at $D=3,5,7,9$. No new heavy algebraic topology is done here; the work is naming, packaging, and audit-facing witnesses.

why it matters in Recognition Science

T8 in the forcing chain asserts $D=3$ spatial dimensions. Without a genuine topological criterion, that step collapses to a definition. This module is the verification-side record that the criterion is Alexander duality for an embedded circle, nontrivial exactly at $D=3$.

It is imported by Verification.T6T8SpineAudit, the machine-checked honesty audit of tiers T6 (phi fixed point) through T8 (dimension). That audit distinguishes THEOREM content from FORCED-CONDITIONAL content; DimensionLinking supplies the topological spine item the auditor must see when scoring whether $D=3$ is forced.

Downstream readers checking the Recognition composition law chain or the eight-tick octave can treat this module as the place where "why three dimensions" is tied to a standard duality isomorphism rather than an axiom.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (12)