ledger_state_space_finite
The discrete ledger state space consists of exactly 256 elements because each of eight phases maps independently to an active or inactive boolean. Researchers deriving the physical Church-Turing thesis in Recognition Science cite this bound to establish that RS dynamics remain within finite-state computation. The proof is a one-line term simplification that unfolds the definition of DiscreteLedgerState as maps from Fin 8 to Bool and applies standard cardinality rules for finite products and boolean sets.
claimThe set of all functions from a set of eight elements to the two-element boolean set has cardinality $2^8$.
background
DiscreteLedgerState is defined as the type Fin 8 → Bool, where each of the eight indices corresponds to one tick in the octave structure and the boolean records whether that phase is active. This discretization arises from the eight-tick operator that governs ledger updates in the Recognition Science framework. The module IC-003 derives the physical Church-Turing thesis from this finite discrete ledger, noting that each tick updates a bounded number of entries and that J-cost minimization maps finite states to finite states. Upstream structures from spectral emergence and phi forcing supply the eight-phase count that fixes the domain size.
proof idea
The proof is a term-mode simplification. It unfolds DiscreteLedgerState to Fin 8 → Bool, then invokes Fintype.card_pi to treat the function space as an eight-fold product, Fintype.card_fin to obtain cardinality 8 for the domain, and Fintype.card_bool to obtain cardinality 2 for each codomain factor, yielding the product 2^8.
why it matters in Recognition Science
This theorem supplies the finite-state cardinality required by the downstream ic003_certificate that certifies the full Church-Turing physics structure. It completes the discrete-state-space step in the IC-003 chain and directly instantiates the eight-tick octave (T7) whose period 2^3 produces the 256-element space. The result closes one scaffolding link between the ledger factorization and the claim that RS dynamics admit Turing-machine simulation, while leaving open the precise rate at which continuous limits emerge from the finite discretization.
scope and limits
- Does not claim that ledger states exhaust every physical configuration.
- Does not bound approximation error when continuous fields are recovered from the discrete ledger.
- Does not derive explicit transition functions between states.
- Does not resolve undecidability questions for the halting problem on RS dynamics.
formal statement (Lean)
86theorem ledger_state_space_finite :
87 Fintype.card DiscreteLedgerState = 2 ^ 8 := by
proof body
Term-mode proof.
88 simp [DiscreteLedgerState, Fintype.card_pi, Fintype.card_fin, Fintype.card_bool]
89
90/-! ## III. RS Dynamics are Church-Turing Computable -/
91
92/-- Carrier of computation_limits_from_ledger through the chain. -/