pith. machine review for the scientific record. sign in
def definition def or abbrev high

next

show as:
view Lean formalization →

Defines the cyclic successor operation on phases within the 8-beat discretization. Researchers modeling periodic traces in Recognition Science cite it when advancing through LOCK and BALANCE segments of the cycle. The implementation is a direct one-line assignment that increments the underlying Fin 8 element.

claimLet $p$ belong to the cyclic phase set $P = Fin 8 = {0,1,2,3,4,5,6,7}$. The successor function satisfies $next(p) = p + 1$ (modulo 8).

background

The module encodes the explicit hypothesis that folding and recognition traces exhibit 8-phase periodicity, with phases 0-3 assigned to LOCK (structure formation) and phases 4-7 assigned to BALANCE (equilibration). Phase is introduced as the finite type Fin 8. Upstream results supply the angular realization: Foundation.EightTick.phase maps each index k in Fin 8 to kπ/4, while ChurchTuringPhysicsStructure.Phase and RiemannHypothesis.Wedge.phase reuse the identical Fin 8 carrier for information-theoretic and complex-phase contexts.

proof idea

One-line definition that applies the built-in addition operation on Fin 8, which automatically performs the required modular reduction.

why it matters in Recognition Science

It supplies the successor needed to realize the eight-tick octave (T7) of the forcing chain and is invoked by forty downstream results, including bimodal_ratio_gt_thirty in PulsarPeriodFromRung and normalizedRadius together with ionization_monotone_within_period in the chemistry modules. The module documentation presents the construction as the testing interface for the 8-tick hypothesis, leaving open the falsification route via observed traces that prefer a different cycle length.

scope and limits

formal statement (Lean)

  63def next (p : Phase) : Phase := p + 1

proof body

Definition body.

  64
  65/-- Predecessor phase (cyclic). -/

used by (40)

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

… and 10 more

depends on (4)

Lean names referenced from this declaration's body.