LedgerComputer
plain-language theorem explainer
LedgerComputer defines a structure modeling universal computation in Recognition Science as a ledger state (list of reals) paired with an 8-tick phase update function. Researchers deriving the Church-Turing thesis from physical ledger universality would cite this definition. It is a direct structure declaration with no proof steps, simply naming the state and transition components.
Claim. A LedgerComputer consists of a list of real numbers $entries$ for the current ledger configuration together with a function $update : List(ℝ) → List(ℝ)$ that applies the 8-tick phase transition.
background
The Information.ChurchTuring module derives the Church-Turing thesis from RS ledger universality: the ledger simulates any physical process, so every computation is a sequence of ledger updates. The upstream tick definition supplies the fundamental time quantum τ₀ = 1, with one octave equal to 8 ticks as the evolution period. The sibling Transition structure encodes a Turing-machine step from (state, symbol) to (new state, new symbol, direction).
proof idea
This is a structure definition that directly introduces the two fields: entries as List ℝ and update as the 8-tick-based map. No lemmas or tactics are applied; the declaration itself establishes the model.
why it matters
The structure supplies the core object for ledger-based universal computation, directly supporting the module goal of obtaining the Church-Turing thesis from RS principles. It instantiates the eight-tick octave (T7) from the forcing chain as the update mechanism. Subsequent siblings such as ledger_follows_8tick and physical_ct_thesis build on this model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.