balanced_list
plain-language theorem explainer
balanced_list encodes the double-entry constraint on a list of recognition events by requiring equal multiplicity for every event and its reciprocal. Ledger-based models in Recognition Science cite this predicate when deriving conservation or symmetry preservation results. The definition is a direct predicate that applies list count to the reciprocal map on events.
Claim. A list $l$ of recognition events is balanced when, for every event $e$, the multiplicity of $e$ in $l$ equals the multiplicity of its reciprocal $e^{-1}$, where the reciprocal swaps the source and target agents while inverting the ratio.
background
RecognitionEvent is the structure recording a directed recognition between two agents (source and target) together with a positive real ratio. The reciprocal operation, defined in the same module, produces the inverse event by exchanging source and target and replacing the ratio by its multiplicative inverse. The LedgerForcing module shows that J-symmetry on recognition events forces a double-entry ledger structure; balanced_list supplies the predicate that enforces the required pairing.
proof idea
This is a direct definition whose body states that list count of each event equals list count of its reciprocal. It uses the module-local reciprocal function and the standard List.count operation; no lemmas are applied beyond the definition of those primitives.
why it matters
The definition supplies the double-entry predicate that appears in the Ledger structure and is invoked by conservation_from_balance (net flow vanishes) and add_event_balanced_list (balance is preserved by adjoining reciprocal pairs). It therefore realizes the module's central claim that J-symmetry forces double-entry accounting, feeding directly into PreservesJSymmetry and the larger Recognition Science derivation of ledger balance from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.