prev
prev supplies the cyclic predecessor on phases in the 8-beat discretization of Recognition Science RRF hypotheses. Modelers of ledger schedules, cone bounds, and phi-ladder constructions cite it when stepping backward through the cycle. The definition is a direct one-line subtraction on Fin 8 that inherits modular arithmetic from the phase type.
claimLet $p$ be an element of the cyclic group of order 8. The predecessor phase is $p-1$ (modulo 8).
background
The module formalizes the explicit 8-tick hypothesis that observed folding and recognition traces exhibit 8-phase periodicity, with phases 0-3 assigned to LOCK (structure formation) and 4-7 to BALANCE (equilibration). Phase is the type Fin 8, matching the upstream definition in ChurchTuringPhysicsStructure that supplies the 8-tick phase space. The hypothesis is presented as a testable interface for LNAL bytecode rather than a foundational axiom.
proof idea
This is a one-line definition that applies subtraction by 1 directly to the Fin 8 input, relying on the built-in modular arithmetic of Mathlib's Fin type.
why it matters in Recognition Science
The definition supports the eight-tick octave (T7) by furnishing the backward step required for cycle navigation. It is invoked by next_prev to prove that next and prev are mutual inverses, and appears in downstream sites including phiPow (phi-ladder construction), ballFS and card_ballFS_succ_le (causality cone bounds), normalizedRadius (atomic radii), and ledger run (posting schedules). It closes a basic interface piece for the RRF discretization hypothesis.
scope and limits
- Does not prove the 8-tick periodicity of any observed trace.
- Does not assign physical or computational meaning to individual phases.
- Does not extend the cycle length beyond eight phases.
- Does not supply transition probabilities or metrics between phases.
formal statement (Lean)
66def prev (p : Phase) : Phase := p - 1
proof body
Definition body.
67