discrete_ledger_computable
plain-language theorem explainer
Any transition t on the finite set of 256 discrete ledger states (Fin 8 to Bool) admits an explicit finite lookup table of pairs. Recognition Science researchers deriving the physical Church-Turing thesis cite this to bound RS dynamics inside Turing machines. The term proof constructs the table directly as the image of the universal Finset under the graph map of t and verifies membership by the image introduction lemma.
Claim. Let $S$ be the finite set of all functions from a set of eight indices to the Boolean values. For any function $t: S → S$ there exists a finite collection $T ⊂ S × S$ such that for every $s ∈ S$ there is an $s' ∈ S$ with $(s, s') ∈ T$ and $t(s) = s'$.
background
DiscreteLedgerState is defined as Fin 8 → Bool, the set of all assignments of active/inactive flags to the eight phases of the RS octave. LedgerTransition is the type of all functions from this set to itself. The module IC-003 derives the physical Church-Turing thesis from the discrete ledger: each tick updates a finite number of entries at rate 1/τ₀, so no trans-Turing jump is possible. Upstream, DiscreteLedgerState derives Fintype and DecidableEq, supplying the finite universal set used in the construction.
proof idea
The term proof applies Finset.image to the map s ↦ (s, t s) over Finset.univ, then for each s invokes Finset.mem_image.mpr with the witness s and the reflexivity proof that t s equals the second component. No additional lemmas beyond the standard Finset image membership rules are required.
why it matters
This is theorem IC-003.3 inside the Church-Turing derivation. It supplies the finite-table step that lets the module conclude every RS ledger transition is Turing-computable and that physical processes remain inside BQP. It closes the finite-state half of the argument that begins from the eight-tick operator (T7) and the discrete phase space. The sibling result church_turing_physics_from_ledger uses the same finite-state premise to embed RS dynamics into Turing machines.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.