LedgerComputation
plain-language theorem explainer
LedgerComputation defines a structure for ledger-based computation that includes state evolution, boolean-list encoding, and measurement with an explicit query lower bound derived from balanced-parity hiding. Researchers modeling dual computation-recognition scales in the ledger framework would reference this when examining information-theoretic barriers. The declaration is a direct structure with placeholder conservation and a measurement axiom using the enc encoder.
Claim. A structure with state space $S$, evolution map $e:S→S$, encoding $enc$ from lists of booleans to $S$, measurement map from states and subsets of size less than $n$ to booleans, the property that $e$ is the identity, and the axiom that no measurement on a proper subset recovers every encoded bit $b$ under the balanced-parity mask.
background
The module is explicitly labeled a scaffold for exploratory work on ledger implications for complexity and is not part of any verified certificate chain. It draws on BalancedParityHidden.enc, which maps a bit $b$ and mask $R$ to the hidden vector that equals $R$ when $b$ is false and its complement when $b$ is true. It also references LedgerForcing.balanced, which asserts that every ledger event list satisfies the double-entry condition, and the Measurement structure from Data.Import. The local setting examines how the ledger's posting adjacency and parity pattern create an observation cost that the Turing model omits.
proof idea
The declaration is the structure definition itself. It directly assembles the six fields, with the measurement_bound field invoking BalancedParityHidden.enc inside the negated universal quantifier over bits and masks.
why it matters
The structure is extended by CompleteModel and supplies the model parameter for both the hypothetical main_resolution theorem and the Turing_incomplete theorem. It fills the role of supplying an explicit recognition-cost interface inside the ComputationBridge exploration of P-vs-NP hypotheses under ledger assumptions. The module doc-comment states that these results rely on hypothetical model assumptions and are not proven unconditional results; the declaration therefore touches the open question of whether ledger double-entry structure can induce a separation between computation time and recognition time.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.