cube_uniqueness
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute the explicit nonzero value of the linking number in three dimensions.
- Does not demonstrate existence of linking; only characterizes when it is nonzero.
- Does not apply to linking structures outside the cube polytope.
- Does not consider dimensions outside the natural numbers.
- Does not address compatibility with the J-cost function or phi-ladder.
formal statement (Lean)
136theorem cube_uniqueness :
137 ∀ D : ℕ, (linkingNumber D ≠ 0) ↔ D = 3 := by
proof body
Term-mode proof.
138 intro D
139 constructor
140 · intro h
141 unfold linkingNumber at h
142 split_ifs at h with hD
143 · exact hD
144 · contradiction
145 · intro h
146 rw [h]
147 unfold linkingNumber
148 simp
149
150/-! ## 8-Tick Uniqueness -/
151
152/-- A Gray code cycle of length T on D dimensions. -/