eight_tick
plain-language theorem explainer
The eight-tick period is defined as the natural number 8. Researchers tracing the Recognition Science derivation of spatial dimension D=3 cite this constant when connecting ledger cycle length to 2^D. The definition is a direct constant assignment that supports reflexivity steps in compatibility theorems.
Claim. The eight-tick period equals $8$.
background
The Dimension Forcing module proves D=3 is forced by the RS framework through topological linking, gap-45 synchronization, and spinor structure. The eight-tick period is the ledger coverage length 2^D specialized at D=3. Upstream results define gap as the product of closure and fibonacci factors equaling 45, with the doc-comment noting 'The 8-tick period (from ledger coverage of 2^D with D=3)'. The synchronization condition requires lcm(8,45)=360, which isolates D=3 via 2^3=8 and SO(3) periodicity.
proof idea
This is a direct definition that assigns the constant 8. Downstream proofs apply it by reflexivity, as in eight_tick_is_2_cubed, and unfold the name in eight_tick_forces_D3 to reduce the hypothesis to power_of_2_forces_D3.
why it matters
This definition supplies the eight-tick octave from the T7 step of the forcing chain, enabling T8 to conclude D=3. It feeds into downstream results such as D3_compatible, which builds RSCompatibleDimension 3 using eight_tick := rfl, and eight_tick_forces_D3. The value closes the gap-45 synchronization where 45 is the cumulative phase over a closed 8-tick cycle, yielding the 360-degree periodicity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
All fermion masses and α from one equation and the cube
"T7 (Minimal period 8): the shortest closed Hamiltonian path on Q3 has length 8, giving the octave offset Tmin = −8."