pith. sign in
module module high

IndisputableMonolith.Foundation.TopologicalVeto

show as:
view Lean formalization →

The TopologicalVeto module axiomatizes the consequence of Alexander duality that integer linking numbers for embedded circles exist only in three dimensions. It would be cited by any Recognition Science argument that derives D = 3 from topological obstructions rather than from the forcing chain alone. The module imports JCostGeometry and PinchAlgebra but contains no internal proofs, serving purely as an interface to the classical result already established in Verification.Dimension.

claimFor an embedded circle $K ⊂ S^D$, the first homology satisfies $H_1(S^D ∖ K) ≅ ℤ$ if and only if $D = 3$.

background

This module belongs to the Foundation layer and imports the log-domain J-cost geometry of F1 together with the UFD mutual-divisibility results of F5. It introduces the topological veto that follows from Alexander duality: the complement of a circle embedded in the D-sphere has infinite cyclic first homology precisely when the ambient dimension is three. The statement is declared as an axiom that matches the already-proved result in Verification.Dimension; the full algebraic-topology argument is treated as external classical material.

proof idea

This is a definition module, no proofs. It simply declares the topological veto axiom in the form required by the sibling theorems that appear later in the same file.

why it matters in Recognition Science

The module supplies the dimension-dependent linking constraint that the sibling results (linking_requires_D3, finite_capacity_veto, etc.) rely upon. It fills the F6.1.1/1.2 step of the foundation paper by encoding the topological reason that integer linking is possible only for D = 3, thereby supporting the enforcement of three spatial dimensions throughout the Recognition framework.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)