EightTickFromDimension
plain-language theorem explainer
The definition that sets the eight-tick period to 2^D for spatial dimension D. Researchers deriving that the Recognition Science ledger forces exactly three dimensions cite this mapping when equating the cycle length to eight. It is implemented as a direct power expression with no lemmas or tactics.
Claim. For spatial dimension $D$, the eight-tick period equals $2^D$.
background
In the Dimension Forcing module, spatial dimension is an abbreviation for the natural numbers. The eight-tick period captures the minimal cycle length for simplicial recognition loops in a D-dimensional ledger. The module develops four arguments that only D=3 satisfies both nontrivial topological linking (via Alexander duality) and synchronization between the eight-tick cycle and the 45-tick cumulative phase, where lcm(8,45)=360.
proof idea
This declaration is a direct definition that returns the power 2 raised to the input dimension. No lemmas are applied and no tactics are used.
why it matters
The definition supplies the expression used by eight_tick_forces_D3 to conclude D=3 from equality to eight ticks, and by physical_eight_tick to verify the value 8 at D=3. It encodes the T7 eight-tick octave landmark of the framework, where 2^D must equal 8 to synchronize with the gap-45 phase. It supports the uniqueness claim in why_D_equals_3 that combines this period with spinor structure and linking conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.