phase_space_bounded
plain-language theorem explainer
The declaration establishes that the phase space in one Recognition Science tick contains at most 8 phases. Researchers deriving physical Church-Turing bounds from discrete ledger dynamics would cite this to cap resources per step and rule out hypercomputation. The proof is a direct term reduction that unfolds the phase count definition and normalizes the resulting numerical inequality.
Claim. Let $N$ denote the number of phases in one 8-tick cycle. Then $N ≤ 8$.
background
Recognition Science models physical processes via a discrete ledger whose state transitions are governed by an 8-tick operator. The definition numPhases fixes this count at exactly 8, matching the octave period that arises from the self-similar fixed point in the forcing chain. Module documentation states that each tick therefore updates only a finite number of ledger entries, yielding computable maps from finite state to finite state and preventing any jump to infinity.
proof idea
The proof is a one-line term wrapper. It unfolds the definition of numPhases (which is the constant 8) and applies norm_num to discharge the inequality 8 ≤ 8.
why it matters
This is IC-003.7 and supplies the finite-phase premise used by the downstream IC-003 certificate. It instantiates the eight-tick octave (T7) from the forcing chain, confirming that RS dynamics remain within Turing-machine approximability. The result closes one route to hypercomputation by bounding resources per tick.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.