closes: a run of members closes splits cumulatively

Each close into members' capital rounded on its own, ties to the
earlier member, so twelve monthly 50/50 closes of odd-cent income could
leave one member several cents ahead of half the year (docs/testing.md
#12, found with the members' equity fix).

- CloseTo::Members now splits cumulatively over a run (closes back to
  back with the same members and shares): each close gives a member
  allocate(run total so far) - allocate(run total before). Periods
  record their close order and a cumulative close's members and net
  (Period::close_seq, member_close) so the next close continues the run
  and replay recomputes it exactly. A close to anything else, or other
  shares, ends the run.
- Journaled "rounding": "cumulative". The per-close rule is kept as
  CloseTo::MembersPerClose for closes journaled "largest_remainder";
  older closes still replay with the last member absorbing it.
- Lean: runPart_telescopes (a member's total from a run is their
  allocation of the run's total) and closePart_total (each close hands
  out exactly its net), audited to the standard axioms.
- Tests: hand-computed three one-cent months (per close A 0.03 / B 0;
  cumulative A 0.02 / B 0.01), a run ending, a property that each member
  stays within a cent of their share (fails on the per-close rule), and
  a store contract that each rule journals and replays as itself.

Wanderland's books have no closes yet, so all of theirs use the new rule.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GWVo7x3UHw5kwCUaWxiejX

verify/lean/Audit.lean

@@ -19,6 +19,8 @@ open Wanderbooks
 #print axioms net_closings_is_net_income
 #print axioms plugLast_total
 #print axioms plugLast_keeps
+#print axioms runPart_telescopes
+#print axioms closePart_total
 #print axioms Reachable.inv
 #print axioms Reachable.books_net_zero
 #print axioms Reachable.trial_balance

verify/lean/Wanderbooks/Closing.lean

@@ -317,4 +317,54 @@ theorem plugLast_keeps (whole : Int) (ps : List Int) :
       rw [show plugLast whole (p :: q :: rest) = p :: plugLast (whole - p) (q :: rest) from rfl,
         List.dropLast_cons_of_ne_nil hne, ih, List.dropLast_cons_cons]
 
+/-! ## Cumulative member closes
+
+A run of members closes (`CloseTo::Members`, rules.md B-13) gives each
+member, at each close, their allocation of the run's total so far minus
+their allocation of the total before it. `alloc` is any allocation of an
+amount to members (member `i` gets `alloc x i`), such as
+`periods::allocate`. -/
+
+/-- What one close gives member `i`: `before` is the run's total before
+it, `net` what it closes. -/
+def closePart (alloc : Int → Nat → Int) (before net : Int) (i : Nat) : Int :=
+  alloc (before + net) i - alloc before i
+
+/-- What a run of closes with these nets, starting after `before`, gives
+member `i` in all. -/
+def runPart (alloc : Int → Nat → Int) : Int → List Int → Nat → Int
+  | _, [], _ => 0
+  | before, net :: rest, i => closePart alloc before net i + runPart alloc (before + net) rest i
+
+/-- **A run telescopes**: member `i`'s total from a run is their allocation
+of everything the run closed, less their allocation of where it started.
+From an empty start (`alloc 0 = 0`), it is exactly their allocation of
+the run's total, so its rounding is one allocation's rounding, never a
+sum of them. -/
+theorem runPart_telescopes (alloc : Int → Nat → Int) (before : Int) (nets : List Int) (i : Nat) :
+    runPart alloc before nets i = alloc (before + nets.sum) i - alloc before i := by
+  induction nets generalizing before with
+  | nil => simp [runPart]
+  | cons n rest ih =>
+    simp only [runPart, closePart, ih, List.sum_cons]
+    rw [show before + n + rest.sum = before + (n + rest.sum) by omega]
+    omega
+
+/-- A sum of differences is the difference of the sums. -/
+theorem sum_map_sub (f g : Nat → Int) (ms : List Nat) :
+    (ms.map (fun i => f i - g i)).sum = (ms.map f).sum - (ms.map g).sum := by
+  induction ms with
+  | nil => simp
+  | cons m ms ih => simp only [List.map_cons, List.sum_cons, ih]; omega
+
+/-- **Each close hands out exactly its net** when every allocation sums
+to its amount (`periods::allocate` does: `kernel::apportion`). -/
+theorem closePart_total (alloc : Int → Nat → Int) (members : List Nat)
+    (sums : ∀ x, (members.map (alloc x)).sum = x) (before net : Int) :
+    (members.map (closePart alloc before net)).sum = net := by
+  have h := sum_map_sub (alloc (before + net)) (alloc before) members
+  unfold closePart
+  rw [h, sums, sums]
+  omega
+
 end Wanderbooks