H_LinkingDimensionUniqueness
plain-language theorem explainer
H_LinkingDimensionUniqueness defines the proposition that the linking number of curves is nonzero precisely when the ambient dimension equals three. Researchers closing the uniqueness gap for the Recognition Science ledger cite it to establish why the cube must be three-dimensional rather than two or four or higher. The definition follows directly from the piecewise construction of linkingNumber, which returns one only for D=3 and zero otherwise.
Claim. $forall D in mathbb{N} (D geq 2 implies (text{linking number of curves in dimension }D neq 0 iff D=3))$
background
The module LedgerUniqueness addresses the objection that discrete conservative systems might admit structures other than phi, the 3-cube, and the 8-tick cycle. It resolves the dimension question by isolating the constraint of irreducible topological linking: D=2 admits no linking between curves, while D greater than or equal to 4 permits unlinking, leaving only D=3 with a nontrivial invariant (the Hopf link). The upstream definition of linkingNumber encodes this behavior explicitly: linkingNumber D equals 1 if D=3 and 0 otherwise, with the accompanying note that D=2 yields always zero (curves separate), D=3 yields non-trivial linking, and D greater than or equal to 4 yields always zero (unlinking possible).
proof idea
The declaration is a direct definition that states the biconditional for all D greater than or equal to 2. It applies the upstream piecewise definition of linkingNumber without further lemmas or tactics, simply asserting that the nonzero case occurs exclusively at D=3.
why it matters
This supplies the uniqueness constraint for the three-dimensional cube inside the Ledger Uniqueness module. It supports the module's main theorem that any discrete conservative system is isomorphic to the RS ledger with phi, Q3, and the 8-tick cycle. The declaration fills the T8 step forcing D=3 spatial dimensions and leaves open the explicit proof that the linking invariant for 1-spheres holds only in D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.