pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.EightTick

show as:
view Lean formalization →

The EightTick module defines the discrete phases at multiples of π/4 that realize the eight-tick octave in Recognition Science. Researchers deriving spin-statistics relations or quantum error-correction bounds cite it to anchor their work in the universal time structure. The module supplies definitions for phase maps and parity predicates together with short algebraic lemmas confirming closure under eighth powers and sign flips.

claimThe phases are the angles $kπ/4$ for $k=0,1,…,7$, equipped with a periodic extension, even-tick and odd-tick predicates, and an exponential representation satisfying $e^{i8θ}=1$.

background

The module imports the fundamental time quantum τ₀ = 1 tick from Constants and operates in the Foundation domain. It encodes the eight-tick cadence required once three spatial dimensions are fixed, since 2^D = 8. Core objects include the phase function that assigns each tick index an angle, its periodic lift, and the predicates isEvenTick and isOddTick that distinguish the two sublattices of the Z_8 group.

proof idea

This is a definition module, no proofs. It introduces the phase functions and then records their immediate algebraic consequences (eighth-power identity, value at four ticks, etc.) as short lemmas.

why it matters in Recognition Science

The module supplies the eight-tick structure that downstream results rely on: SpinStatistics uses it to obtain the spin-statistics theorem, QuantumLedger connects ledger entries to quantum states, and the Information modules derive error-correction bounds and Church-Turing statements. It directly implements the T7 eight-tick octave forced by D = 3 in the unified forcing chain.

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)