ledger_state_space_finite
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.