no_circle_linking_low_dim
plain-language theorem explainer
The theorem establishes that the D-sphere admits no nontrivial circle linking for any natural number D at most 2. Topologists and Recognition Science researchers formalizing dimension constraints would cite this as the low-dimensional case of the Alexander duality characterization. The proof is a one-line wrapper that assumes the linking predicate, invokes the forcing lemma that linking implies D equals 3, and derives a contradiction via arithmetic.
Claim. For any natural number $D$ with $D ≤ 2$, the D-sphere does not admit nontrivial linking of embedded circles, where the linking predicate holds precisely when the reduced cohomology group $˜H^{D-2}(S¹; ℤ)$ is nontrivial.
background
The module formalizes the topological argument that nontrivial circle linking in the D-sphere exists if and only if D equals 3, replacing a prior definitional tautology with a proof from reduced cohomology axioms. SphereAdmitsCircleLinking D is defined as CircleReducedCohomologyNontrivial ((D : ℤ) - 2), which by Alexander duality (Hatcher Thm 3.44) encodes whether $˜H_1(S^D ∖ S¹; ℤ)$ is nontrivial. The upstream theorem circle_linking_forces_D3 states that SphereAdmitsCircleLinking D implies D = 3.
proof idea
The proof is a term-mode wrapper. It introduces the assumption SphereAdmitsCircleLinking D, applies the lemma circle_linking_forces_D3 to obtain D = 3, and uses the omega tactic to reach a contradiction with the hypothesis D ≤ 2.
why it matters
This declaration supplies the low-dimensional half of the biconditional that characterizes D = 3 via circle linking. It pairs with circle_linking_forces_D3 and the high-dimensional counterpart to replace the earlier tautology, aligning with the Recognition Science forcing chain step that yields D = 3. The module doc-comment cites Hatcher Theorem 3.44 as the source of the duality isomorphism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.