eight_tick_step_computable
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not claim that phi-ladder quantities with irrational exponents are exactly computable.
- Does not decide the halting problem for arbitrary RS ledger sequences.
- Does not extend to continuous-time or infinite-state limits of the dynamics.
formal statement (Lean)
147theorem eight_tick_step_computable (step : Phase → Phase) :
148 ∃ (table : Finset (Phase × Phase)),
149 ∀ p : Phase, ∃ p' : Phase, (p, p') ∈ table ∧ step p = p' :=
proof body
Term-mode proof.
150 finite_function_is_computable (α := Phase) (β := Phase) step
151
152/-! ## VI. RS Complexity Classes -/
153
154/-- **THEOREM IC-003.12**: φ is irrational, so RS dynamics involving φ-ladders
155 cannot be exactly computed by finite rational algorithms.
156 This places exact RS computations in the class of "real number computations"
157 (beyond classical Turing machines for exact values). -/