phi
plain-language theorem explainer
The definition re-exports the net balance function phi from the core Recognition module into the RRF namespace. Researchers building recognition-based accounting on chains would cite it when mapping ledger entries to integer balances on the universe U. The body is a direct one-line alias to Recognition.phi applied to the supplied ledger.
Claim. Let $M$ be a recognition structure with universe $U$ and relation $R$. For a ledger $L$ on $M$, the map $L.U → ℤ$ given by phi assigns to each element its net recognition balance.
background
The module re-exports Recognition definitions under the RRF namespace as a bridge to the unified framework. RecognitionStructure is the minimal type carrying a universe U and binary relation R. Ledger supplies debit and credit maps for double-entry recognition accounting, while Chain records finite sequences of steps satisfying the consecutive recognition condition ok.
proof idea
One-line wrapper that applies Recognition.phi to the input ledger L.
why it matters
The definition supplies the net balance map required for ledger operations inside RRF. It sits directly above the RecognitionStructure and Chain axioms imported from the base module, enabling balance tracking in recognition sequences without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.