utm_exists
plain-language theorem explainer
Recognition Science asserts existence of a universal Turing machine to ground derivation of the Church-Turing thesis from ledger dynamics. Researchers modeling physical computation would cite it when connecting 8-tick ledger updates to universal gate sets. The proof is a one-line term that reduces directly to the inhabited proposition True.
Claim. There exists a universal Turing machine.
background
The module INFO-009 derives the Church-Turing thesis from RS ledger universality: any effectively computable function is realized by sequences of ledger updates. The ledger supplies state (configuration), transition (8-tick phase update), memory (infinite entries), and program (initial pattern). Upstream results supply the time quantum tick (fundamental RS time unit with one octave equal to 8 ticks) and phase (kπ/4 for k in Fin 8, periodic with period 2π).
proof idea
The proof is a term-mode proof consisting of the single term trivial.
why it matters
This theorem marks the existence claim required for the module's derivation of the Church-Turing thesis from ledger universality, as described in the Foundations paper proposition on the physical basis of universal computation. It connects directly to the eight-tick octave (T7) supplying a universal gate set. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.