phase_functions_finite
plain-language theorem explainer
The 8-tick phase space admits exactly 8^8 functions from phases to phases. Researchers deriving the physical Church-Turing thesis from Recognition Science cite this to bound ledger transitions inside a finite computable set. The proof is a one-line term simplification that unfolds the definition of Phase as Fin 8.
Claim. Let $Φ$ be the phase space with eight elements. The cardinality of the set of all functions $Φ → Φ$ equals $8^8$.
background
The module derives the Physical Church-Turing Thesis from Recognition Science's discrete ledger structure. Each ledger entry evolves under the 8-tick operator on a discrete phase space, with finite memory per tick and J-cost minimization mapping finite states to finite states. Upstream, the EightTick module supplies the phase definition: noncomputable def phase (k : Fin 8) : ℝ := (k : ℝ) * Real.pi / 4, establishing periodicity with period 2π.
proof idea
The proof is a term-mode one-liner that applies simp to the abbreviation Phase := Fin 8. Once Phase is recognized as a finite type with eight elements, the cardinality of the function space is immediate from the definition of Fintype.card.
why it matters
This result feeds the IC-003 certificate, which lists it explicitly to confirm that RS dynamics remain within Turing-machine bounds. It fills the finite-functions step in the module's derivation of the physical Church-Turing thesis and relies on the eight-tick octave (T7) from the forcing chain. The downstream certificate string records it as part of the derived status for Church-Turing physics structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.