add_event_balanced_list
plain-language theorem explainer
If a list of recognition events is balanced, meaning every event has the same multiplicity as its reciprocal, then prepending any event e together with its reciprocal preserves the balance property. Ledger constructions in Recognition Science cite this to obtain double-entry structure directly from J-symmetry. The tactic proof unfolds the count predicate, rewrites via the hypothesis, and equates the two new increments through case analysis on decidable equality together with injectivity and involution of reciprocal.
Claim. Let $l$ be a list of recognition events such that for every event $x$, the multiplicity of $x$ in $l$ equals the multiplicity of its reciprocal. Then for any recognition event $e$, the extended list $e ::$ reciprocal$(e) :: l$ satisfies the same multiplicity equality for every event.
background
The module Ledger Forcing shows that J-symmetry forces double-entry ledger structure. A recognition event is a triple of natural-number agents together with a positive real ratio; its reciprocal swaps the agents and inverts the ratio, implementing the automorphism supplied by CostAlgebra.reciprocal. balanced_list is the predicate that every event count equals the count of its reciprocal, which directly encodes the double-entry constraint on a finite ledger.
proof idea
The tactic proof introduces the test event x, unfolds balanced_list at the hypothesis, and simplifies the cons-counts with List.count_cons. It rewrites the tail count via the hypothesis, then proves two auxiliary equalities by cases on beq: the first uses reciprocal_inj to swap e with reciprocal e, the second uses reciprocal_reciprocal to swap the test point. The resulting arithmetic identity is closed by ring.
why it matters
The result supplies the double_entry field for the add_event definition in the same module, which constructs a Ledger by prepending a paired event. It therefore realizes the module claim that J-symmetry forces double-entry bookkeeping. In the broader forcing chain it supplies the concrete ledger object required after T5 J-uniqueness and before any cost or mass calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Unique reciprocal cost on ratios forces balanced discrete ledgers
"Under deterministic update semantics and minimality (no intra-tick ordering metadata), we derive atomic ticks (at most one event per tick). Explicit structural assumptions (conservation, no sources/sinks, pairwise locality, quantization in δℤ) force balanced double-entry postings"