pith. sign in
module module high

IndisputableMonolith.Foundation.EightTick

show as:
view Lean formalization →

The module defines the eight-tick phases as multiples of π/4, realizing the discrete time structure forced by three spatial dimensions. Researchers deriving spin-statistics or diurnal cycles cite it as the source of universal 8-fold periodicity. It consists of definitions establishing algebraic closure and periodicity properties that import only the base time quantum.

claimThe phases are the angles $kπ/4$ for $k=0,1,…,7$, extended by periodicity with period 8 in the discrete tick index and satisfying the algebraic relations of an eighth root of unity.

background

Recognition Science obtains an eight-tick octave as step T7 of the forcing chain, where the period equals $2^D$ and $D=3$ spatial dimensions. The module imports the fundamental time quantum $τ_0=1$ tick from Constants. It introduces the phase function that maps each integer tick index to the corresponding angle $kπ/4$, together with derived periodicity and power identities.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the eight-tick cadence required by SpinStatistics for the spin-statistics theorem, by Climate.DiurnalEightTick for the 24-hour cycle, and by the Information modules for error-correction bounds. It directly implements the T7 eight-tick octave landmark of the forcing chain. Downstream modules treat it as the origin of the 8-fold phase structure forced by spatial dimensionality.

scope and limits

used by (18)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (13)