pith. sign in
module module high

IndisputableMonolith.RRF.Hypotheses.EightTick

show as:
view Lean formalization →

This module defines Phase and supporting predicates for the 8-beat cycle in Recognition Science's RRF hypotheses. QFT and quantum measurement derivations cite it as the source of the discrete phase structure. It supplies type definitions, lock/balance partitions, and cycle navigation functions without theorems or proofs.

claimLet $\text{Phase}$ be an element of the 8-beat cycle. Define $\text{isLock}(p)$ and $\text{isBalance}(p)$ as predicates that partition the cycle, with $\text{lock_balance_disjoint}$ and $\text{lock_balance_partition}$ ensuring mutual exclusivity and coverage. Cycle operations $\text{next}$ and $\text{prev}$ satisfy $\text{next_prev}$ as an involution.

background

Recognition Science organizes state evolution via the eight-tick octave (T7), a period-8 structure. This module introduces Phase as the basic object in that cycle together with lock and balance subsets. It imports Fin, ZMod, and Real to support modular indexing and real-valued balance measures.

The sibling definitions supply the partition into lock_start/lock_end and balance_start/balance_end intervals, plus the isLock and isBalance predicates. These objects stand as explicit physical hypotheses rather than derived theorems.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the 8-tick phase structure required by QFT.CPTInvariance (CPT invariance from ledger symmetry), QFT.SpinStatistics (spin-statistics theorem from 8-tick phase), and Quantum.Measurement.WavefunctionCollapse (measurement postulate from ledger structure). It sits under the RRF.Hypotheses umbrella, which collects physical claims that carry 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)