DiscreteLedgerState
plain-language theorem explainer
The type of discrete ledger states consists of all functions assigning a boolean activity value to each of the eight phases. Researchers deriving the Physical Church-Turing Thesis within Recognition Science reference this construction to bound physical processes to finite-state computable transitions. The declaration is a direct type abbreviation deriving Fintype and DecidableEq instances from the standard structures on Fin 8 and Bool.
Claim. Let $S$ be the set of discrete ledger states. Then $S$ consists of all functions $f : [8] → {true, false}$, where $f(i)$ records whether phase $i$ is active under the eight-tick cycle.
background
Module IC-003 shows that the Physical Church-Turing Thesis follows in Recognition Science once dynamics are restricted to a discrete ledger whose updates are governed by the eight-tick operator. Each tick processes only a finite number of ledger entries, with memory bounded by the eight phases. The upstream constant A, defined as the active edge count per fundamental tick and fixed at 1, supplies the coherence scale that keeps every configuration inside this finite phase space.
proof idea
The declaration is a one-line type abbreviation that sets the discrete ledger state to the function type Fin 8 → Bool. It inherits the Fintype instance directly from the product of Fintype instances on Fin 8 and Bool, and DecidableEq follows from the decidability of boolean equality.
why it matters
This type supplies the finite carrier set required by the theorems establishing that every ledger transition admits a finite lookup table and that the state space has exactly 256 elements. It therefore completes the discrete-state premise in the IC-003 derivation that Recognition Science dynamics remain Turing-computable. The construction rests on the eight-tick octave of the forcing chain, confirming that no trans-Turing process can arise inside the ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.