Pith. sign in
module module high

IndisputableMonolith.Foundation.EightTick

show as:
view Lean formalization →

Defines the eight discrete recognition phases at angles kπ/4 for k = 0..7, the algebraic skeleton of the T7 eight-tick octave. Supplies parity predicates, the cyclic next-phase map, complex phase factors, and the Z/8Z generation facts used throughout spin-statistics, cycle operators, and complex-structure forcing. Mostly definitional with short algebraic identities (eighth roots of unity).

claimThe eight-tick phase set is $\{\,e^{i k \pi/4}: k=0,\ldots,7\,\}$ on the unit circle, with period $8$, even/odd tick predicates, successor map $k\mapsto k+1\bmod 8$, and the identities $\omega^8=1$, $\omega^4=-1$, $\omega^0=1$ for $\omega=e^{i\pi/4}$. These generate the cyclic group $\mathbb{Z}/8\mathbb{Z}$.

background

Recognition Science forces an eight-tick temporal octave (forcing chain T7): the minimal closed recognition cycle has period $2^3=8$, matching the Gray-code Hamiltonian cycle on the cube $Q_3$. Time is counted in the RS-native quantum $\tau_0=1$ tick from Constants.

This module packages that discrete clock as concrete phase data. The primary object is the phase index $k\in{0,\ldots,7}$ with geometric realization $e^{i k\pi/4}$. Even and odd ticks split the octave into two 4-tick half-cycles; the successor map advances one tick. Complex exponentials of these phases are the characters of the cycle.

Sibling facts record the standard eighth-root identities and that the eight ticks generate $\mathbb{Z}/8\mathbb{Z}$. Downstream spin-statistics work treats a full $2\pi$ rotation as four ticks for spin-$1/2$ and eight ticks for integer spin.

proof idea

Definition module with short algebraic lemmas, not a long derivation. Phases, parity predicates, successor, and complex exponentials are introduced by definition. Identities such as $\omega^8=1$, $\omega^4=-1$, and $\omega^0=1$ are immediate from the exponential form (or from Mathlib roots-of-unity facts). Generation of $\mathbb{Z}/8\mathbb{Z}$ is the standard cyclic-group fact for a primitive eighth root. No deep tactic scripts; the content is the shared vocabulary for later operator and statistics modules.

why it matters in Recognition Science

Anchors T7 in the forcing chain: every later construction that needs a discrete eight-fold clock imports this module. ComplexStructureForcing uses the 8-tick shift to show diagonalization over $\mathbb{R}$ is impossible, so complex structure is forced. CycleOperator builds the unitary $\hat R$ on $\mathbb{C}^8$ from the Gray-code cycle and derives CKM structure from it. SpinStatistics proves spin-$1/2$ anticommutation (phase $-1$ after 4 ticks / $2\pi$) and integer-spin commutation from the same octave. QuantumLedger ties ledger entries to quantum states on this clock; cosmology partition kernels and information-theoretic modules (Church-Turing, error correction) reuse the tick structure as the discrete time base.

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)