net_flow
plain-language theorem explainer
Net flow at an agent sums the logarithms of event ratios over all recognition events incident to that agent. Conservation theorems in the Recognition framework cite this definition when establishing zero net flow from ledger balance. The definition is implemented directly as a left fold that adds Real.log of the ratio precisely when source or target matches the agent.
Claim. For a ledger $L$ whose events are a list of recognition events and an agent $a$, the net flow is defined by $net_flow(L,a) = sum_{e} log(ratio(e))$ where the sum runs over those $e$ in the events of $L$ for which source($e$)=a or target($e$)=a.
background
The LedgerForcing module shows that J-symmetry forces double-entry ledger structure. A Ledger is the structure whose fields are a list of RecognitionEvent together with the balanced_list predicate that encodes the double-entry constraint. The net_flow definition supplies the concrete real-valued quantity whose vanishing is later proved from balance.
proof idea
The definition is given by a single foldl over the events list. The accumulator starts at 0; for each event the code adds Real.log of its ratio exactly when the agent equals source or target and otherwise leaves the accumulator unchanged.
why it matters
conservation_from_balance invokes net_flow to prove that any balanced ledger has zero net flow at every agent; empty_ledger_net_flow applies the same definition to the empty case. The Euler-ledger results (finiteEulerLedger_net_flow_zero, sensorEulerLedger_net_flow_zero) then obtain zero net flow by calling conservation_from_balance on concrete constructions. The definition therefore supplies the computational content for the J-symmetry to double-entry forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.