eightTick
plain-language theorem explainer
eightTick is defined as the natural number 8, which equals 2 raised to Dspatial where Dspatial equals 3. Researchers on the Recognition Science cardinality spectrum cite it as the size of the eight-tick octave. The definition is a direct constant assignment that inherits its value from the upstream definition of Dspatial.
Claim. Define eightTick as the natural number $8$, satisfying $8 = 2^{D_{spatial}}$ where $D_{spatial} = 3$.
background
The module CrossDomain.CardinalitySpectrum assembles witnesses showing that RS cardinalities form a structured spectrum generated from the cube generators {2, 3}, the configuration dimension 5, and gap45. The module doc states that every member of the spectrum admits a decomposition into RS primitives, with zero sorry or axiom in Lean. Dspatial is defined as the natural number 3, representing the three spatial dimensions.
proof idea
This is a direct definition that assigns the constant 8 to eightTick. It functions as a one-line wrapper encoding the relation eightTick = 2 ^ Dspatial via the upstream definition of Dspatial.
why it matters
This definition supplies the eight-tick cardinality required by the CardinalitySpectrumCert structure, which asserts eightTick_as_D : eightTick = 2 ^ Dspatial among other spectrum relations. It realizes the eight-tick octave (T7) forced by D = 3 spatial dimensions (T8) in the unified forcing chain. Downstream results such as eight_is_2cube and threeSixty_is_tick_gap use it to verify decompositions like 360 = eightTick * gap45.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.