Q3_unique_linking_dimension
plain-language theorem explainer
The theorem proves that for any natural number D at least 2 the linking number is nonzero precisely when D equals 3. Researchers closing the uniqueness gap for discrete conservative systems cite it to rule out alternative spatial dimensions. The proof is a direct case split on the piecewise definition of linkingNumber that extracts the equality in one direction and substitutes the assumption in the other.
Claim. For every natural number $D$ with $D$ at least 2, the linking number of $D$ is nonzero if and only if $D$ equals 3.
background
The module addresses Gap 9 by showing that any discrete conservative ledger must be isomorphic to the RS ledger built from the golden ratio, the three-dimensional cube, and an eight-tick cycle. The key local definition is linkingNumber, which returns 1 when the dimension is exactly 3 and 0 otherwise; this encodes the topological fact that only three-dimensional space admits irreducible linking of curves (Hopf link) while D=2 separates curves and D greater than or equal to 4 permits unlinking. The upstream result linkingNumber supplies the explicit piecewise definition used throughout the argument.
proof idea
The term proof begins by introducing D and the hypothesis D greater than or equal to 2. It then constructs the biconditional by handling each direction separately. The forward direction unfolds linkingNumber and applies split_ifs to isolate the case D=3. The reverse direction unfolds linkingNumber and simplifies directly under the assumption that D equals 3.
why it matters
This declaration supplies the Q3 uniqueness step required by complete_ledger_uniqueness and rs_ledger_is_unique. It thereby closes the dimension part of the Gap 9 objection that other discrete ledgers might exist. In the Recognition framework it realizes the T8 forcing that spatial dimension equals 3, confirming that only the cube Q3 supports the required irreducible linking structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.