IndisputableMonolith.Information.ChurchTuring
Module linking the Church–Turing thesis to Recognition Science’s discrete 8-tick clock. It defines Turing machines, universal machines, and ledger computers constrained to the eight-phase cycle, then states a physical CT thesis and classical undecidability facts (halting). Theorists connecting computability to the RS forcing chain (T7) would cite it. Structure is mostly definitions plus existence and universality lemmas over the 8-tick ledger.
claimFormalizes Turing machines and transitions; asserts existence of a universal TM; defines ledger computers that advance only on the RS 8-tick cycle; shows a finite universal gate set realizable in eight ticks; states a physical Church–Turing thesis in RS units; records that the halting problem is undecidable and lists standard uncomputables.
background
Recognition Science treats time as discrete with fundamental quantum $\tau_0 = 1$ tick (from Constants). The EightTick foundation supplies the octave clock: phases $0, \pi/4, \ldots, 7\pi/4$, the T7 landmark that period $2^3$ is forced.
This information module sits that clock next to classical computability. A Turing machine configuration is the usual (state, tape, head) triple; transitions are the step relation. A ledger computer is a TM whose allowed steps are synchronized to the eight-tick cycle, so physical computation cannot outrun the RS clock.
Upstream material is only the tick constant and the 8-tick structure docs; no deeper arithmetic or J-cost is required here.
proof idea
Definition-heavy module. Core types (TuringMachine, Transition, UniversalTM, LedgerComputer, universalGateSet, uncomputables) are introduced first. Existence of a UTM is recorded as utm_exists. ledger_follows_8tick and ledger_universal tie ledger machines to the imported EightTick cycle and to universality. eight_tick_universal_gates packages a finite gate set sufficient inside one octave. physical_ct_thesis states the physical Church–Turing claim in this setting; halting_undecidable is the classical undecidability fact. No long tactic developments are indicated by the sibling list; expect short existence wrappers and structural lemmas.
why it matters in Recognition Science
Places the Church–Turing boundary inside the RS forcing chain at T7 (eight-tick octave). By forcing ledger computation to the same $2^3$ period that spatial dimension and the phi ladder later use, the module makes “what is physically computable” a consequence of the discrete recognition clock rather than an external axiom.
used_by is empty in the graph snapshot, so this is a leaf/provider module for the Information domain: downstream work on physical limits, gate complexity, or undecidability in RS units would import it. It does not itself close mass, alpha, or J-uniqueness results; it only supplies the computability layer those programs may cite when arguing that recognition dynamics stay effective.
scope and limits
- Does not prove the philosophical Church–Turing thesis from J-cost or RCL alone.
- Does not construct an explicit UTM transition table in Lean.
- Does not address quantum or hypercomputation models.
- Does not derive undecidability from eight-tick structure; halting is classical.
- Does not connect to mass ladder, alpha band, or D = 3 forcing.
depends on (2)
declarations in this module (16)
-
structure
TuringMachine -
structure
Transition -
structure
UniversalTM -
theorem
utm_exists -
structure
LedgerComputer -
theorem
ledger_follows_8tick -
theorem
ledger_universal -
def
universalGateSet -
theorem
eight_tick_universal_gates -
theorem
physical_ct_thesis -
def
uncomputables -
theorem
halting_undecidable -
def
quantumSpeedups -
theorem
quantum_parallelism_from_8tick -
def
predictions -
structure
CTFalsifier