eight_tick_step_computable
plain-language theorem explainer
Any transition map on the eight-phase space admits an explicit finite lookup table. Researchers deriving the physical Church-Turing thesis from Recognition Science ledger dynamics cite the result to place exact 8-tick steps inside classical computability. The argument is a one-line wrapper that instantiates the general finite-function computability lemma on the Phase type.
Claim. For any function $step : Phase → Phase$ where $Phase$ is the set of eight phases, there exists a finite set $T ⊆ Phase × Phase$ such that for every phase $p$ there is a phase $p'$ with $(p,p') ∈ T$ and $step(p) = p'$.
background
The module derives the physical Church-Turing thesis from the discrete ledger structure of Recognition Science. Phase is the 8-tick phase space, the finite set Fin 8 whose elements label the successive states in one octave of the J-cost dynamics. The module imports the general fact that every function between finite types is encodable by a Finset table, together with the ledger factorization and phi-forcing structures that force the phase space to be exactly eight elements.
proof idea
The proof is a one-line wrapper that applies the finite_function_is_computable lemma to the Phase type, supplying the required Finset table by exhaustive enumeration of the eight input-output pairs.
why it matters
The declaration supplies the exact-computability half of the IC-003 certificate that assembles the physical Church-Turing thesis for RS dynamics. It rests on the eight-tick octave (T7) that fixes the phase space cardinality and feeds directly into the downstream certificate string that records the finite phase-space and finite-function facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.