phiVec
plain-language theorem explainer
phiVec extracts the integer vector of net recognition values from a ledger state L over d accounts. Ledger modelers building parity patterns from debit-credit postings cite this when reducing single-account updates to coordinate changes. The declaration is a one-line abbreviation delegating directly to Recognition.phi.
Claim. For a ledger state $L$ with $d$ accounts, let $phiVec(L)$ be the map $Fin d to Z$ given by applying the recognition function $phi$ to $L$.
background
LedgerState d is defined locally as Recognition.Ledger (AccountRS d). The module models a posting ledger in which each tick adds one unit of debit or credit to exactly one account, so that phi equals debit minus credit per account. Upstream LedgerState structures from VariationalDynamics, InformationIsLedger, Thermodynamics, GaugeInvariance and Recognition supply conserved quantities or event lists, but the present abbreviation specializes phi to the recognition ledger for adjacency calculations.
proof idea
one-line wrapper that applies Recognition.phi to the input ledger state L.
why it matters
phiVec supplies the vector used to define parity as parityPattern of phiVec and to prove parity_oneBitDiff_of_post together with the coordinate step lemmas. It supplies the explicit link between the posting model and the one-bit adjacency results of LedgerParityAdjacency, closing the gap noted in the module documentation between ledger language and Gray-code parity. In the Recognition framework this supports discrete updates compatible with the eight-tick octave and D=3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.