LedgerVecState
plain-language theorem explainer
LedgerVecState supplies the type for d-dimensional integer vectors as ledger states in the parity-adjacency bridge. Researchers on Workstream B2 cite it as the domain on which atomic steps and parity patterns are defined. The abbreviation is a direct type alias to Fin d → ℤ with no added structure.
Claim. A ledger-vector state of dimension $d$ is an element of the function space $Fin d → ℤ$.
background
The LedgerParityAdjacency module models ledger states as integer vectors on which a single-coordinate ±1 update occurs. The atomic step relation is supplied by coordAtomicStep and the parity observation by parityPattern. This construction forms the mathematical core of Workstream B2: a single atomic update changes the induced parity pattern in exactly one bit.
proof idea
The declaration is a direct type abbreviation to the function space Fin d → ℤ.
why it matters
LedgerVecState supplies the state space for the downstream declarations ledgerVecStep, ledgerVecParity and ledgerVecStep_oneBitDiff. It fills the ledger-model slot in the B2 bridge-lemma scaffold that connects integer-vector updates to one-bit parity changes. In the Recognition framework it supports the passage from ledger legality to adjacency properties under cost minimization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.