LedgerComputation
LedgerComputation assembles a structure for modeling computation via ledger states that explicitly tracks evolution, input encoding through balanced parity, and measurement operations with query bounds. Researchers examining complexity separations in the Recognition Science ledger framework would cite this when testing whether double-entry rules create an information barrier between computation and observation. The declaration is a plain structure definition that directly incorporates fields from upstream balanced and parity constructions with
claimA structure consisting of a state space $S$, an evolution map $e:S→S$, an encoding map from lists of booleans into $S$, and a measurement map from states and finite subsets of Fin $n$ to booleans, subject to the conditions that evolution preserves closed-chain flux and that measurement of any balanced-parity encoding requires more than a single query for every proper subset of coordinates.
background
This structure appears in the scaffold module ComputationBridge, which the module documentation describes as an exploratory framework for ledger-style dual complexity rather than part of the verified certificate chain. Upstream definitions supply the concrete pieces: BalancedParityHidden.enc produces a hidden mask by flipping the mask R precisely when the bit b is true, while LedgerForcing.balanced asserts that a ledger remains balanced when its event list satisfies the balanced_list predicate. LedgerPostingAdjacency.parity further supplies the parity pattern derived from the phi-vector of a ledger state. The local setting treats states as a placeholder Type (commonly Unit) and measurement as an explicit cost that the Turing model omits.
proof idea
The declaration is a structure definition with an empty proof body. Its fields are assembled by direct reference to the supplied upstream constructions: encode is instantiated from BalancedParityHidden.enc, flux_conserved invokes the balanced predicate from LedgerForcing, and measurement_bound encodes the query lower bound that follows from the information-hiding property of the parity mask.
why it matters in Recognition Science
LedgerComputation supplies the base model extended by CompleteModel and invoked inside the main_resolution and Turing_incomplete theorems that explore a hypothetical P versus NP separation. It occupies the position of defining the computational substrate in the scaffold exploration of how ledger double-entry forces recognition cost to diverge from computation cost. The module documentation explicitly flags that these results rest on hypothetical assumptions and are not to be cited as proven mathematics; the structure therefore touches the open question of whether the Recognition Science ledger framework can produce an unconditional complexity separation while remaining outside the verified T0-T8 forcing chain.
scope and limits
- Does not claim an unconditional resolution of P versus NP.
- Does not belong to the verified certificate chain in Verification or URCGenerators.
- Does not supply a concrete state type beyond the placeholder Type.
- Does not prove the measurement lower bound for arbitrary encodings.
formal statement (Lean)
76structure LedgerComputation where
77 /-- State space (ledger configurations) -/
78 states : Type
79 /-- Evolution rule (double-entry updates) -/
80 evolve : states → states
81 /-- Input encoding into ledger -/
82 encode : List Bool → states
83 /-- Output protocol (measurement operations) -/
84 measure : states → Finset (Fin n) → Bool
85 /-- Evolution preserves closed-chain flux = 0 -/
86 flux_conserved : ∀ s, evolve s = s -- placeholder for actual conservation
87 /-- Measurement requires Ω(n) queries for balanced-parity encoding -/
88 measurement_bound : ∀ n M (hM : M.card < n),
89 ¬(∀ b R, measure (encode (BalancedParityHidden.enc b R).toList) M = b)
90
91/-- SAT instance in ledger representation -/