RSCompatibleDimension
plain-language theorem explainer
A spatial dimension D is RS-compatible when it admits nontrivial linking of closed curves on the D-sphere, satisfies EightTickFromDimension D = 8, and has 2^D dividing the synchronization period. Researchers proving that spatial dimension is forced to equal 3 in the Recognition Science framework cite this predicate as the interface for the uniqueness argument. The declaration is a structure definition that packages the three forcing conditions without further proof obligations.
Claim. Let $D$ be a natural number. Then $D$ is RS-compatible if $S^D$ admits disjoint $S^1$-embeddings with nonzero linking number, $2^D = 8$, and $2^D$ divides the gap-45 synchronization period.
background
In the Dimension Forcing module, spatial dimension is the natural number $D$. SupportsNontrivialLinking $D$ is defined as SphereAdmitsCircleLinking $D$, which holds precisely when Alexander duality gives a nontrivial linking group (i.e., only for $D=3$). EightTickFromDimension $D$ is $2^D$ and the constant eight_tick is 8. The gap_sync condition requires $2^D$ to divide sync_period, which equals 360 under the gap-45 cycle.
proof idea
This is a structure definition that directly encodes the three conditions: linking via SupportsNontrivialLinking, equality EightTickFromDimension $D$ = eight_tick, and the divisibility gap_sync. No lemmas or tactics are invoked; it functions as the interface type for downstream results.
why it matters
RSCompatibleDimension serves as the central predicate for the dimension forcing theorem dimension_forced, which asserts a unique $D$ satisfying the structure. It packages the topological linking requirement and the eight-tick/gap-45 synchronization from the module documentation, directly enabling D3_compatible, dimension_unique, and why_D_equals_3. In the Recognition Science framework it implements the T8 step that forces $D=3$ from the eight-tick octave and Alexander duality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.