eight_tick
plain-language theorem explainer
The eight-tick period is the natural number 8 arising as the ledger coverage length 2^D at spatial dimension D=3. Dimension-forcing arguments in Recognition Science cite it to close the octave and force the synchronization gap of 45. The definition is a direct constant assignment that supplies the period for downstream compatibility checks.
Claim. The eight-tick period is the natural number $8$, equal to $2^3$ and equal to the fundamental evolution period of the ledger when the spatial dimension is $D=3$.
background
The tick is the fundamental RS time quantum, defined as 1 in native units and serving as the base interval for all ledger evolution. The eight-tick period follows from the requirement that ledger coverage equals $2^D$; at $D=3$ this yields exactly 8. The module uses the fence-post principle to note that closing such a cycle requires 9 steps, whose cumulative phase sum is the triangular number 45.
proof idea
Direct definition that assigns the constant 8. It is invoked verbatim in downstream results such as eight_tick_is_2_cubed and D3_compatible to discharge the period condition.
why it matters
This supplies the eight-tick octave required at step T7 of the forcing chain. It is used by D3_compatible to verify the eight-tick and gap-sync conditions simultaneously, and by eight_tick_forces_D3 to conclude that only D=3 satisfies the ledger coverage. The definition therefore anchors the physical motivation for the 45-tick synchronization gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.