dimension_unique
plain-language theorem explainer
The theorem shows that any natural number D satisfying the RS-compatibility conditions must equal three. Researchers deriving spatial dimensionality from the Recognition Science forcing chain cite this uniqueness step to close the T8 argument. The proof is a one-line term that destructures the compatibility hypothesis and applies the linking-requires-D3 lemma.
Claim. If a natural number $D$ satisfies the RS-compatibility conditions (supports non-trivial linking, eight-tick period equals eight, and $2^D$ divides the synchronization period), then $D=3$.
background
Dimension is the natural number representing spatial dimension. RSCompatibleDimension D is the structure requiring three properties: SupportsNontrivialLinking D for ledger conservation, EightTickFromDimension D equal to the eight-tick constant, and $2^D$ dividing sync_period for gap-45 synchronization. The DimensionForcing module proves D=3 is forced by the RS framework via topological linking and synchronization arguments. Upstream, linking_requires_D3 states that SupportsNontrivialLinking D implies D=3, obtained from Alexander duality (Hatcher Thm 3.44) without using the eight-tick or gap-45 conditions.
proof idea
The proof is a one-line term-mode wrapper. It introduces the RSCompatibleDimension hypothesis, extracts its linking component, and applies linking_requires_D3 directly to obtain D=3. No further tactics or reductions are needed.
why it matters
This uniqueness result is invoked inside dimension_forced to prove existence and uniqueness of an RS-compatible dimension. It completes the T8 step of the forcing chain by showing D=3 is the only value compatible with ledger conservation, making the eight-tick octave and gap-45 synchronization consequences of the framework rather than premises. The module documentation notes that D is now determined with no free parameter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.