cube_uniqueness
plain-language theorem explainer
The theorem states that the linking number is nonzero precisely when the dimension equals three. Researchers justifying the three-dimensional cube in discrete ledger models would cite this to enforce uniqueness of the linking topology. The argument reduces to unfolding the linking number definition and performing case analysis on whether the dimension is three.
Claim. For every natural number $D$, the linking number in dimension $D$ is nonzero if and only if $D=3$.
background
Module LedgerUniqueness resolves why any discrete conservative system must adopt the golden ratio, the three-dimensional cube Q₃, and an eight-tick cycle. The cube is forced by the requirement of irreducible topological linking: dimension two admits none while dimension four or higher yields only trivial linking. The local setting is the main theorem that every such system is isomorphic to the RS ledger with these three components.
proof idea
The term proof introduces D and splits the biconditional. Forward direction unfolds linkingNumber, splits the if-then-else on whether D equals three, and extracts the equality or reaches contradiction. Reverse direction rewrites the assumption D=3 into the definition and simplifies to obtain nonzero.
why it matters
This result supplies the uniqueness step for Q₃ inside the ledger uniqueness module, directly supporting the claim that the cube is the unique linking-compatible polytope. It aligns with the T8 forcing of three spatial dimensions and feeds the overall isomorphism theorem for the RS ledger. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.