Pith. sign in
module module high

IndisputableMonolith.Foundation.TopologicalVeto

show as:
view Lean formalization →

The TopologicalVeto module axiomatizes the fact that integer-valued linking numbers for an embedded circle exist if and only if the ambient dimension is three, via Alexander duality on the complement homology. Recognition Science researchers cite it when enforcing D=3 from topological constraints in the forcing chain. The module imports J-cost geometry and pinch algebra but declares the duality result as an axiom aligned with the already-proved statement in Verification.Dimension.

claimFor an embedded circle $K \subset S^D$, the first homology satisfies $H_1(S^D \setminus K) \cong \mathbb{Z}$ if and only if $D=3$.

background

The module sits in the Foundation layer and imports JCostGeometry (F1: log-domain J-cost geometry with canonical reciprocal cost $J(x) = \frac12(x + x^{-1}) - 1$) and PinchAlgebra (F5: mutual divisibility in UFDs and Fredholm obstruction). Its doc-comment states the result as F6.1.1/1.2 and notes that the full Alexander duality proof is classical algebraic topology, matched to an already-proved result in Verification.Dimension.

No new definitions are introduced; the module supplies the topological veto that integer linking exists precisely when the spatial dimension is three.

proof idea

This is an axiomatic module with no internal proofs. It declares the homology isomorphism as an axiom whose justification is the classical Alexander duality theorem, cross-referenced to the prior verification result.

why it matters in Recognition Science

The module supplies the topological veto that forces D=3 in the Recognition framework (T8). It fills proposition F6.1.1/1.2 of the foundation paper and is referenced by sibling declarations such as linking_requires_D3 and linking_nontrivial_iff_D3 that build the dimension constraint into the J-cost and pinch-algebra setting.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)