D2_no_linking
plain-language theorem explainer
Dimension 2 excludes nontrivial linking of closed curves in the Recognition Science ledger model. Researchers working on topological conservation cite this to rule out planar geometries from ledger constructions. The proof is a one-line term that applies the general linking-requires-D3 lemma to the assumption and derives an immediate numerical contradiction.
Claim. The two-dimensional sphere $S^2$ does not admit disjoint embeddings of circles with nonzero linking number (equivalently, the reduced cohomology group vanishes).
background
The DimensionForcing module establishes that spatial dimension D=3 is forced by the Recognition Science framework through four independent arguments. The linking argument uses a topological predicate: a dimension supports nontrivial linking precisely when the sphere admits disjoint circle embeddings whose linking number is nonzero, as detected by Alexander duality (reduced homology of the complement is isomorphic to the integers if and only if D=3). SupportsNontrivialLinking is defined directly as SphereAdmitsCircleLinking and is independent of the eight-tick period. The upstream theorem linking_requires_D3 states that any dimension satisfying the predicate must equal 3; its proof rests on the classical Alexander duality isomorphism without reference to cost functions or the H reparametrization.
proof idea
The proof is a one-line term-mode wrapper. It assumes SupportsNontrivialLinking 2, feeds this hypothesis into the upstream lemma linking_requires_D3 to obtain the equality D=3, and then invokes norm_num to produce the contradiction 2=3.
why it matters
This theorem supplies the D=2 case in the linking argument that forces D=3 as the unique dimension permitting stable topological conservation. It completes the exhaustive case analysis (D=1 collinear, D=2 Jordan separation, D=3 Hopf link, D>=4 general position) that appears in the module's four-argument structure for T8. The result is cited by any downstream construction that requires a ledger to carry non-trivial linking information, such as the simplicial ledger or the eight-tick synchronization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.