add_event_balanced_list
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove balance for an arbitrary initial list without the supplied hypothesis.
- Does not address infinite collections or structures other than finite lists.
- Does not compute J-costs or numerical values attached to the events.
- Does not extend the balance property to removal or merging operations.
- Does not establish uniqueness of the reciprocal pairing beyond injectivity.
Lean usage
noncomputable def add_event (L : Ledger) (e : RecognitionEvent) : Ledger := { events := e :: reciprocal e :: L.events, double_entry := add_event_balanced_list L.events L.double_entry e }formal statement (Lean)
282theorem add_event_balanced_list (l : List RecognitionEvent) (h : balanced_list l) (e : RecognitionEvent) :
283 balanced_list (e :: reciprocal e :: l) := by
proof body
Tactic-mode proof.
284 intro x
285 unfold balanced_list at h
286 -- The new list is e :: reciprocal e :: l
287 -- count x in this list = (if x = e then 1 else 0) + (if x = reciprocal e then 1 else 0) + count x l
288 simp only [List.count_cons]
289 -- Using h: count x l = count (reciprocal x) l
290 rw [h x]
291 -- Now need: (e == x) + (reciprocal e == x) = (e == reciprocal x) + (reciprocal e == reciprocal x)
292 -- where == is decidable equality (beq)
293 -- This follows from the symmetry: x ↔ reciprocal x swaps e and reciprocal e
294 -- Specifically: (e == x) = (reciprocal e == reciprocal x) and (reciprocal e == x) = (e == reciprocal x)
295 -- Using: x = e ↔ reciprocal x = reciprocal e, and x = reciprocal e ↔ reciprocal x = e
296 have key1 : (e == x) = (reciprocal e == reciprocal x) := by
297 -- e == x ↔ e = x (since DecidableEq RecognitionEvent)
298 -- e = x ↔ reciprocal e = reciprocal x (by reciprocal_inj symmetry)
299 cases h1 : e == x
300 · -- e ≠ x
301 have hne : e ≠ x := by simpa using h1
302 have hne' : reciprocal e ≠ reciprocal x := fun h => hne ((reciprocal_inj e x).mp h)
303 simp [hne', beq_eq_false_iff_ne]
304 · -- e = x
305 have heq : e = x := by simpa using h1
306 have heq' : reciprocal e = reciprocal x := by rw [heq]
307 simp [heq']
308 have key2 : (reciprocal e == x) = (e == reciprocal x) := by
309 cases h2 : reciprocal e == x
310 · -- reciprocal e ≠ x
311 have hne : reciprocal e ≠ x := by simpa using h2
312 have hne' : e ≠ reciprocal x := fun h => hne (by rw [← reciprocal_reciprocal x, h, reciprocal_reciprocal])
313 simp [hne', beq_eq_false_iff_ne]
314 · -- reciprocal e = x
315 have heq : reciprocal e = x := by simpa using h2
316 have heq' : e = reciprocal x := by rw [← heq, reciprocal_reciprocal]
317 simp [heq']
318 -- Now use these to rewrite the goal
319 -- Goal becomes: a + (b + c) = b + (a + c) which is add_right_comm
320 simp only [key1, key2]
321 ring
322
323/-- Add an event and its reciprocal to a ledger. -/