pith. machine review for the scientific record. sign in
def definition def or abbrev high

SphereAdmitsCircleLinking

show as:
view Lean formalization →

SphereAdmitsCircleLinking D asserts that the D-sphere permits nontrivial linking between two disjoint embedded circles. Algebraic topologists and Recognition Science researchers would cite it when deriving dimension constraints from duality. The definition is a direct one-line encoding of Alexander duality that reduces the linking predicate to nontrivial reduced cohomology of the circle in degree D-2.

claimSphereAdmitsCircleLinking(D) holds precisely when the reduced cohomology group $H̃^{D-2}(S^1;ℤ)$ is nontrivial.

background

The module replaces a prior tautological definition of circle linking with one grounded in Alexander duality. For a compact locally contractible X ⊂ S^n, duality gives H̃_q(S^n ∖ X) ≅ H̃^{n-q-1}(X). Setting X = S^1 and q = 1 yields H̃_1(S^D ∖ S^1) ≅ H̃^{D-2}(S^1), so linking is detected exactly by the reduced cohomology of the circle. CircleReducedCohomologyNontrivial(k) is defined as k = 1, matching the standard computation that H̃^k(S^1; ℤ) is nontrivial only in degree 1 (Hatcher §2.2, Thm 2.13). Upstream circle_reduced_cohomology_iff records the same equivalence as a theorem after the concrete definition closed the prior axiom.

proof idea

One-line definition that directly sets SphereAdmitsCircleLinking D to CircleReducedCohomologyNontrivial((D : ℤ) - 2). It applies the upstream definition CircleReducedCohomologyNontrivial together with the equivalence in circle_reduced_cohomology_iff to encode the Alexander duality condition without further tactics.

why it matters in Recognition Science

This definition supplies the topological predicate that alexander_duality_circle_linking, circle_linking_forces_D3, D3_admits_circle_linking, no_circle_linking_low_dim and no_circle_linking_high_dim all rely on. Those results in turn feed physical_eight_tick and spinor_eight_tick_forces_D3 in DimensionForcing. It realizes T8 of the forcing chain by grounding D = 3 in the eight-tick octave and self-similar fixed point rather than an arbitrary choice. The module documentation records that the prior axiom status is now closed.

scope and limits

formal statement (Lean)

 129def SphereAdmitsCircleLinking (D : ℕ) : Prop :=

proof body

Definition body.

 130  CircleReducedCohomologyNontrivial ((D : ℤ) - 2)
 131
 132/-! ## Theorem: Linking Characterizes D = 3 -/
 133
 134/-- **Alexander Duality Applied to Circle Linking** (Hatcher, Thm 3.44).
 135
 136Non-trivial closed-curve linking in S^D exists iff D = 3.
 137
 138**Proof structure**:
 1391. By definition, `SphereAdmitsCircleLinking D` ↔ H̃^{D-2}(S¹) nontrivial
 1402. By `circle_reduced_cohomology_iff`, this holds iff D - 2 = 1
 1413. For D : ℕ, (D : ℤ) - 2 = 1 iff D = 3
 142
 143This is a genuine theorem requiring the S¹ cohomology axiom, not a
 144definitional identity. -/

used by (12)

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

depends on (12)

Lean names referenced from this declaration's body.