RecogLedger
plain-language theorem explainer
The RecogLedger abbreviation imports the double-entry ledger type from the core Recognition module into the RRF namespace. It supplies the bookkeeping structure needed to track recognizer-recognized pairs and their balances in recognition-based derivations. Researchers constructing RRF models of recognition chains or strain would reference this alias when instantiating ledgers. The definition is a direct one-line alias with no added computation or proof obligations.
Claim. Let $RecogLedger$ denote the type of double-entry ledgers for recognition processes, defined by aliasing the Ledger type from the Recognition module.
background
The module re-exports core Recognition definitions to bridge them into the RRF framework. Key among them is the Ledger, which implements double-entry bookkeeping to record recognition events while maintaining balance. Upstream results supply supporting primitives: the Phi function defined as the integral of a history function H from 0 to t, and the net balance operator that subtracts credit from debit on a ledger constraint or state.
proof idea
The declaration is a direct abbreviation that aliases the Ledger type from the imported Recognition module.
why it matters
This alias embeds the recognition ledger into the RRF namespace, enabling consistent use of double-entry structures alongside strain nets and atomic ticks in the Recognition Composition Law and forcing chain. It fills the bookkeeping role required for ledger-based models of recognition without introducing new hypotheses. No downstream theorems are listed, so it functions as a foundational bridge rather than a derived result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.