cube_uniqueness
plain-language theorem explainer
cube_uniqueness establishes that nonzero linking occurs exclusively in three dimensions, confirming the cube Q₃ as the unique linking-compatible polytope in the Recognition Science framework. A physicist constructing discrete models from topological constraints would cite this to exclude other dimensionalities. The proof relies on direct unfolding of the linkingNumber definition followed by conditional case splitting on whether D equals 3.
Claim. For any natural number $D$, the linking number in $D$ dimensions is nonzero if and only if $D=3$.
background
The Meta.LedgerUniqueness module resolves why the Recognition Science ledger must select specifically φ, the three-dimensional cube Q₃, and an eight-tick cycle. For the dimensional component the constraint is irreducible topological linking: D=2 admits no linking while D≥4 produces only trivial linking. This builds directly on SpectralEmergence.of, whose doc-comment states that Q₃ simultaneously forces SU(3)×SU(2)×U(1) gauge content (sector dimensions summing to 6), exactly three particle generations (from face-pair count), and 24 chiral fermion flavors (=D×2^D). The linkingNumber function encodes the indicator of whether a given dimension supports such linking structure.
proof idea
The proof introduces an arbitrary natural number D and splits the biconditional. In the forward direction it unfolds linkingNumber and splits on the if-condition for D=3, yielding the equality or a contradiction. In the reverse direction it rewrites D to 3 and simplifies the unfolded definition to a nonzero value.
why it matters
This theorem completes the uniqueness argument for the three-dimensional cube required by the Gap 9 resolution in the module documentation. It supports the main claim that any discrete conservative system is isomorphic to the RS ledger with φ, Q₃, and the 8-tick cycle. In the framework it realizes the T8 forcing of exactly three spatial dimensions. The parent result is the overall ledger uniqueness combining this with phi_unique_fixed_point and eight_tick_minimal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.