pith. sign in
module module high

IndisputableMonolith.RRF.Hypotheses.EightTick

show as:
view Lean formalization →

EightTick defines the Phase datatype for the 8-beat cycle together with lock and balance partitions in the RRF hypotheses. QFT modules on CPT invariance and spin-statistics import it to access the discrete symmetry structure. The module contains only definitions and no theorems or proofs.

claimPhase denotes an element of the 8-element cycle equipped with predicates isLock, isBalance and successor maps next, prev satisfying the partition and disjointness conditions lock_balance_partition and lock_balance_disjoint.

background

The module belongs to RRF.Hypotheses, the umbrella file that collects explicit physical claims rather than proven theorems. It introduces the eight-tick octave (T7) through the Phase type and the auxiliary functions lock_start, lock_end, balance_start, balance_end. The sibling definitions next_prev and lock_balance_disjoint enforce the cyclic order and the separation into two intervals of four ticks.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

EightTick supplies the 8-tick phase structure to QFT.CPTInvariance (CPT invariance from ledger symmetry), QFT.SpinStatistics (spin-statistics theorem from 8-tick phase), and Quantum.Measurement.WavefunctionCollapse (measurement problem from ledger structure). It also populates the RRF.Hypotheses umbrella that documents physical claims with explicit falsification criteria.

scope and limits

used by (4)

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

declarations in this module (19)