phiVec
plain-language theorem explainer
phiVec extracts the integer recognition-cost vector from a ledger state L with d accounts by direct delegation to Recognition.phi. Researchers building ledger models of recognition dynamics cite it to track coordinate-wise changes under single-unit postings. The definition is a one-line alias to Recognition.phi applied to L.
Claim. For natural number $d$ and ledger state $L$ with $d$ accounts, the map $imapsto phi(L)_i$ from Fin $d$ to $Z$ is the recognition-cost vector of $L$.
background
LedgerState $d$ is the type Recognition.Ledger (AccountRS $d$), where each state records debit and credit counters per account. The module develops an explicit posting model: a single tick adds one unit to exactly one account on either the debit or credit side. phiVec supplies the net integer vector of recognition costs used to induce parity patterns from these states.
proof idea
The abbrev is a one-line wrapper that applies Recognition.phi to the input ledger state L.
why it matters
phiVec supplies the coordinate vector required to define parity and to prove one-bit adjacency under posting. It is invoked directly by parity, phiVec_post_debit, phiVec_post_credit, phiVec_coordAtomicStep_of_post, and parity_oneBitDiff_of_post. The construction supplies the ledger-to-parity bridge stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.