Phase
plain-language theorem explainer
The Phase abbreviation supplies the finite set of eight elements that indexes discrete states within each fundamental octave of Recognition Science ledger dynamics. Researchers deriving the physical Church-Turing thesis or bounding state transitions per tick cite this construction to enforce the eight-phase periodicity. The definition is a direct alias to Fin 8 with no additional structure or lemmas required.
Claim. Let $P$ denote the finite phase space consisting of the integers from 0 to 7 that label the discrete states inside one 8-tick cycle of the ledger.
background
The module derives the physical Church-Turing thesis from the discrete ledger structure whose dynamics are governed by an 8-tick operator on a finite phase space. Upstream, the constant tick is defined as the fundamental RS time quantum with the property that one octave equals exactly 8 ticks. The LedgerFactorization and PhiForcingDerived structures supply the J-cost minimization that maps states within this bounded space.
proof idea
This is a direct abbreviation that aliases the standard finite type Fin 8. No lemmas or tactics are invoked; the definition follows immediately from the requirement for an eight-phase cycle stated in the module doc-comment.
why it matters
The abbreviation supplies the discrete phase space required by the eight-tick octave (T7) in the forcing chain. It is referenced downstream in ticksToOctaves, PhaseLocked structures, J_bit, and sc_gap_scale. The construction closes the finite-state requirement for the physical Church-Turing thesis, ensuring all RS dynamics remain within BQP and inherit undecidability from Turing machines.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.