pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Information.ChurchTuring

show as:
view Lean formalization →

The Information.ChurchTuring module formalizes Turing machines and the Church-Turing thesis inside Recognition Science. It supplies configurations, transitions, a universal TM, and ledger links all synchronized to the discrete 8-tick clock. Researchers modeling physical computation on RS time quanta cite it to ground universality. The module is definitional, importing Constants and EightTick with no internal proofs.

claimA Turing machine configuration is a state-tape-head triple operating under the 8-tick cycle with each transition advancing by the RS time quantum $τ_0 = 1$ tick; the module also defines a universal TM and the physical Church-Turing thesis over this clock.

background

The module sits in the Information domain and imports the RS time quantum $τ_0 = 1$ tick from Constants together with the 8-tick structure from EightTick. The latter supplies the discrete clock whose phases run through 0, π/4, π/2, 3π/4, π, 5π/4, 3π/2, 7π/4. It introduces the sibling definitions TuringMachine (a configuration), Transition, UniversalTM, ledger_follows_8tick, physical_ct_thesis, and halting_undecidable, all expressed in RS-native units.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the computational primitives that feed physical_ct_thesis, ledger_universal, and eight_tick_universal_gates. It realizes the eight-tick octave (T7) for discrete computation, enabling the claim that physical processes are simulable by a universal TM on the RS clock. It touches the open question of uncomputables within the discrete framework.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (16)