pith. sign in
def

SphereAdmitsCircleLinking

definition
show as:
module
IndisputableMonolith.Foundation.AlexanderDuality
domain
Foundation
line
129 · github
papers citing
26 papers (below)

plain-language theorem explainer

SphereAdmitsCircleLinking D is the predicate that the D-sphere admits nontrivial linking of embedded circles, defined by the reduced cohomology of the circle being nontrivial in degree D-2. Recognition Science researchers cite it when deriving spatial dimension from topology rather than by fiat. The definition is a direct one-line delegation to the circle cohomology predicate, shifting the D=3 equivalence into a separate theorem.

Claim. For $D$ a natural number, the $D$-sphere admits nontrivial linking of disjoint embedded circles precisely when the reduced cohomology group $H^{D-2}(S^1;Z)$ is nontrivial.

background

The Alexander Duality module replaces an earlier tautological definition of circle linking with one grounded in cohomology. Alexander duality (Hatcher Thm 3.44) supplies the isomorphism $H_q(S^D minus S^1) cong H^{D-2}(S^1)$ for an embedded circle; linking is detected by the first homology of the complement, which therefore equals the (D-2)th reduced cohomology of the circle. The predicate CircleReducedCohomologyNontrivial k encodes the standard computation that this group is nontrivial exactly for k=1 (Hatcher §2.2).

proof idea

One-line definition that sets the predicate equal to CircleReducedCohomologyNontrivial applied to (D cast to Z) minus 2. It directly invokes the upstream definition of CircleReducedCohomologyNontrivial as equality to 1 and the theorem circle_reduced_cohomology_iff.

why it matters

This definition supplies the topological content for alexander_duality_circle_linking, circle_linking_forces_D3, D3_admits_circle_linking, and the dimension-forcing results in DimensionForcing. It advances the Recognition Science chain by grounding T8 (D=3 spatial dimensions) in Alexander duality rather than an axiom, closing the historical scaffolding around the eight-tick octave.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.