H_D2NoLinking
plain-language theorem explainer
Records the topological hypothesis that in two spatial dimensions any two closed curves can be separated, so irreducible linking is impossible. Dimensional-rigidity arguments cite it when ruling out D=2 as a home for Hopf-type linking penalties. The body is only a placeholder Prop (true for dummy Unit curves), not a formalized Jordan-curve argument.
Claim. Hypothesis (scaffold): in spatial dimension $D=2$, any two closed curves can be separated; equivalently, there is no irreducible linking of closed curves in the plane (Jordan-curve content).
background
Module Verification.Dimension shows that RSCounting plus 45-gap synchronization forces spatial dimension $D=3$, with the iff RSCounting_Gap45_Absolute D \leftrightarrow D=3. The path is kept arithmetic (lcm and the RecogSpec layer) so PrimeClosure stays light.
Elsewhere in the framework, $D$ is fixed to 3 by the forcing chain (T8 spatial dimensions; AlphaDerivation/GapDerivation both set D := 3 as the value forced by linking). Linking geometry is the physical reason: only three dimensions support a unique nontrivial Hopf link that can carry a recognition penalty.
This declaration is the $D=2$ side of that trichotomy. The doc-comment states the standard fact: in the plane, closed curves separate and can be pulled apart (Jordan). Sibling placeholders cover $D\ge 4$ (always unlinked by ambient isotopy) and the unique $D=3$ linking case.
proof idea
Not a proof. The definition is the Prop
∀ (C1 C2 : Unit), True,
an explicit placeholder: curve objects are stubbed as Unit, and the statement is vacuously true. A commented axiom h_d2_no_linking is left for a future discharge. Closing the scaffold means replacing the Unit dummies by real closed-curve types and citing a formalized Jordan-curve (or planar separation) theorem that implies absence of irreducible linking.
why it matters
In the Recognition dimensional story, linking selects $D=3$: the plane has no irreducible links, dimensions $\ge 4$ allow ambient unlinking, and only $D=3$ hosts a unique Hopf link. This hypothesis is the $D=2$ leg of that case split, sitting beside siblings H_D4TrivialLinking, H_ThreeDimensionalLinkingUnique, and hopf_linking_penalty.
It supports the T8 landmark (spatial dimension forced to 3) and the module-level claim that RSCounting with the 45-gap forces $D=3$. No used_by edges are wired yet; the object is still a named interface for the missing topology lemma. Open work: connect Mathlib/planar topology to "no irreducible linking" so the dimensional rigidity witness can cite a real theorem instead of a scaffold Prop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.