phiVec
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive the posting rule from more primitive axioms.
- Does not handle states with negative balances.
- Does not extend to concurrent or multi-tick updates.
- Does not compute numerical values for physical constants.
formal statement (Lean)
60abbrev phiVec {d : Nat} (L : LedgerState d) : Fin d → ℤ :=
proof body
Definition body.
61 Recognition.phi L
62