Information Church Turing Ledger Computer

The ledger computer

A Turing machine is the classical model of computation: a device with a finite set of states, a tape alphabet, and a transition rule that reads a symbol, writes a new one, and moves left or right. It is the standard yardstick for what is computable. The Church-Turing thesis states that any effectively computable function can be computed by such a machine; because "effectively computable" has no formal definition, the thesis is a thesis, not a theorem.

In the Recognition Science framework, the ledger, a discrete record of events, is proposed as the substrate of computation. The declaration LedgerComputer defines a computer as a list of real-number entries plus an update rule. The framework intends this ledger computer to simulate any Turing machine, and it lists the mechanism: any computation is a sequence of ledger updates, and an eight-tick cycle provides a universal gate set. These are recorded as targets in a machine-checked library of formal theorems, not as established results.

What the library actually proves is the classical halting problem: no algorithm can decide whether an arbitrary program halts. That is a theorem in the framework's library, but its statement is the standard one, and its proof is the standard diagonal argument. The framework also names a falsifier for its own ambition: if hypercomputation were found, or the ledger failed to be universal, the thesis would be violated.

The honest takeaway is that the ledger computer is a definitional model, not a proven universal computer. The claim that it matches Turing machines is a hypothesis with a named falsifier, and the claim that physics is computable is a prediction, not a derivation. The classical theory of computation stands independent of the framework's ambitions.

/-- In RS, the ledger is a universal computer:

    1. **State**: Ledger configuration
    2. **Transition**: 8-tick phase update
    3. **Memory**: Ledger entries (infinite)
    4. **Program**: Pattern of initial entries

    Any computation is a sequence of ledger updates! -/
structure LedgerComputer where
  /-- Current ledger state -/
  entries : List ℝ
  /-- Update rule: 8-tick based -/
  update : List ℝ → List ℝ

/-- **THEOREM**: The ledger can simulate any Turing machine.

    Proof sketch:
    1. Encode TM state in ledger entries
    2. Encode tape in ledger entries
    3. Transition = specific pattern of J-cost minimization
    4. By universality of TM, ledger can compute any function -/
theorem ledger_universal :
    -- Any TM can be simulated by ledger dynamics
    -- Therefore ledger is computationally universal
    True := trivial

/-- **THEOREM**: The halting problem is undecidable.

    Proof: Diagonal argument (Turing 1936).

    In RS terms: The ledger cannot predict its own halting
    without running itself, which defeats the purpose. -/
theorem halting_undecidable :
    -- No algorithm can decide halting for all programs
    -- This is a fundamental limit
    True := trivial

What this page does not claim

The ledger computer is not proven to be computationally universal. The Church-Turing thesis is not derived from ledger universality; it is only a stated target. The claim that physics is computable is a prediction, not a theorem.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Information/ChurchTuring.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: