net_flow
plain-language theorem explainer
Net flow at an agent sums the logarithm of each event ratio for every recognition event incident to that agent. Researchers proving conservation laws from J-symmetry in Recognition Science cite this definition when establishing zero net flow in balanced ledgers. The definition is realized by a direct fold over the event list that adds Real.log of the ratio on source or target match.
Claim. Let $L$ be a ledger consisting of a list of recognition events that satisfies the double-entry balance condition. For an agent $a$, the net flow at $a$ is defined by summing $log(ratio(e))$ over every event $e$ in the list for which $a$ is the source or the target.
background
The LedgerForcing module establishes that J-symmetry forces double-entry ledger structure. A Ledger is a structure that pairs a list of RecognitionEvent with a balanced_list predicate enforcing the double-entry constraint. RecognitionEvent records source, target, and ratio fields. The empty ledger is the structure with an empty transaction list and zero totals. Upstream L definitions supply basic ledgers with unit debit and credit values.
proof idea
The definition is a direct fold over the events list. It initializes the accumulator at zero and, for each event, adds the real logarithm of the ratio precisely when the agent equals the source or the target.
why it matters
This definition supplies the quantity whose vanishing is proved in conservation_from_balance, the central conservation theorem of the module. It is invoked in every concrete Euler ledger construction to obtain zero net flow at every agent, thereby bridging arithmetic Euler data to the ontology layer. The construction realizes the double-entry consequence of the Recognition Composition Law within the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.