linkingNumber
plain-language theorem explainer
The linking number function returns 1 precisely when the spatial dimension equals 3 and 0 in every other dimension, isolating the topological property that only three-dimensional space supports irreducible linking of closed curves. Researchers proving ledger uniqueness in Recognition Science cite this definition to rule out alternative dimensions in the Gap 9 argument. The implementation consists of a direct conditional check on the dimension input.
Claim. Let $l(D)$ be the linking number for curves in dimension $D$. Then $l(D) = 1$ if $D = 3$ and $l(D) = 0$ otherwise. This encodes that curves in $D=2$ always separate, non-trivial linking of 1-spheres occurs in $D=3$ (as with the Hopf link), and unlinking remains possible for all $D ≥ 4$.
background
The Ledger Uniqueness module resolves the objection that other discrete conservative structures might exist besides the Recognition Science ledger. It shows that the golden ratio, the three-dimensional cube, and the eight-tick cycle are each the unique solution to their respective forcing constraints. The linking number supplies the invariant that forces the spatial dimension to be exactly three.
proof idea
The definition is a direct case distinction on the natural-number input: it returns 1 exactly when the dimension equals 3 and 0 in all other cases. No upstream lemmas are invoked; the body is a simple conditional that serves as the base for the dimension-uniqueness theorems.
why it matters
This definition is invoked by the parent theorems complete_ledger_uniqueness and cube_uniqueness, which together close Gap 9 by proving that the Recognition Science ledger is the only discrete conservative structure. It supplies the concrete linking invariant required for the dimension step in the module's resolution of the uniqueness objection. The construction aligns with the forcing-chain landmark that selects three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.