feat(bookspec): the five laws as Lean theorems (P13 step 4)

The first edition's five laws (debits equal credits; the accounting
equation; the trial balance balances; net income articulates to equity;
the cash-flow sections sum to the change in cash) are theorems in
bookspec/lean, ported from verify/lean (Basic, Entry, Statements, Closing,
Ledger under namespace Bookspec) and restated by name in Laws.lean, each a
statement about every reachable state of the books. Audit.lean prints
their axioms; the checker's lean.rs test fails on a sorry, a law not
audited, or any axiom beyond propext, Quot.sound and Classical.choice.
Money is Int, the exact count of the smallest unit: every law is a law of
addition, so the model is faithful to exact decimals.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HS8WZziDnyxunC23MUxrLp

bookspec/lean/Bookspec/Basic.lean

@@ -0,0 +1,165 @@
+/-!
+# Lines, sides, and nets
+
+The vocabulary of double entry. Money is `Int`: an exact count of the
+smallest unit the books use. Any finite set of exact decimals (what the
+engine stores) scales to integers without loss, and every law here is a
+law of addition, so `Int` is a faithful model.
+
+Mirrors `crates/ledger-core/src/kernel.rs` (`flip`, `signed`, `net`,
+`totals`) and `account.rs` (`Side`, `AccountType`, `normal_side`).
+-/
+
+namespace Bookspec
+
+/-- Debit or credit. -/
+inductive Side where
+  | debit
+  | credit
+  deriving DecidableEq, Repr
+
+/-- The other side (`kernel::flip`). -/
+def Side.flip : Side → Side
+  | .debit => .credit
+  | .credit => .debit
+
+@[simp] theorem Side.flip_flip (s : Side) : s.flip.flip = s := by
+  cases s <;> rfl
+
+theorem Side.flip_ne (s : Side) : s.flip ≠ s := by
+  cases s <;> simp [Side.flip]
+
+/-- The five account types. -/
+inductive AccountType where
+  | asset
+  | liability
+  | equity
+  | revenue
+  | expense
+  deriving DecidableEq, Repr
+
+/-- The side that increases an account (`AccountType::normal_side`). -/
+def AccountType.normal : AccountType → Side
+  | .asset | .expense => .debit
+  | .liability | .equity | .revenue => .credit
+
+/-- A line's signed amount: `+a` for a debit, `-a` for a credit
+(`kernel::signed`). -/
+def signed : Side → Int → Int
+  | .debit, a => a
+  | .credit, a => -a
+
+@[simp] theorem signed_debit (a : Int) : signed .debit a = a := rfl
+@[simp] theorem signed_credit (a : Int) : signed .credit a = -a := rfl
+
+theorem signed_flip (s : Side) (a : Int) : signed s.flip a = -signed s a := by
+  cases s <;> simp [Side.flip]
+
+/-- One journal line. -/
+structure Line where
+  account : Nat
+  side : Side
+  amount : Int
+  deriving DecidableEq, Repr
+
+/-- A line's signed amount. -/
+def Line.signed (l : Line) : Int := Bookspec.signed l.side l.amount
+
+/-- The net of some lines: debits minus credits (`kernel::net`). -/
+def net : List Line → Int
+  | [] => 0
+  | l :: ls => l.signed + net ls
+
+/-- Total debits. -/
+def debits : List Line → Int
+  | [] => 0
+  | l :: ls => (if l.side = .debit then l.amount else 0) + debits ls
+
+/-- Total credits. -/
+def credits : List Line → Int
+  | [] => 0
+  | l :: ls => (if l.side = .credit then l.amount else 0) + credits ls
+
+@[simp] theorem net_nil : net [] = 0 := rfl
+@[simp] theorem net_cons (l : Line) (ls : List Line) : net (l :: ls) = l.signed + net ls := rfl
+
+theorem net_append (xs ys : List Line) : net (xs ++ ys) = net xs + net ys := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih => simp only [List.cons_append, net_cons, ih]; omega
+
+/-- The net is debits minus credits. -/
+theorem net_eq_debits_sub_credits (ls : List Line) : net ls = debits ls - credits ls := by
+  induction ls with
+  | nil => rfl
+  | cons l ls ih =>
+    obtain ⟨a, s, m⟩ := l
+    cases s <;> simp [net, debits, credits, Line.signed, signed, ih] <;> omega
+
+/-- A sum over a list of account codes. -/
+def sumOver (f : Nat → Int) : List Nat → Int
+  | [] => 0
+  | a :: as => f a + sumOver f as
+
+@[simp] theorem sumOver_nil (f : Nat → Int) : sumOver f [] = 0 := rfl
+@[simp] theorem sumOver_cons (f : Nat → Int) (a : Nat) (as : List Nat) :
+    sumOver f (a :: as) = f a + sumOver f as := rfl
+
+theorem sumOver_add (f g : Nat → Int) (as : List Nat) :
+    sumOver (fun a => f a + g a) as = sumOver f as + sumOver g as := by
+  induction as with
+  | nil => rfl
+  | cons a as ih => simp only [sumOver_cons, ih]; omega
+
+theorem sumOver_neg (f : Nat → Int) (as : List Nat) :
+    sumOver (fun a => -f a) as = -sumOver f as := by
+  induction as with
+  | nil => rfl
+  | cons a as ih => simp only [sumOver_cons, ih]; omega
+
+theorem sumOver_zero (as : List Nat) : sumOver (fun _ => 0) as = 0 := by
+  induction as with
+  | nil => rfl
+  | cons a as ih => simp [ih]
+
+theorem sumOver_congr (f g : Nat → Int) (as : List Nat) (h : ∀ a ∈ as, f a = g a) :
+    sumOver f as = sumOver g as := by
+  induction as with
+  | nil => rfl
+  | cons a as ih =>
+    simp only [sumOver_cons]
+    rw [h a (by simp), ih (fun b hb => h b (by simp [hb]))]
+
+/-- No code repeats (a chart's codes are unique). -/
+def Distinct : List Nat → Prop
+  | [] => True
+  | a :: as => a ∉ as ∧ Distinct as
+
+/-- Summing an indicator over codes that do not include `k` gives zero. -/
+theorem sumOver_indicator_absent (k : Nat) (x : Int) (as : List Nat) (h : k ∉ as) :
+    sumOver (fun a => if k = a then x else 0) as = 0 := by
+  induction as with
+  | nil => rfl
+  | cons a as ih =>
+    have hka : k ≠ a := fun e => h (e ▸ List.mem_cons_self ..)
+    have hk : k ∉ as := fun hm => h (List.mem_cons_of_mem _ hm)
+    simp [hka, ih hk]
+
+/-- Summing an indicator over distinct codes that include `k` picks out
+exactly one term. -/
+theorem sumOver_indicator (k : Nat) (x : Int) (as : List Nat) (hd : Distinct as)
+    (hk : k ∈ as) : sumOver (fun a => if k = a then x else 0) as = x := by
+  induction as with
+  | nil => simp at hk
+  | cons a as ih =>
+    obtain ⟨ha, hd⟩ := hd
+    by_cases e : k = a
+    · subst e
+      simp [sumOver_indicator_absent k x as ha]
+    · have : k ∈ as := by
+        cases hk with
+        | head => exact absurd rfl e
+        | tail _ h => exact h
+      simp [e, ih hd this]
+
+end Bookspec

bookspec/lean/Bookspec/Closing.lean

@@ -0,0 +1,451 @@
+import Bookspec.Statements
+
+/-!
+# Closing a period, and splitting the net
+
+Mirrors `kernel::closing_line`, `kernel::credit_line`, `kernel::plug_last`,
+`periods::allocate`, and `Ledger::close_period_to` (income closing, net to
+one equity account or split among members).
+-/
+
+namespace Bookspec
+
+/-- The line that zeroes an account with movement `m`: the opposite side,
+same amount; nothing for zero (`kernel::closing_line`). It is also the
+line that credits `m` to an account (`kernel::credit_line`). -/
+def closingLine (a : Nat) (m : Int) : List Line :=
+  if 0 < m then [⟨a, .credit, m⟩] else if m < 0 then [⟨a, .debit, -m⟩] else []
+
+theorem net_closingLine (a : Nat) (m : Int) : net (closingLine a m) = -m := by
+  unfold closingLine
+  split
+  · simp [Line.signed]
+  · split <;> simp [Line.signed] <;> omega
+
+theorem movement_closingLine (b a : Nat) (m : Int) :
+    movement b (closingLine a m) = if b = a then -m else 0 := by
+  by_cases e : b = a
+  · subst e
+    rcases (by omega : 0 < m ∨ m < 0 ∨ m = 0) with h | h | h
+    · simp [closingLine, h, Line.signed]
+    · have : ¬ 0 < m := by omega
+      simp [closingLine, h, this, Line.signed]
+    · simp [closingLine, h]
+  · have e' : ¬ a = b := fun x => e x.symm
+    unfold closingLine
+    split <;> (try split) <;> simp [e']
+
+theorem closingLine_pos (a : Nat) (m : Int) : ∀ l ∈ closingLine a m, 0 < l.amount := by
+  unfold closingLine
+  split
+  · simp; omega
+  · split
+    · simp; omega
+    · simp
+
+theorem closingLine_account (a : Nat) (m : Int) : ∀ l ∈ closingLine a m, l.account = a := by
+  unfold closingLine
+  split
+  · simp
+  · split <;> simp
+
+theorem closingLine_eq_nil (a : Nat) (m : Int) : closingLine a m = [] ↔ m = 0 := by
+  unfold closingLine
+  split
+  · simp; omega
+  · split
+    · simp; omega
+    · simp; omega
+
+/-- The closing lines for some accounts: one per account with a nonzero
+movement. -/
+def closings (as : List Nat) (ls : List Line) : List Line :=
+  match as with
+  | [] => []
+  | a :: as => closingLine a (movement a ls) ++ closings as ls
+
+theorem net_closings (as : List Nat) (ls : List Line) :
+    net (closings as ls) = -sumOver (fun a => movement a ls) as := by
+  induction as with
+  | nil => rfl
+  | cons a as ih => simp only [closings, net_append, net_closingLine, ih, sumOver_cons]; omega
+
+theorem movement_closings (b : Nat) (as : List Nat) (ls : List Line) (hd : Distinct as) :
+    movement b (closings as ls) = if b ∈ as then -movement b ls else 0 := by
+  induction as with
+  | nil => simp [closings]
+  | cons a as ih =>
+    obtain ⟨ha, hd⟩ := hd
+    simp only [closings, movement_append, movement_closingLine, ih hd]
+    by_cases e : b = a
+    · subst e; simp [ha]
+    · simp [e]
+
+theorem closings_pos (as : List Nat) (ls : List Line) : ∀ l ∈ closings as ls, 0 < l.amount := by
+  induction as with
+  | nil => simp [closings]
+  | cons a as ih =>
+    intro l hl
+    simp only [closings, List.mem_append] at hl
+    cases hl with
+    | inl h => exact closingLine_pos _ _ l h
+    | inr h => exact ih l h
+
+theorem closings_account (as : List Nat) (ls : List Line) : ∀ l ∈ closings as ls, l.account ∈ as := by
+  induction as with
+  | nil => simp [closings]
+  | cons a as ih =>
+    intro l hl
+    simp only [closings, List.mem_append] at hl
+    cases hl with
+    | inl h => rw [closingLine_account _ _ l h]; simp
+    | inr h => exact List.mem_cons_of_mem _ (ih l h)
+
+/-- Nothing to close means every closed account was already at zero. -/
+theorem closings_eq_nil (as : List Nat) (ls : List Line) (h : closings as ls = []) :
+    ∀ a ∈ as, movement a ls = 0 := by
+  induction as with
+  | nil => simp
+  | cons a as ih =>
+    simp only [closings, List.append_eq_nil_iff] at h
+    intro b hb
+    cases hb with
+    | head => exact (closingLine_eq_nil _ _).1 h.1
+    | tail _ hb => exact ih h.2 b hb
+
+/-! ## The net to equity -/
+
+/-- The sum of some amounts. -/
+def total : List Int → Int
+  | [] => 0
+  | x :: xs => x + total xs
+
+/-- Lines crediting each target its part (`kernel::credit_line` per
+member). -/
+def equityLines : List (Nat × Int) → List Line
+  | [] => []
+  | (t, c) :: ts => closingLine t c ++ equityLines ts
+
+theorem net_equityLines (ts : List (Nat × Int)) :
+    net (equityLines ts) = -total (ts.map Prod.snd) := by
+  induction ts with
+  | nil => rfl
+  | cons x ts ih =>
+    obtain ⟨t, c⟩ := x
+    simp only [equityLines, net_append, net_closingLine, ih, List.map_cons, total]; omega
+
+theorem movement_equityLines_absent (b : Nat) (ts : List (Nat × Int))
+    (h : ∀ x ∈ ts, x.1 ≠ b) : movement b (equityLines ts) = 0 := by
+  induction ts with
+  | nil => rfl
+  | cons x ts ih =>
+    obtain ⟨t, c⟩ := x
+    have ht : b ≠ t := fun e => h (t, c) (by simp) e.symm
+    simp only [equityLines, movement_append, movement_closingLine, ht, ite_false,
+      ih (fun y hy => h y (List.mem_cons_of_mem _ hy))]
+    rfl
+
+theorem equityLines_pos (ts : List (Nat × Int)) : ∀ l ∈ equityLines ts, 0 < l.amount := by
+  induction ts with
+  | nil => simp [equityLines]
+  | cons x ts ih =>
+    obtain ⟨t, c⟩ := x
+    intro l hl
+    simp only [equityLines, List.mem_append] at hl
+    cases hl with
+    | inl h => exact closingLine_pos _ _ l h
+    | inr h => exact ih l h
+
+theorem equityLines_account (ts : List (Nat × Int)) :
+    ∀ l ∈ equityLines ts, ∃ x ∈ ts, l.account = x.1 := by
+  induction ts with
+  | nil => simp [equityLines]
+  | cons x ts ih =>
+    obtain ⟨t, c⟩ := x
+    intro l hl
+    simp only [equityLines, List.mem_append] at hl
+    cases hl with
+    | inl h => exact ⟨(t, c), by simp, closingLine_account _ _ l h⟩
+    | inr h =>
+      obtain ⟨y, hy, e⟩ := ih l h
+      exact ⟨y, List.mem_cons_of_mem _ hy, e⟩
+
+theorem equityLines_eq_nil (ts : List (Nat × Int)) (h : equityLines ts = []) :
+    total (ts.map Prod.snd) = 0 := by
+  induction ts with
+  | nil => rfl
+  | cons x ts ih =>
+    obtain ⟨t, c⟩ := x
+    simp only [equityLines, List.append_eq_nil_iff] at h
+    simp only [List.map_cons, total, (closingLine_eq_nil _ _).1 h.1, ih h.2]; rfl
+
+/-- The closing entry: zero the closed accounts, credit the net to the
+targets. -/
+def closingEntry (as : List Nat) (ts : List (Nat × Int)) (ls : List Line) : List Line :=
+  closings as ls ++ equityLines ts
+
+/-- **A closing entry balances** when the targets' parts sum to the net
+of the closing lines (the net income), however that net was split. -/
+theorem closingEntry_net (as : List Nat) (ts : List (Nat × Int)) (ls : List Line)
+    (hsum : total (ts.map Prod.snd) = net (closings as ls)) :
+    net (closingEntry as ts ls) = 0 := by
+  rw [closingEntry, net_append, net_equityLines, hsum]; omega
+
+/-- **A closing entry zeroes every account it closes.** -/
+theorem closingEntry_zeroes (as : List Nat) (ts : List (Nat × Int)) (ls : List Line)
+    (hd : Distinct as) (b : Nat) (hb : b ∈ as) (ht : ∀ x ∈ ts, x.1 ≠ b) :
+    movement b (ls ++ closingEntry as ts ls) = 0 := by
+  rw [movement_append, closingEntry, movement_append, movement_closings b as ls hd,
+    movement_equityLines_absent b ts ht]
+  simp only [hb, ite_true]; omega
+
+/-- **A non-empty closing entry is acceptable**: two or more lines, every
+amount positive, debits equal to credits. -/
+theorem closingEntry_accepted (as : List Nat) (ts : List (Nat × Int)) (ls : List Line)
+    (hsum : total (ts.map Prod.snd) = net (closings as ls)) (hne : closings as ls ≠ []) :
+    Accepted (closingEntry as ts ls) := by
+  refine ⟨?_, ?_, ?_⟩
+  · rw [closingEntry, List.length_append]
+    match hc : closings as ls with
+    | [] => exact absurd hc hne
+    | [l] =>
+      have hl : 0 < l.amount := closings_pos as ls l (by rw [hc]; simp)
+      have hnet : net (closings as ls) ≠ 0 := by
+        rw [hc]; obtain ⟨a, s, m⟩ := l
+        cases s <;> simp [Line.signed] at hl ⊢ <;> omega
+      have : equityLines ts ≠ [] := fun h => hnet (hsum ▸ equityLines_eq_nil ts h)
+      have : 1 ≤ (equityLines ts).length := by
+        cases h : equityLines ts with
+        | nil => exact absurd h this
+        | cons _ _ => simp
+      simp; omega
+    | _ :: _ :: _ => simp; omega
+  · intro l hl
+    simp only [closingEntry, List.mem_append] at hl
+    cases hl with
+    | inl h => exact closings_pos as ls l h
+    | inr h => exact equityLines_pos ts l h
+  · have := closingEntry_net as ts ls hsum
+    rw [net_eq_debits_sub_credits] at this; omega
+
+/-! ## Net income -/
+
+/-- The chart's revenue and expense codes: what a close zeroes. -/
+def nominalCodes : Chart → List Nat
+  | [] => []
+  | (a, t) :: c => if t = .revenue ∨ t = .expense then a :: nominalCodes c else nominalCodes c
+
+theorem nominalCodes_sub (c : Chart) : ∀ a ∈ nominalCodes c, a ∈ codes c := by
+  induction c with
+  | nil => simp [nominalCodes]
+  | cons x c ih =>
+    obtain ⟨a, t⟩ := x
+    intro b hb
+    simp only [nominalCodes] at hb
+    split at hb
+    · cases hb with
+      | head => simp
+      | tail _ h => exact List.mem_cons_of_mem _ (ih b h)
+    · exact List.mem_cons_of_mem _ (ih b hb)
+
+theorem nominalCodes_distinct (c : Chart) (hd : Distinct (codes c)) : Distinct (nominalCodes c) := by
+  induction c with
+  | nil => trivial
+  | cons x c ih =>
+    obtain ⟨a, t⟩ := x
+    obtain ⟨ha, hd⟩ := hd
+    simp only [nominalCodes]
+    split
+    · exact ⟨fun h => ha (nominalCodes_sub c a h), ih hd⟩
+    · exact ih hd
+
+/-- **The net a close credits to equity is the period's net income**:
+revenue balances minus expense balances. -/
+theorem net_closings_is_net_income (c : Chart) (ls : List Line) :
+    net (closings (nominalCodes c) ls) = typeTotal .revenue ls c - typeTotal .expense ls c := by
+  rw [net_closings]
+  induction c with
+  | nil => rfl
+  | cons x c ih =>
+    obtain ⟨a, t⟩ := x
+    cases t <;> simp [nominalCodes, typeTotal, balance, AccountType.normal, signed] at ih ⊢ <;> omega
+
+/-! ## Splitting among members -/
+
+/-- Make rounded parts sum to the whole: the last becomes the whole minus
+the others (`kernel::plug_last`). -/
+def plugLast (whole : Int) : List Int → List Int
+  | [] => []
+  | [_] => [whole]
+  | p :: q :: rest => p :: plugLast (whole - p) (q :: rest)
+
+/-- **An allocation's parts sum to the whole, exactly**, however the
+other parts were rounded. -/
+theorem plugLast_total (whole : Int) (ps : List Int) (h : ps ≠ []) :
+    total (plugLast whole ps) = whole := by
+  induction ps generalizing whole with
+  | nil => exact absurd rfl h
+  | cons p rest ih =>
+    match rest, ih with
+    | [], _ => show total [whole] = whole; simp [total]
+    | q :: rest, ih =>
+      simp only [plugLast, total]
+      have := ih (whole - p) (by simp)
+      omega
+
+theorem plugLast_length (whole : Int) (ps : List Int) : (plugLast whole ps).length = ps.length := by
+  induction ps generalizing whole with
+  | nil => rfl
+  | cons p rest ih =>
+    match rest, ih with
+    | [], _ => rfl
+    | q :: rest, ih => simp only [plugLast, List.length_cons]; rw [ih]; rfl
+
+/-- Only the last part changes. -/
+theorem plugLast_keeps (whole : Int) (ps : List Int) :
+    (plugLast whole ps).dropLast = ps.dropLast := by
+  induction ps generalizing whole with
+  | nil => rfl
+  | cons p rest ih =>
+    match rest, ih with
+    | [], _ => rfl
+    | q :: rest, ih =>
+      have hne : plugLast (whole - p) (q :: rest) ≠ [] := by
+        intro h
+        have := plugLast_length (whole - p) (q :: rest)
+        rw [h] at this; simp at this
+      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 under the run rule of 2026-10-13 to P3
+(`CloseTo::MembersRun`, journaled `"cumulative"`; 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
+
+/-! ## Members closes counted from a count's start (P3)
+
+The rule since P3 (`CloseTo::Members`, rules.md B-13; D-10): a close gives
+member `i` their allocation of everything the count has closed (`closed`
+before it, plus its `net`), less what the count's earlier closes gave them
+(`given i`), whatever rule those closes were made under
+(`periods::allocate_cumulative`, `kernel::apportion_cumulative`). The run
+rule of 2026-10-13 (`CloseTo::MembersRun`, `closePart`) is the special case
+where the earlier closes gave exactly the allocation. -/
+
+/-- What a cumulative close gives member `i`. -/
+def trueUp (alloc : Int → Nat → Int) (closed net : Int) (given : Nat → Int) (i : Nat) : Int :=
+  alloc (closed + net) i - given i
+
+/-- **A cumulative close hands out exactly its net**, whatever rule the
+earlier closes used, as long as they handed out what they closed. -/
+theorem trueUp_total (alloc : Int → Nat → Int) (members : List Nat)
+    (sums : ∀ x, (members.map (alloc x)).sum = x) (closed net : Int) (given : Nat → Int)
+    (hg : (members.map given).sum = closed) :
+    (members.map (trueUp alloc closed net given)).sum = net := by
+  have h := sum_map_sub (alloc (closed + net)) given members
+  unfold trueUp
+  rw [h, sums, hg]
+  omega
+
+/-- **A running total is one allocation**: after the close, what the count
+has given member `i` is their allocation of everything it closed, so its
+rounding is one allocation's, never a sum of them. -/
+theorem trueUp_running (alloc : Int → Nat → Int) (closed net : Int) (given : Nat → Int)
+    (i : Nat) : given i + trueUp alloc closed net given i = alloc (closed + net) i := by
+  unfold trueUp
+  omega
+
+/-- The run rule is the special case `given = alloc closed`. -/
+theorem closePart_eq_trueUp (alloc : Int → Nat → Int) (before net : Int) (i : Nat) :
+    closePart alloc before net i = trueUp alloc before net (alloc before) i := rfl
+
+/-- **Bounded drift, for any history**: when every allocation is under one
+unit from exact (scaled by `W`, the shares being `w i / W`), so is every
+member's running total after a cumulative close, whatever the earlier
+closes gave (`Apportion.allocW_drift` supplies the hypothesis). -/
+theorem cumulative_drift (alloc : Int → Nat → Int) (w : Nat → Int) (W : Int)
+    (hd : ∀ x i, -W < alloc x i * W - x * w i ∧ alloc x i * W - x * w i < W)
+    (closed net : Int) (given : Nat → Int) (i : Nat) :
+    -W < (given i + trueUp alloc closed net given i) * W - (closed + net) * w i ∧
+    (given i + trueUp alloc closed net given i) * W - (closed + net) * w i < W := by
+  rw [trueUp_running]
+  exact hd _ _
+
+/-- The statement of members' equity's share of the earnings `U` not yet
+closed, as of a day: what the count's next close would give of them, its
+allocation of `closed + U` less its allocation of `closed` (D-38; P3 review
+R-1: never the true-up a close hasn't posted). -/
+def unclosedShare (alloc : Int → Nat → Int) (closed U : Int) (i : Nat) : Int :=
+  alloc (closed + U) i - alloc closed i
+
+/-- **Closing a period moves a member's capital on a day by exactly the
+true-up the close posts** (D-38, R-1): before, their capital `cap` plus
+their share of the unclosed `U`; after closing `net` of it, `cap` plus the
+close's part plus their share of the rest. The difference is
+`alloc closed i - given i`. -/
+theorem statement_after_close (alloc : Int → Nat → Int) (cap closed net U : Int)
+    (given : Nat → Int) (i : Nat) :
+    cap + trueUp alloc closed net given i + unclosedShare alloc (closed + net) (U - net) i
+      = cap + unclosedShare alloc closed U i + (alloc closed i - given i) := by
+  unfold trueUp unclosedShare
+  rw [show closed + net + (U - net) = closed + U by omega]
+  omega
+
+/-- **A member's capital on a day never moves when its period is closed**
+(D-38), once the count's closes gave what the cumulative rule gives
+(`given = alloc closed`: every count the rule began, and every count after
+its first close that posts). -/
+theorem statement_unmoved_by_close (alloc : Int → Nat → Int) (cap closed net U : Int)
+    (i : Nat) :
+    cap + trueUp alloc closed net (alloc closed) i + unclosedShare alloc (closed + net) (U - net) i
+      = cap + unclosedShare alloc closed U i := by
+  rw [statement_after_close]
+  omega
+
+end Bookspec

bookspec/lean/Bookspec/Entry.lean

@@ -0,0 +1,117 @@
+import Bookspec.Basic
+
+/-!
+# Entries: acceptance, movements, reversals
+
+Mirrors `kernel::check_lines`, `kernel::movements`, `kernel::reversal`,
+and `JournalEntry::validate`.
+-/
+
+namespace Bookspec
+
+/-- What the engine accepts (the arithmetic of `JournalEntry::validate`,
+i.e. `kernel::check_lines`): two or more lines, every amount positive,
+debits equal to credits. (Range, account, and currency checks are not
+arithmetic laws and are left out of the model.) -/
+def Accepted (ls : List Line) : Prop :=
+  2 ≤ ls.length ∧ (∀ l ∈ ls, 0 < l.amount) ∧ debits ls = credits ls
+
+/-- **Every accepted entry nets to zero.** -/
+theorem Accepted.net_zero {ls : List Line} (h : Accepted ls) : net ls = 0 := by
+  rw [net_eq_debits_sub_credits]; have := h.2.2; omega
+
+/-- Net movement of account `a` over some lines. -/
+def movement (a : Nat) : List Line → Int
+  | [] => 0
+  | l :: ls => (if l.account = a then l.signed else 0) + movement a ls
+
+@[simp] theorem movement_nil (a : Nat) : movement a [] = 0 := rfl
+@[simp] theorem movement_cons (a : Nat) (l : Line) (ls : List Line) :
+    movement a (l :: ls) = (if l.account = a then l.signed else 0) + movement a ls := rfl
+
+theorem movement_append (a : Nat) (xs ys : List Line) :
+    movement a (xs ++ ys) = movement a xs + movement a ys := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih => simp only [List.cons_append, movement_cons, ih]; omega
+
+/-- **Movements partition the net.** Summed over a chart's distinct codes
+that cover every line's account, the per-account movements add up to the
+net of the lines: grouping by account loses and invents nothing. -/
+theorem sum_movements (as : List Nat) (hd : Distinct as) :
+    ∀ ls : List Line, (∀ l ∈ ls, l.account ∈ as) →
+      sumOver (fun a => movement a ls) as = net ls := by
+  intro ls
+  induction ls with
+  | nil => intro _; simpa using sumOver_zero as
+  | cons l ls ih =>
+    intro hcov
+    simp only [movement_cons, net_cons]
+    rw [sumOver_add, ih (fun m hm => hcov m (List.mem_cons_of_mem _ hm)),
+      sumOver_indicator l.account l.signed as hd (hcov l (List.mem_cons_self ..))]
+
+/-- So the movements of an accepted entry sum to zero. -/
+theorem Accepted.movements_sum_zero {ls : List Line} (h : Accepted ls) (as : List Nat)
+    (hd : Distinct as) (hcov : ∀ l ∈ ls, l.account ∈ as) :
+    sumOver (fun a => movement a ls) as = 0 := by
+  rw [sum_movements as hd ls hcov, h.net_zero]
+
+/-! ## Reversals -/
+
+/-- A line with its side flipped. -/
+def Line.reverse (l : Line) : Line := { l with side := l.side.flip }
+
+/-- A reversing entry's lines (`kernel::reversal`). -/
+def reversal (ls : List Line) : List Line := ls.map Line.reverse
+
+theorem Line.reverse_signed (l : Line) : l.reverse.signed = -l.signed := by
+  simp [Line.reverse, Line.signed, signed_flip]
+
+theorem net_reversal (ls : List Line) : net (reversal ls) = -net ls := by
+  induction ls with
+  | nil => rfl
+  | cons l ls ih =>
+    simp only [reversal, List.map_cons] at ih ⊢
+    simp only [net_cons, ih, Line.reverse_signed]; omega
+
+theorem movement_reversal (a : Nat) (ls : List Line) :
+    movement a (reversal ls) = -movement a ls := by
+  induction ls with
+  | nil => rfl
+  | cons l ls ih =>
+    simp only [reversal, List.map_cons] at ih ⊢
+    simp only [movement_cons, ih, Line.reverse_signed]
+    by_cases h : l.account = a <;> simp [Line.reverse, h] <;> omega
+
+/-- **An entry and its reversal net every account to zero.** -/
+theorem movement_with_reversal (a : Nat) (ls : List Line) :
+    movement a (ls ++ reversal ls) = 0 := by
+  rw [movement_append, movement_reversal]; omega
+
+theorem debits_reversal (ls : List Line) : debits (reversal ls) = credits ls := by
+  induction ls with
+  | nil => rfl
+  | cons l ls ih =>
+    simp only [reversal, List.map_cons] at ih ⊢
+    obtain ⟨a, s, m⟩ := l
+    cases s <;> simp [debits, credits, Line.reverse, Side.flip, ih]
+
+theorem credits_reversal (ls : List Line) : credits (reversal ls) = debits ls := by
+  induction ls with
+  | nil => rfl
+  | cons l ls ih =>
+    simp only [reversal, List.map_cons] at ih ⊢
+    obtain ⟨a, s, m⟩ := l
+    cases s <;> simp [debits, credits, Line.reverse, Side.flip, ih]
+
+/-- **A reversal is accepted exactly when the original is.** -/
+theorem accepted_reversal_iff (ls : List Line) : Accepted (reversal ls) ↔ Accepted ls := by
+  unfold Accepted
+  rw [debits_reversal, credits_reversal]
+  have hlen : (reversal ls).length = ls.length := List.length_map ..
+  have hpos : (∀ l ∈ reversal ls, 0 < l.amount) ↔ (∀ l ∈ ls, 0 < l.amount) := by
+    simp [reversal, Line.reverse]
+  rw [hlen, hpos]
+  constructor <;> rintro ⟨a, b, c⟩ <;> exact ⟨a, b, c.symm⟩
+
+end Bookspec

bookspec/lean/Bookspec/Laws.lean

@@ -0,0 +1,62 @@
+import Bookspec.Ledger
+
+/-!
+# bookspec's five laws
+
+The five laws of the first edition (`bookspec/spec/00-model.md`, "The five
+laws"), each stated once, by name, as a theorem about *every* reachable
+state of the books, ported from `verify/lean` (P13 step 4). Money is `Int`,
+an exact count of the smallest unit; any finite set of exact decimals
+scales to integers without loss, and every law is a law of addition.
+
+1. Debits equal credits (BS-entry-1).
+2. Assets = Liabilities + Equity + (Revenue - Expenses) (BS-statement-2).
+3. The trial balance balances (BS-statement-1).
+4. Net income articulates to equity: a close credits equity with exactly
+   revenue less expenses (BS-period-1).
+5. The cash-flow sections sum to the change in cash (BS-statement-3).
+-/
+
+namespace Bookspec
+
+/-- Law 1. In every reachable state the posted lines' debits equal their
+credits (`net` is debits less credits). -/
+theorem law_debits_equal_credits {L : Ledger} (r : Reachable L) :
+    net (allLines L.posted) = 0 :=
+  r.books_net_zero
+
+/-- Law 2. The accounting equation, in every reachable state. -/
+theorem law_accounting_equation {L : Ledger} (r : Reachable L) :
+    let ls := allLines L.posted
+    typeTotal .asset ls L.chart
+      = typeTotal .liability ls L.chart + typeTotal .equity ls L.chart
+        + (typeTotal .revenue ls L.chart - typeTotal .expense ls L.chart) :=
+  r.accounting_equation
+
+/-- Law 3. The trial balance balances, in every reachable state. -/
+theorem law_trial_balance {L : Ledger} (r : Reachable L) :
+    tbDebits (allLines L.posted) (codes L.chart)
+      = tbCredits (allLines L.posted) (codes L.chart) :=
+  r.trial_balance
+
+/-- Law 4. A close credits equity with exactly the period's net income. -/
+theorem law_net_income_articulates (L : Ledger) (p : Period) (ts : List (Nat × Int))
+    (hsum : total (ts.map Prod.snd)
+      = net (closings (nominalCodes L.chart) (allLines (through p.stop L.posted)))) :
+    let ls := allLines (through p.stop L.posted)
+    total (ts.map Prod.snd) = typeTotal .revenue ls L.chart - typeTotal .expense ls L.chart :=
+  close_credits_net_income L p ts hsum
+
+/-- Law 5. The three sections of the statement of cash flows sum to the
+change in the cash accounts. -/
+theorem law_cash_flow_is_change_in_cash {L : Ledger} (r : Reachable L) (b c : Nat)
+    (hbc : b ≤ c) (F : List Line → Line → Flow) (C : List Line → List Int)
+    (hC : ∀ e, sum3 (C e) = 0) (cash : List Nat) (hd : Distinct cash)
+    (hF : ∀ e l, F e l = .cash ↔ l.account ∈ cash) :
+    let es := (between b c L.posted).map Entry.lines
+    sectionTotal F C 0 es + sectionTotal F C 1 es + sectionTotal F C 2 es
+      = sumOver (fun a => movement a (allLines (through c L.posted))) cash
+        - sumOver (fun a => movement a (allLines (through b L.posted))) cash :=
+  r.cashflow_is_change_in_cash b c hbc F C hC cash hd hF
+
+end Bookspec

bookspec/lean/Bookspec/Ledger.lean

@@ -0,0 +1,562 @@
+import Bookspec.Closing
+
+/-!
+# The ledger as a state machine
+
+The engine's command surface (`Ledger`), modelled as the steps it allows:
+add an account, start a draft, post, reverse, open a period, close one.
+Each step carries the checks the engine makes before it mutates. The
+theorems below hold in *every* state reachable from empty books, by any
+sequence of commands, of any length.
+
+Mirrors `Ledger::add_account`, `try_create_entry`, `post_entry`,
+`reverse_entry`, `create_period`, and `close_period_to`; and, as one step
+`record`, everything the books keep about how they are kept: settings,
+conventions, decisions, open items and approvals (`apply_settings`,
+`apply_convention`, `apply_decision`, `apply_open_item`,
+`apply_approval`, and their retirements and resolutions), each a record
+the step adds and nothing else; and an account's rename
+(`rename_account`, `account.renamed`, rules.md B-31), since the model's
+chart is codes and types and a name is no part of it.
+-/
+
+namespace Bookspec
+
+/-- A journal entry: its id, its date (a day number), its lines. -/
+structure Entry where
+  id : Nat
+  date : Nat
+  lines : List Line
+  deriving DecidableEq
+
+/-- Every line of some entries, in order. -/
+def allLines : List Entry → List Line
+  | [] => []
+  | e :: es => e.lines ++ allLines es
+
+theorem allLines_append (xs ys : List Entry) : allLines (xs ++ ys) = allLines xs ++ allLines ys := by
+  induction xs with
+  | nil => rfl
+  | cons x xs ih => simp [allLines, ih]
+
+theorem mem_allLines {l : Line} {es : List Entry} : l ∈ allLines es ↔ ∃ e ∈ es, l ∈ e.lines := by
+  induction es with
+  | nil => simp [allLines]
+  | cons e es ih => simp [allLines, ih]
+
+/-- **Any collection of balanced entries nets to zero**: all of them, those
+dated through some day, those in some period, any filter at all. -/
+theorem net_allLines (es : List Entry) (h : ∀ e ∈ es, net e.lines = 0) : net (allLines es) = 0 := by
+  induction es with
+  | nil => rfl
+  | cons e es ih =>
+    simp only [allLines, net_append, h e (by simp), ih (fun x hx => h x (by simp [hx]))]
+    rfl
+
+/-- An accounting period: inclusive day range, open or closed. -/
+structure Period where
+  id : Nat
+  start : Nat
+  stop : Nat
+  closed : Bool
+  deriving DecidableEq
+
+/-- Whether a day falls in a period. -/
+def Period.contains (p : Period) (d : Nat) : Bool := decide (p.start ≤ d ∧ d ≤ p.stop)
+
+/-- The books: chart, posted entries in posting order, drafts, periods,
+and the record of how they are kept (settings, conventions, decisions,
+open items, approvals), each record abstracted to a number. -/
+structure Ledger where
+  chart : Chart
+  posted : List Entry
+  drafts : List Entry
+  periods : List Period
+  records : List Nat
+
+/-- Empty books. -/
+def Ledger.empty : Ledger := ⟨[], [], [], [], []⟩
+
+/-- Whether a closed period contains a day. -/
+def Ledger.closedOn (L : Ledger) (d : Nat) : Prop :=
+  ∃ p ∈ L.periods, p.closed = true ∧ p.contains d = true
+
+/-- Entries dated on or before a day. -/
+def through (d : Nat) (es : List Entry) : List Entry := es.filter (fun e => decide (e.date ≤ d))
+
+/-- Mark one period closed. -/
+def closeIn (p : Period) (ps : List Period) : List Period :=
+  ps.map (fun q => if q = p then { q with closed := true } else q)
+
+/-- The closing entry for period `p` crediting targets `ts`, if there is
+anything to close. -/
+def closingFor (L : Ledger) (p : Period) (ts : List (Nat × Int)) (id : Nat) : List Entry :=
+  if closings (nominalCodes L.chart) (allLines (through p.stop L.posted)) = [] then []
+  else [⟨id, p.stop, closingEntry (nominalCodes L.chart) ts (allLines (through p.stop L.posted))⟩]
+
+/-- What the engine allows. -/
+inductive Step : Ledger → Ledger → Prop
+  /-- `add_account`: codes are unique. -/
+  | addAccount (L : Ledger) (a : Nat) (t : AccountType) (h : a ∉ codes L.chart) :
+      Step L { L with chart := (a, t) :: L.chart }
+  /-- `try_create_entry` (and lines added to it): not in a closed period. -/
+  | draft (L : Ledger) (e : Entry) (h : ¬ L.closedOn e.date) :
+      Step L { L with drafts := e :: L.drafts }
+  /-- `post_entry`: a draft, acceptable, on known accounts, not in a closed
+  period. Appends to the log. -/
+  | post (L : Ledger) (e : Entry) (hd : e ∈ L.drafts) (ha : Accepted e.lines)
+      (hk : ∀ l ∈ e.lines, l.account ∈ codes L.chart) (hc : ¬ L.closedOn e.date) :
+      Step L { L with posted := L.posted ++ [e], drafts := L.drafts.filter (· ≠ e) }
+  /-- `reverse_entry`: a posted entry's lines, sides flipped, posted on a
+  day not in a closed period. -/
+  | reverse (L : Ledger) (e : Entry) (he : e ∈ L.posted) (r : Entry)
+      (hr : r.lines = reversal e.lines) (hc : ¬ L.closedOn r.date) :
+      Step L { L with posted := L.posted ++ [r] }
+  /-- `create_period`: periods open. -/
+  | openPeriod (L : Ledger) (p : Period) (h : p.closed = false) :
+      Step L { L with periods := p :: L.periods }
+  /-- `close_period_to`: an open period with no drafts in it, whose last day
+  is in no other closed period, with no later period closed, crediting the
+  net income to equity targets (not themselves revenue or expense) in
+  parts that sum to it. -/
+  | close (L : Ledger) (p : Period) (hp : p ∈ L.periods) (hopen : p.closed = false)
+      (hdrafts : ∀ d ∈ L.drafts, p.contains d.date = false)
+      (hother : ∀ q ∈ L.periods, q.closed = true → q.contains p.stop = false)
+      (hlater : ∀ q ∈ L.periods, q.closed = true → q.stop ≤ p.stop)
+      (ts : List (Nat × Int))
+      (hts : ∀ x ∈ ts, x.1 ∈ codes L.chart ∧ x.1 ∉ nominalCodes L.chart)
+      (hsum : total (ts.map Prod.snd)
+        = net (closings (nominalCodes L.chart) (allLines (through p.stop L.posted))))
+      (id : Nat) :
+      Step L { L with posted := L.posted ++ closingFor L p ts id, periods := closeIn p L.periods }
+  /-- `apply_settings`, `apply_convention`, `apply_decision`,
+  `apply_open_item`, `apply_approval` and their retirements and
+  resolutions, and the 1099 records `set_vendor_1099`,
+  `set_vendor_w9_flag`, `add_instrument` and `set_entry_instrument`: a
+  record of how the books are kept, and nothing else. `rename_account`
+  too: a name is outside the chart the model keeps. -/
+  | record (L : Ledger) (r : Nat) : Step L { L with records := r :: L.records }
+
+/-- States reachable from empty books. -/
+inductive Reachable : Ledger → Prop
+  | empty : Reachable Ledger.empty
+  | step {L L' : Ledger} : Reachable L → Step L L' → Reachable L'
+
+/-- What holds in every reachable state. -/
+structure Inv (L : Ledger) : Prop where
+  distinct : Distinct (codes L.chart)
+  accepted : ∀ e ∈ L.posted, Accepted e.lines
+  known : ∀ e ∈ L.posted, ∀ l ∈ e.lines, l.account ∈ codes L.chart
+  draftsOpen : ∀ d ∈ L.drafts, ¬ L.closedOn d.date
+
+theorem closedOn_closeIn (L : Ledger) (p : Period) (d : Nat) :
+    ({ L with periods := closeIn p L.periods } : Ledger).closedOn d →
+      L.closedOn d ∨ (p ∈ L.periods ∧ p.contains d = true) := by
+  rintro ⟨q, hq, hc, hd⟩
+  simp only [closeIn, List.mem_map] at hq
+  obtain ⟨q', hq', rfl⟩ := hq
+  by_cases e : q' = p
+  · subst e; right; simp at hd; exact ⟨hq', by simpa [Period.contains] using hd⟩
+  · left; simp [e] at hc hd; exact ⟨q', hq', hc, hd⟩
+
+theorem closingFor_lines (L : Ledger) (p : Period) (ts : List (Nat × Int)) (id : Nat) :
+    ∀ e ∈ closingFor L p ts id,
+      e.date = p.stop ∧ e.lines = closingEntry (nominalCodes L.chart) ts
+        (allLines (through p.stop L.posted))
+      ∧ closings (nominalCodes L.chart) (allLines (through p.stop L.posted)) ≠ [] := by
+  intro e he
+  unfold closingFor at he
+  split at he
+  · simp at he
+  · simp at he; subst he; exact ⟨rfl, rfl, by assumption⟩
+
+/-- **Every step preserves the invariant.** -/
+theorem Step.inv {L L' : Ledger} (s : Step L L') (h : Inv L) : Inv L' := by
+  cases s with
+  | addAccount a t ha =>
+    exact ⟨⟨ha, h.distinct⟩, h.accepted,
+      fun e he l hl => List.mem_cons_of_mem _ (h.known e he l hl), h.draftsOpen⟩
+  | draft e hc =>
+    refine ⟨h.distinct, h.accepted, h.known, ?_⟩
+    intro d hd
+    cases hd with
+    | head => exact hc
+    | tail _ hd => exact h.draftsOpen d hd
+  | post e hd ha hk hc =>
+    refine ⟨h.distinct, ?_, ?_, ?_⟩
+    · intro x hx
+      simp only [List.mem_append, List.mem_singleton] at hx
+      rcases hx with hx | rfl
+      · exact h.accepted x hx
+      · exact ha
+    · intro x hx
+      simp only [List.mem_append, List.mem_singleton] at hx
+      rcases hx with hx | rfl
+      · exact h.known x hx
+      · exact hk
+    · intro d hd
+      exact h.draftsOpen d ((List.mem_filter.1 hd).1)
+  | reverse e he r hr hc =>
+    refine ⟨h.distinct, ?_, ?_, h.draftsOpen⟩
+    · intro x hx
+      simp only [List.mem_append, List.mem_singleton] at hx
+      rcases hx with hx | rfl
+      · exact h.accepted x hx
+      · rw [hr, accepted_reversal_iff]; exact h.accepted e he
+    · intro x hx
+      simp only [List.mem_append, List.mem_singleton] at hx
+      rcases hx with hx | rfl
+      · exact h.known x hx
+      · intro l hl
+        rw [hr] at hl
+        simp only [reversal, List.mem_map] at hl
+        obtain ⟨l', hl', rfl⟩ := hl
+        exact h.known e he l' hl'
+  | openPeriod p hp =>
+    refine ⟨h.distinct, h.accepted, h.known, ?_⟩
+    rintro d hd ⟨q, hq, hc, hdq⟩
+    cases hq with
+    | head => simp [hp] at hc
+    | tail _ hq => exact h.draftsOpen d hd ⟨q, hq, hc, hdq⟩
+  | close p hp hopen hdrafts hother hlater ts hts hsum id =>
+    refine ⟨h.distinct, ?_, ?_, ?_⟩
+    · intro x hx
+      simp only [List.mem_append] at hx
+      rcases hx with hx | hx
+      · exact h.accepted x hx
+      · obtain ⟨-, hl, hne⟩ := closingFor_lines L p ts id x hx
+        rw [hl]; exact closingEntry_accepted _ _ _ hsum hne
+    · intro x hx
+      simp only [List.mem_append] at hx
+      rcases hx with hx | hx
+      · exact h.known x hx
+      · obtain ⟨-, hl, -⟩ := closingFor_lines L p ts id x hx
+        intro l hl'
+        rw [hl] at hl'
+        simp only [closingEntry, List.mem_append] at hl'
+        rcases hl' with hl' | hl'
+        · exact nominalCodes_sub _ _ (closings_account _ _ l hl')
+        · obtain ⟨y, hy, e⟩ := equityLines_account ts l hl'
+          rw [e]; exact (hts y hy).1
+    · intro d hd hcl
+      rcases closedOn_closeIn L p d.date hcl with hcl | ⟨-, hc⟩
+      · exact h.draftsOpen d hd hcl
+      · simp [hdrafts d hd] at hc
+  | record r => exact ⟨h.distinct, h.accepted, h.known, h.draftsOpen⟩
+
+/-- **The invariant holds in every reachable state.** -/
+theorem Reachable.inv {L : Ledger} (r : Reachable L) : Inv L := by
+  induction r with
+  | empty => exact ⟨trivial, by simp [Ledger.empty], by simp [Ledger.empty], by simp [Ledger.empty]⟩
+  | step _ s ih => exact s.inv ih
+
+/-! ## The books always balance -/
+
+/-- **The books net to zero**: in every reachable state, the posted lines'
+debits equal their credits. -/
+theorem Reachable.books_net_zero {L : Ledger} (r : Reachable L) : net (allLines L.posted) = 0 :=
+  net_allLines _ (fun e he => (r.inv.accepted e he).net_zero)
+
+/-- The same through any day: the books as of any date balance too. -/
+theorem Reachable.net_zero_through {L : Ledger} (r : Reachable L) (d : Nat) :
+    net (allLines (through d L.posted)) = 0 :=
+  net_allLines _ (fun e he => (r.inv.accepted e ((List.mem_filter.1 he).1)).net_zero)
+
+theorem Reachable.covers {L : Ledger} (r : Reachable L) (es : List Entry)
+    (hs : ∀ e ∈ es, e ∈ L.posted) : ∀ l ∈ allLines es, l.account ∈ codes L.chart := by
+  intro l hl
+  obtain ⟨e, he, hl⟩ := mem_allLines.1 hl
+  exact r.inv.known e (hs e he) l hl
+
+/-- **The trial balance balances**, in every reachable state. -/
+theorem Reachable.trial_balance {L : Ledger} (r : Reachable L) :
+    tbDebits (allLines L.posted) (codes L.chart) = tbCredits (allLines L.posted) (codes L.chart) :=
+  trial_balance_balances _ _ r.inv.distinct (r.covers _ (fun _ h => h)) r.books_net_zero
+
+/-- **The trial balance as of any date balances.** -/
+theorem Reachable.trial_balance_through {L : Ledger} (r : Reachable L) (d : Nat) :
+    tbDebits (allLines (through d L.posted)) (codes L.chart)
+      = tbCredits (allLines (through d L.posted)) (codes L.chart) :=
+  trial_balance_balances _ _ r.inv.distinct
+    (r.covers _ (fun _ h => (List.mem_filter.1 h).1)) (r.net_zero_through d)
+
+/-- **The accounting equation holds**, in every reachable state:
+Assets = Liabilities + Equity + (Revenue - Expenses). -/
+theorem Reachable.accounting_equation {L : Ledger} (r : Reachable L) :
+    let ls := allLines L.posted
+    typeTotal .asset ls L.chart
+      = typeTotal .liability ls L.chart + typeTotal .equity ls L.chart
+        + (typeTotal .revenue ls L.chart - typeTotal .expense ls L.chart) :=
+  Bookspec.accounting_equation _ _ r.inv.distinct (r.covers _ (fun _ h => h)) r.books_net_zero
+
+/-- **The balance sheet as of any date balances.** -/
+theorem Reachable.accounting_equation_through {L : Ledger} (r : Reachable L) (d : Nat) :
+    let ls := allLines (through d L.posted)
+    typeTotal .asset ls L.chart
+      = typeTotal .liability ls L.chart + typeTotal .equity ls L.chart
+        + (typeTotal .revenue ls L.chart - typeTotal .expense ls L.chart) :=
+  Bookspec.accounting_equation _ _ r.inv.distinct
+    (r.covers _ (fun _ h => (List.mem_filter.1 h).1)) (r.net_zero_through d)
+
+/-! ## Posted is forever -/
+
+/-- **Posting only appends.** No step edits, reorders, or removes a posted
+entry. -/
+theorem Step.extends {L L' : Ledger} (s : Step L L') : ∃ t, L'.posted = L.posted ++ t := by
+  cases s with
+  | addAccount => exact ⟨[], by simp⟩
+  | draft => exact ⟨[], by simp⟩
+  | post e => exact ⟨[e], rfl⟩
+  | reverse e _ r => exact ⟨[r], rfl⟩
+  | openPeriod => exact ⟨[], by simp⟩
+  | close p _ _ _ _ _ ts _ _ id => exact ⟨closingFor L p ts id, rfl⟩
+  | record => exact ⟨[], by simp⟩
+
+/-- Any number of steps. -/
+inductive Steps : Ledger → Ledger → Prop
+  | refl (L : Ledger) : Steps L L
+  | tail {L M N : Ledger} : Steps L M → Step M N → Steps L N
+
+/-- **Posted is forever**: after any sequence of commands, the old log is
+a prefix of the new one. Every posted entry keeps its place and its
+lines. -/
+theorem Steps.extends {L L' : Ledger} (s : Steps L L') : ∃ t, L'.posted = L.posted ++ t := by
+  induction s with
+  | refl => exact ⟨[], by simp⟩
+  | tail _ s ih =>
+    obtain ⟨t, ht⟩ := ih
+    obtain ⟨u, hu⟩ := s.extends
+    exact ⟨t ++ u, by rw [hu, ht, List.append_assoc]⟩
+
+/-! ## Closed periods are frozen -/
+
+/-- Entries dated in a period. -/
+def within (p : Period) (es : List Entry) : List Entry := es.filter (fun e => p.contains e.date)
+
+theorem within_append (p : Period) (xs ys : List Entry) :
+    within p (xs ++ ys) = within p xs ++ within p ys := List.filter_append ..
+
+/-- A closed period stays closed. -/
+theorem Step.keeps_closed {L L' : Ledger} (s : Step L L') (q : Period) (hq : q ∈ L.periods)
+    (hc : q.closed = true) : q ∈ L'.periods := by
+  cases s with
+  | openPeriod p _ => exact List.mem_cons_of_mem _ hq
+  | close p _ hopen =>
+    have : q ≠ p := fun e => by subst e; simp [hopen] at hc
+    exact List.mem_map.2 ⟨q, hq, by simp [this]⟩
+  | _ => exact hq
+
+/-- **A step never changes what a closed period contains.** -/
+theorem Step.frozen {L L' : Ledger} (s : Step L L') (q : Period) (hq : q ∈ L.periods)
+    (hc : q.closed = true) : within q L'.posted = within q L.posted := by
+  have nothing : ∀ e : Entry, ¬ L.closedOn e.date → within q [e] = [] := by
+    intro e he
+    simp only [within, List.filter_cons, List.filter_nil]
+    split
+    · exact absurd ⟨q, hq, hc, by assumption⟩ he
+    · rfl
+  cases s with
+  | post e _ _ _ hcl => rw [within_append, nothing e hcl, List.append_nil]
+  | reverse e _ r _ hcl => rw [within_append, nothing r hcl, List.append_nil]
+  | close p hp hopen hdrafts hother hlater ts hts hsum id =>
+    rw [within_append]
+    have : within q (closingFor L p ts id) = [] := by
+      unfold closingFor
+      split
+      · rfl
+      · simp only [within, List.filter_cons, List.filter_nil]
+        rw [hother q hq hc]; rfl
+    rw [this, List.append_nil]
+  | _ => rfl
+
+/-- **Closed periods are frozen**: once a period is closed, no sequence of
+commands adds, removes, or changes an entry dated in it. -/
+theorem Steps.frozen {L L' : Ledger} (s : Steps L L') (q : Period) (hq : q ∈ L.periods)
+    (hc : q.closed = true) : within q L'.posted = within q L.posted ∧ q ∈ L'.periods := by
+  induction s with
+  | refl => exact ⟨rfl, hq⟩
+  | tail _ s ih =>
+    obtain ⟨h1, h2⟩ := ih
+    exact ⟨(s.frozen q h2 hc).trans h1, s.keeps_closed q h2 hc⟩
+
+/-! ## Closing -/
+
+/-- **After a close, every revenue and expense account is zero through the
+period's last day.** (The trial balance still balances: the close is a
+step, and `Reachable.trial_balance` covers every step.) -/
+theorem close_zeroes {L : Ledger} (r : Reachable L) (p : Period)
+    (ts : List (Nat × Int)) (hts : ∀ x ∈ ts, x.1 ∈ codes L.chart ∧ x.1 ∉ nominalCodes L.chart)
+    (id : Nat) (a : Nat) (ha : a ∈ nominalCodes L.chart) :
+    movement a (allLines (through p.stop (L.posted ++ closingFor L p ts id))) = 0 := by
+  have hd := nominalCodes_distinct _ r.inv.distinct
+  have hta : ∀ x ∈ ts, x.1 ≠ a := fun x hx e => (hts x hx).2 (e ▸ ha)
+  rw [through, List.filter_append, ← through, allLines_append]
+  unfold closingFor
+  split
+  · rename_i hnil
+    simp only [List.filter_nil, allLines, List.append_nil]
+    exact closings_eq_nil _ _ hnil a ha
+  · simp only [List.filter_cons, Nat.le_refl, decide_true, ite_true, List.filter_nil, allLines,
+      List.append_nil]
+    exact closingEntry_zeroes _ ts _ hd a ha hta
+
+/-- **A close credits equity with exactly the period's net income**:
+revenue minus expenses through its last day, split among the targets. -/
+theorem close_credits_net_income (L : Ledger) (p : Period) (ts : List (Nat × Int))
+    (hsum : total (ts.map Prod.snd)
+      = net (closings (nominalCodes L.chart) (allLines (through p.stop L.posted)))) :
+    let ls := allLines (through p.stop L.posted)
+    total (ts.map Prod.snd) = typeTotal .revenue ls L.chart - typeTotal .expense ls L.chart := by
+  intro ls
+  rw [hsum, net_closings_is_net_income]
+
+/-! ## Period statements add up -/
+
+/-- Entries dated after day `b`, through day `c`. -/
+def between (b c : Nat) (es : List Entry) : List Entry :=
+  es.filter (fun e => decide (b < e.date ∧ e.date ≤ c))
+
+theorem movement_split (a b c : Nat) (h : b ≤ c) (es : List Entry) :
+    movement a (allLines (through c es))
+      = movement a (allLines (through b es)) + movement a (allLines (between b c es)) := by
+  induction es with
+  | nil => rfl
+  | cons e es ih =>
+    simp only [through, between] at ih ⊢
+    by_cases h1 : e.date ≤ b
+    · have h2 : e.date ≤ c := by omega
+      have h3 : ¬ (b < e.date ∧ e.date ≤ c) := by omega
+      rw [List.filter_cons_of_pos (by simpa using h2), List.filter_cons_of_pos (by simpa using h1),
+        List.filter_cons_of_neg (by simpa using h3)]
+      simp only [allLines, movement_append, ih]; omega
+    · by_cases h2 : e.date ≤ c
+      · have h3 : b < e.date ∧ e.date ≤ c := by omega
+        rw [List.filter_cons_of_pos (by simpa using h2), List.filter_cons_of_neg (by simpa using h1),
+          List.filter_cons_of_pos (by simpa using h3)]
+        simp only [allLines, movement_append, ih]; omega
+      · have h3 : ¬ (b < e.date ∧ e.date ≤ c) := by omega
+        rw [List.filter_cons_of_neg (by simpa using h2), List.filter_cons_of_neg (by simpa using h1),
+          List.filter_cons_of_neg (by simpa using h3)]
+        exact ih
+
+theorem typeTotal_split (t : AccountType) (x y z : List Line)
+    (h : ∀ a, movement a x = movement a y + movement a z) (c : Chart) :
+    typeTotal t x c = typeTotal t y c + typeTotal t z c := by
+  induction c with
+  | nil => rfl
+  | cons p c ih =>
+    obtain ⟨a, t'⟩ := p
+    simp only [typeTotal, h a, ih]
+    split
+    · cases t' <;> simp [balance, AccountType.normal, signed] <;> omega
+    · omega
+
+/-- **Period statements add up**: every account type's total (so revenue,
+expenses, and net income) through day `c` is its total through day `b`
+plus its total for the days after `b` through `c`. A year's P&L is the sum
+of its months'. -/
+theorem statements_add_up (t : AccountType) (b c : Nat) (h : b ≤ c) (es : List Entry)
+    (chart : Chart) :
+    typeTotal t (allLines (through c es)) chart
+      = typeTotal t (allLines (through b es)) chart
+        + typeTotal t (allLines (between b c es)) chart :=
+  typeTotal_split t _ _ _ (fun a => movement_split a b c h es) chart
+
+/-! ## The statement of cash flows foots (rules.md B-14 rule 9) -/
+
+/-- Some entries' cash, summed, is the movement of the cash accounts over
+their lines, when the cash tag follows the account. -/
+theorem cashTotal_is_movement (F : List Line → Line → Flow) (cash : List Nat)
+    (hd : Distinct cash) (hF : ∀ e l, F e l = .cash ↔ l.account ∈ cash) :
+    ∀ xs : List Entry,
+      cashTotal F (xs.map Entry.lines) = sumOver (fun a => movement a (allLines xs)) cash := by
+  intro xs
+  induction xs with
+  | nil => simpa [cashTotal, allLines] using (sumOver_zero cash).symm
+  | cons x xs ih =>
+    simp only [List.map_cons, cashTotal, allLines, movement_append]
+    rw [sumOver_add, ← ih, cashOf, secNet_cash_is_movement (F x.lines) cash hd (hF x.lines)]
+
+/-- **The statement of cash flows foots**, in every reachable state: over
+the posted entries dated after day `b` through day `c` (any selection of
+them, `p`: the engine leaves out closing entries), operating + investing +
+financing is the movement of the cash accounts over the same entries, for
+any tagging whose cash tag follows the account, and whatever a member or
+lender handled for each entry (`C`, rule 11) as long as it nets to zero
+(`constructive_nets`). Every posted entry is accepted (`Reachable.inv`),
+so each nets to zero. -/
+theorem Reachable.cashflow_foots {L : Ledger} (r : Reachable L) (b c : Nat) (p : Entry → Bool)
+    (F : List Line → Line → Flow) (C : List Line → List Int) (hC : ∀ e, sum3 (C e) = 0)
+    (cash : List Nat) (hd : Distinct cash)
+    (hF : ∀ e l, F e l = .cash ↔ l.account ∈ cash) :
+    let xs := (between b c L.posted).filter p
+    sectionTotal F C 0 (xs.map Entry.lines) + sectionTotal F C 1 (xs.map Entry.lines)
+        + sectionTotal F C 2 (xs.map Entry.lines)
+      = sumOver (fun a => movement a (allLines xs)) cash := by
+  intro xs
+  rw [cashflow_sections_sum_to_cash_change, cashTotal_is_movement F cash hd hF]
+  · intro e he
+    obtain ⟨x, hx, rfl⟩ := List.mem_map.1 he
+    have hb := (List.mem_filter.1 hx).1
+    exact (r.inv.accepted x (List.mem_filter.1 hb).1).net_zero
+  · exact fun e _ => hC e
+
+/-- **The sections are the change in the cash accounts' balances**: with
+every entry between `b` and `c` counted, the three sections sum to the
+cash accounts' movement through `c` less their movement through `b`
+(their ending balance less their beginning balance). -/
+theorem Reachable.cashflow_is_change_in_cash {L : Ledger} (r : Reachable L) (b c : Nat)
+    (hbc : b ≤ c) (F : List Line → Line → Flow) (C : List Line → List Int)
+    (hC : ∀ e, sum3 (C e) = 0) (cash : List Nat) (hd : Distinct cash)
+    (hF : ∀ e l, F e l = .cash ↔ l.account ∈ cash) :
+    let es := (between b c L.posted).map Entry.lines
+    sectionTotal F C 0 es + sectionTotal F C 1 es + sectionTotal F C 2 es
+      = sumOver (fun a => movement a (allLines (through c L.posted))) cash
+        - sumOver (fun a => movement a (allLines (through b L.posted))) cash := by
+  intro es
+  have h := r.cashflow_foots b c (fun _ => true) F C hC cash hd hF
+  have hall : (between b c L.posted).filter (fun _ => true) = between b c L.posted :=
+    List.filter_eq_self.2 (fun _ _ => rfl)
+  simp only [hall] at h
+  rw [h]
+  have hs : ∀ a, movement a (allLines (through c L.posted))
+      = movement a (allLines (through b L.posted)) + movement a (allLines (between b c L.posted)) :=
+    fun a => movement_split a b c hbc L.posted
+  rw [sumOver_congr _ _ cash (fun a _ => hs a), sumOver_add]
+  omega
+
+/-- **A reversal and its original in one period drop out together**: for
+an entry and its reversal (lines flipped, tagged as the original's, and
+what was handled for it mirrored, `constructive_neg`), the sum of their
+flows in each section is zero. -/
+theorem cashflow_reversal_nets (F : List Line → Line → Flow) (C : List Line → List Int)
+    (e : List Line) (hF : ∀ l ∈ e, F (reversal e) l.reverse = F e l)
+    (hC : C (reversal e) = (C e).map (fun x => -x)) (k : Nat) :
+    sectionTotal F C k [e, reversal e] = 0 := by
+  simp only [sectionTotal, stmt_flows_reversal F C e hF hC, getD_neg]
+  omega
+
+/-! ## How the books are kept changes no figure -/
+
+/-- **A record changes nothing the books hold**: a settings change, a
+convention, a decision, an open item or an approval leaves the chart, every
+posted entry, every draft and every period exactly as they were. (The
+`record` step touches only `records` by definition: this pins the model.
+The engine's side is checked in Rust by `settings_replay_is_pure`.
+Settings that change how the same entries are presented, such as the
+fiscal year, are outside the model.) -/
+theorem Step.record_changes_no_figure (L : Ledger) (r : Nat) :
+    let L' : Ledger := { L with records := r :: L.records }
+    L'.chart = L.chart ∧ L'.posted = L.posted ∧ L'.drafts = L.drafts ∧ L'.periods = L.periods :=
+  ⟨rfl, rfl, rfl, rfl⟩
+
+/-- **Any number of records changes no figure**, and they keep the
+invariant: a reachable state plus records is reachable, with the same
+books. -/
+theorem Reachable.records {L : Ledger} (h : Reachable L) (rs : List Nat) :
+    Reachable { L with records := rs ++ L.records } := by
+  induction rs with
+  | nil => simpa using h
+  | cons r rs ih => exact Reachable.step ih (Step.record _ r)
+
+end Bookspec

bookspec/lean/Bookspec/Statements.lean

@@ -0,0 +1,683 @@
+import Bookspec.Entry
+
+/-!
+# Balances and statements
+
+Mirrors `kernel::normal_balance`, `kernel::columns`,
+`Ledger::account_balance`, and `reports::trial_balance`; and the statement
+of cash flows (`kernel::take`, `kernel::apply_cash`, `kernel::entry_flows`,
+`kernel::constructive`, `cashflow::cash_flow`'s footing and reconciliation
+checks).
+-/
+
+namespace Bookspec
+
+/-- A chart of accounts: each account's code and type. -/
+abbrev Chart := List (Nat × AccountType)
+
+/-- The chart's codes. -/
+def codes (c : Chart) : List Nat := c.map Prod.fst
+
+@[simp] theorem codes_nil : codes [] = [] := rfl
+@[simp] theorem codes_cons (a : Nat) (t : AccountType) (c : Chart) :
+    codes ((a, t) :: c) = a :: codes c := rfl
+
+/-- An account's balance on its normal side (`kernel::normal_balance`). -/
+def balance (t : AccountType) (m : Int) : Int := signed t.normal m
+
+/-- **A normal-side line raises a balance by its amount; an opposite-side
+line lowers it.** -/
+theorem balance_after_line (t : AccountType) (m : Int) (s : Side) (a : Int) :
+    balance t (m + signed s a) = balance t m + (if s = t.normal then a else -a) := by
+  cases t <;> cases s <;> simp [balance, AccountType.normal, signed] <;> omega
+
+/-- The total balance of every account of type `t`. -/
+def typeTotal (t : AccountType) (ls : List Line) : Chart → Int
+  | [] => 0
+  | (a, t') :: rest => (if t' = t then balance t' (movement a ls) else 0) + typeTotal t ls rest
+
+/-- The accounting equation's two sides differ by the net movement of the
+chart's accounts. -/
+theorem equation_gap (ls : List Line) (c : Chart) :
+    typeTotal .asset ls c + typeTotal .expense ls c
+      - typeTotal .liability ls c - typeTotal .equity ls c - typeTotal .revenue ls c
+      = sumOver (fun a => movement a ls) (codes c) := by
+  induction c with
+  | nil => rfl
+  | cons x c ih =>
+    obtain ⟨a, t⟩ := x
+    cases t <;> simp [typeTotal, balance, AccountType.normal, signed] <;> omega
+
+/-- **The accounting equation.** For lines that net to zero, over a chart
+with distinct codes covering every line's account:
+Assets = Liabilities + Equity + (Revenue - Expenses). -/
+theorem accounting_equation (ls : List Line) (c : Chart) (hd : Distinct (codes c))
+    (hcov : ∀ l ∈ ls, l.account ∈ codes c) (hnet : net ls = 0) :
+    typeTotal .asset ls c
+      = typeTotal .liability ls c + typeTotal .equity ls c
+        + (typeTotal .revenue ls c - typeTotal .expense ls c) := by
+  have := equation_gap ls c
+  rw [sum_movements _ hd ls hcov, hnet] at this
+  omega
+
+/-! ## Trial balance -/
+
+/-- The debit column for a movement (`kernel::columns`). -/
+def colDebit (m : Int) : Int := if 0 < m then m else 0
+/-- The credit column for a movement (`kernel::columns`). -/
+def colCredit (m : Int) : Int := if 0 < m then 0 else -m
+
+theorem columns_spec (m : Int) :
+    0 ≤ colDebit m ∧ 0 ≤ colCredit m ∧ (colDebit m = 0 ∨ colCredit m = 0)
+      ∧ colDebit m - colCredit m = m := by
+  unfold colDebit colCredit; split <;> omega
+
+/-- The trial balance's debit column total. -/
+def tbDebits (ls : List Line) (as : List Nat) : Int := sumOver (fun a => colDebit (movement a ls)) as
+/-- The trial balance's credit column total. -/
+def tbCredits (ls : List Line) (as : List Nat) : Int :=
+  sumOver (fun a => colCredit (movement a ls)) as
+
+theorem tb_gap (ls : List Line) (as : List Nat) :
+    tbDebits ls as - tbCredits ls as = sumOver (fun a => movement a ls) as := by
+  induction as with
+  | nil => rfl
+  | cons a as ih =>
+    simp only [tbDebits, tbCredits, sumOver_cons] at ih ⊢
+    have := (columns_spec (movement a ls)).2.2.2
+    omega
+
+/-- **The trial balance balances** for lines that net to zero. -/
+theorem trial_balance_balances (ls : List Line) (as : List Nat) (hd : Distinct as)
+    (hcov : ∀ l ∈ ls, l.account ∈ as) (hnet : net ls = 0) :
+    tbDebits ls as = tbCredits ls as := by
+  have := tb_gap ls as
+  rw [sum_movements as hd ls hcov, hnet] at this
+  omega
+
+/-- And conversely: a balanced trial balance means the lines net to zero.
+The trial balance is a complete check of the books' arithmetic. -/
+theorem trial_balance_iff (ls : List Line) (as : List Nat) (hd : Distinct as)
+    (hcov : ∀ l ∈ ls, l.account ∈ as) :
+    tbDebits ls as = tbCredits ls as ↔ net ls = 0 := by
+  have := tb_gap ls as
+  rw [sum_movements as hd ls hcov] at this
+  omega
+
+/-! ## The statement of cash flows (rules.md B-14)
+
+Mirrors `kernel::Flow`, `kernel::take`, `kernel::apply_cash` and
+`kernel::entry_flows`, and the identities `cashflow::cash_flow` checks at
+runtime: the sections sum to the cash accounts' change, a reversal's flows
+are its original's negated, and net income reconciles to operating cash.
+
+Lines are tagged per entry (`F : List Line → Line → Flow`), as the engine
+tags them: a revenue or expense line is operating in one entry and
+investing in another (rule 4), and a reversal is tagged by its chain's
+root. The theorems hold for every such tagging; their hypotheses say what
+the engine guarantees (the cash tag follows the account; revenue and
+expense lines are operating or investing; a reversal's lines take its
+original's tags). A line the engine splits between two sections (the bill
+split, rule 12) is two lines here; a split keeps the entry's net. -/
+
+/-- Where a line falls on the statement of cash flows (`kernel::Flow`). -/
+inductive Flow where
+  | cash
+  | operating
+  | investing
+  | financing
+  deriving DecidableEq, Repr
+
+/-- The net movement of the lines `f` tags `k`. -/
+def secNet (f : Line → Flow) (k : Flow) : List Line → Int
+  | [] => 0
+  | l :: ls => (if f l = k then l.signed else 0) + secNet f k ls
+
+@[simp] theorem secNet_nil (f : Line → Flow) (k : Flow) : secNet f k [] = 0 := rfl
+@[simp] theorem secNet_cons (f : Line → Flow) (k : Flow) (l : Line) (ls : List Line) :
+    secNet f k (l :: ls) = (if f l = k then l.signed else 0) + secNet f k ls := rfl
+
+/-- **Every line is in exactly one place**: an entry's net is its cash plus
+its three sections' movements. -/
+theorem net_splits_by_flow (f : Line → Flow) (ls : List Line) :
+    net ls = secNet f .cash ls + secNet f .operating ls + secNet f .investing ls
+      + secNet f .financing ls := by
+  induction ls with
+  | nil => rfl
+  | cons l ls ih =>
+    simp only [net_cons, secNet_cons, ih]
+    cases f l <;> simp <;> omega
+
+/-- The cash one section takes from what is left (`kernel::take`): only a
+section moving against the cash, never more than its own movement. -/
+def take (rem n : Int) : Int :=
+  if 0 < rem ∧ n < 0 then min rem (-n) else if rem < 0 ∧ 0 < n then max rem (-n) else 0
+
+/-- `kernel::apply_cash`: the cash applied to each movement in order, and
+what is left. -/
+def applyCash : Int → List Int → List Int × Int
+  | rem, [] => ([], rem)
+  | rem, n :: ns => (take rem n :: (applyCash (rem - take rem n) ns).1,
+      (applyCash (rem - take rem n) ns).2)
+
+/-- A sum of integers. -/
+def isum : List Int → Int
+  | [] => 0
+  | x :: xs => x + isum xs
+
+@[simp] theorem isum_nil : isum [] = 0 := rfl
+@[simp] theorem isum_cons (x : Int) (xs : List Int) : isum (x :: xs) = x + isum xs := rfl
+
+theorem isum_append (xs ys : List Int) : isum (xs ++ ys) = isum xs + isum ys := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih => simp only [List.cons_append, isum_cons, ih]; omega
+
+theorem isum_neg (xs : List Int) : isum (xs.map (fun x => -x)) = -isum xs := by
+  induction xs with
+  | nil => rfl
+  | cons x xs ih => simp only [List.map_cons, isum_cons, ih]; omega
+
+/-- Applying cash invents and loses nothing: the parts and what is left
+sum to the cash. -/
+theorem applyCash_conserves (rem : Int) (ns : List Int) :
+    isum (applyCash rem ns).1 + (applyCash rem ns).2 = rem := by
+  induction ns generalizing rem with
+  | nil => simp [applyCash]
+  | cons n ns ih =>
+    simp only [applyCash, isum_cons]
+    have := ih (rem - take rem n)
+    omega
+
+theorem applyCash_length (rem : Int) (ns : List Int) :
+    (applyCash rem ns).1.length = ns.length := by
+  induction ns generalizing rem with
+  | nil => rfl
+  | cons n ns ih => simp [applyCash, ih]
+
+theorem take_zero (n : Int) : take 0 n = 0 := by
+  simp [take]
+
+/-- With no cash, nothing is applied and nothing is left. -/
+theorem applyCash_zero (ns : List Int) : (applyCash 0 ns).2 = 0 := by
+  induction ns with
+  | nil => rfl
+  | cons n ns ih => simp [applyCash, take_zero, ih]
+
+/-- Cash in is used up when the movements against it cover it. -/
+theorem applyCash_exhausts_pos (rem : Int) (ns : List Int) (h0 : 0 ≤ rem)
+    (h : rem + isum ns ≤ 0) : (applyCash rem ns).2 = 0 := by
+  induction ns generalizing rem with
+  | nil => simp [applyCash] at h ⊢; omega
+  | cons n ns ih =>
+    simp only [applyCash]
+    simp only [isum_cons] at h
+    by_cases hr : rem = 0
+    · subst hr; simp [take_zero, applyCash_zero]
+    · by_cases hn : n < 0
+      · by_cases hle : -n ≤ rem
+        · have ht : take rem n = -n := by
+            simp only [take]; rw [ite_eq_left (by omega)]; omega
+          rw [ht]; exact ih _ (by omega) (by omega)
+        · have ht : take rem n = rem := by
+            simp only [take]; rw [ite_eq_left (by omega)]; omega
+          rw [ht, Int.sub_self]; exact applyCash_zero ns
+      · have ht : take rem n = 0 := by
+          simp only [take]; rw [ite_eq_right (by omega), ite_eq_right (by omega)]
+        rw [ht, Int.sub_zero]; exact ih _ h0 (by omega)
+
+/-- Cash out is used up when the movements against it cover it. -/
+theorem applyCash_exhausts_neg (rem : Int) (ns : List Int) (h0 : rem ≤ 0)
+    (h : 0 ≤ rem + isum ns) : (applyCash rem ns).2 = 0 := by
+  induction ns generalizing rem with
+  | nil => simp [applyCash] at h ⊢; omega
+  | cons n ns ih =>
+    simp only [applyCash]
+    simp only [isum_cons] at h
+    by_cases hr : rem = 0
+    · subst hr; simp [take_zero, applyCash_zero]
+    · by_cases hn : 0 < n
+      · by_cases hle : rem ≤ -n
+        · have ht : take rem n = -n := by
+            simp only [take]; rw [ite_eq_right (by omega), ite_eq_left (by omega)]; omega
+          rw [ht]; exact ih _ (by omega) (by omega)
+        · have ht : take rem n = rem := by
+            simp only [take]; rw [ite_eq_right (by omega), ite_eq_left (by omega)]; omega
+          rw [ht, Int.sub_self]; exact applyCash_zero ns
+      · have ht : take rem n = 0 := by
+          simp only [take]; rw [ite_eq_right (by omega), ite_eq_right (by omega)]
+        rw [ht, Int.sub_zero]; exact ih _ h0 (by omega)
+
+/-- **Balanced, the cash is used up**: when the cash and the movements sum
+to zero, nothing is left over. -/
+theorem applyCash_exhausts (rem : Int) (ns : List Int) (h : rem + isum ns = 0) :
+    (applyCash rem ns).2 = 0 := by
+  rcases Int.le_total 0 rem with h0 | h0
+  · exact applyCash_exhausts_pos rem ns h0 (by omega)
+  · exact applyCash_exhausts_neg rem ns h0 (by omega)
+
+theorem take_neg (r n : Int) : take (-r) (-n) = -take r n := by
+  simp only [take]
+  by_cases h1 : 0 < r ∧ n < 0
+  · rw [ite_eq_right (by omega), ite_eq_left (by omega), ite_eq_left h1]; omega
+  · by_cases h2 : r < 0 ∧ 0 < n
+    · rw [ite_eq_left (by omega), ite_eq_right h1, ite_eq_left h2]; omega
+    · rw [ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right h1, ite_eq_right h2]; omega
+
+/-- Applying minus the cash to minus the movements gives minus the parts:
+what lets a reversal mirror its original. -/
+theorem applyCash_neg (rem : Int) (ns : List Int) :
+    applyCash (-rem) (ns.map (fun x => -x))
+      = ((applyCash rem ns).1.map (fun x => -x), -(applyCash rem ns).2) := by
+  induction ns generalizing rem with
+  | nil => rfl
+  | cons n ns ih =>
+    simp only [List.map_cons, applyCash, take_neg]
+    have : -rem - -take rem n = -(rem - take rem n) := by omega
+    rw [this, ih]
+
+/-- An entry's cash: the net of the lines tagged cash. -/
+def cashOf (F : List Line → Line → Flow) (e : List Line) : Int := secNet (F e) .cash e
+
+/-- An entry's section movements, `[operating, investing, financing]`. -/
+def moves (F : List Line → Line → Flow) (e : List Line) : List Int :=
+  [secNet (F e) .operating e, secNet (F e) .investing e, secNet (F e) .financing e]
+
+/-- An entry's cash flows per section (`kernel::entry_flows`). -/
+def flows (F : List Line → Line → Flow) (e : List Line) : List Int :=
+  (applyCash (cashOf F e) (moves F e)).1
+
+/-- **An entry's cash flows sum to its cash** (`entry_flows_sum`): for a
+balanced entry, the sections' cash is exactly the cash that moved. -/
+theorem entry_flows_sum (F : List Line → Line → Flow) (e : List Line) (h : net e = 0) :
+    isum (flows F e) = cashOf F e := by
+  have hb := net_splits_by_flow (F e) e
+  have hx : (applyCash (cashOf F e) (moves F e)).2 = 0 := by
+    apply applyCash_exhausts
+    simp only [moves, cashOf, isum_cons, isum_nil]
+    omega
+  have := applyCash_conserves (cashOf F e) (moves F e)
+  simp only [flows]
+  omega
+
+theorem flows_length (F : List Line → Line → Flow) (e : List Line) : (flows F e).length = 3 := by
+  simp [flows, applyCash_length, moves]
+
+theorem secNet_reversal (f g : Line → Flow) (k : Flow) (ls : List Line)
+    (h : ∀ l ∈ ls, g l.reverse = f l) : secNet g k (reversal ls) = -secNet f k ls := by
+  induction ls with
+  | nil => rfl
+  | cons l ls ih =>
+    simp only [reversal, List.map_cons] at ih ⊢
+    simp only [secNet_cons, h l (by simp), Line.reverse_signed,
+      ih (fun m hm => h m (by simp [hm]))]
+    split <;> omega
+
+/-- **A reversal's flows are its original's, negated** (`flows_reversal`),
+when its lines take its original's tags: what lets an entry and its
+reversal drop out of the statement together (rules.md B-14 rule 6). -/
+theorem flows_reversal (F : List Line → Line → Flow) (e : List Line)
+    (hF : ∀ l ∈ e, F (reversal e) l.reverse = F e l) :
+    flows F (reversal e) = (flows F e).map (fun x => -x) := by
+  simp only [flows, cashOf, moves]
+  rw [secNet_reversal (F e) (F (reversal e)) .cash e hF,
+    secNet_reversal (F e) (F (reversal e)) .operating e hF,
+    secNet_reversal (F e) (F (reversal e)) .investing e hF,
+    secNet_reversal (F e) (F (reversal e)) .financing e hF]
+  have := applyCash_neg (secNet (F e) .cash e)
+    [secNet (F e) .operating e, secNet (F e) .investing e, secNet (F e) .financing e]
+  simp only [List.map_cons, List.map_nil] at this
+  rw [this]
+
+theorem isum_three (xs : List Int) (h : xs.length = 3) :
+    isum xs = xs.getD 0 0 + xs.getD 1 0 + xs.getD 2 0 := by
+  match xs, h with
+  | [a, b, c], _ => simp; omega
+
+/-! ### What a member or lender pays or receives for the company (rule 11)
+
+`kernel::constructive` (D-42): what is left unsettled of an entry's
+kinds that can pay or receive for the company (`s`, a financing liability
+or a member's capital) settles what is left of the kinds they pay or
+receive for (`u`), as if through the cash accounts. The engine sums the
+parts by section into an entry's constructive triple; the entry theorems
+below take any triple that nets to zero (and, for reversals, mirrors),
+which `constructive_nets` and `constructive_neg` give the kernel's. -/
+
+/-- The credits among some movements, `Σ max(-m, 0)`: what cash in can
+settle. -/
+def creditTotal : List Int → Int
+  | [] => 0
+  | m :: ms => max (-m) 0 + creditTotal ms
+
+/-- The debits among some movements, `Σ max(m, 0)`: what cash out can
+settle. -/
+def debitTotal : List Int → Int
+  | [] => 0
+  | m :: ms => max m 0 + debitTotal ms
+
+theorem creditTotal_nonneg (ms : List Int) : 0 ≤ creditTotal ms := by
+  induction ms with
+  | nil => simp [creditTotal]
+  | cons m ms ih => simp only [creditTotal]; omega
+
+theorem debitTotal_nonneg (ms : List Int) : 0 ≤ debitTotal ms := by
+  induction ms with
+  | nil => simp [debitTotal]
+  | cons m ms ih => simp only [debitTotal]; omega
+
+theorem creditTotal_neg (ms : List Int) :
+    creditTotal (ms.map (fun x => -x)) = debitTotal ms := by
+  induction ms with
+  | nil => rfl
+  | cons m ms ih => simp only [List.map_cons, creditTotal, debitTotal, ih]; omega
+
+theorem debitTotal_neg (ms : List Int) :
+    debitTotal (ms.map (fun x => -x)) = creditTotal ms := by
+  induction ms with
+  | nil => rfl
+  | cons m ms ih =>
+    simp only [List.map_cons, creditTotal, debitTotal, ih]
+
+/-- Cash in is used up when the credits cover it (whatever the debits). -/
+theorem applyCash_exhausts_in (rem : Int) (ns : List Int) (h0 : 0 ≤ rem)
+    (h : rem ≤ creditTotal ns) : (applyCash rem ns).2 = 0 := by
+  induction ns generalizing rem with
+  | nil => simp [applyCash, creditTotal] at h ⊢; omega
+  | cons n ns ih =>
+    simp only [applyCash]
+    simp only [creditTotal] at h
+    by_cases hr : rem = 0
+    · subst hr; simp [take_zero, applyCash_zero]
+    · by_cases hn : n < 0
+      · by_cases hle : -n ≤ rem
+        · have ht : take rem n = -n := by
+            simp only [take]; rw [ite_eq_left (by omega)]; omega
+          rw [ht]; exact ih _ (by omega) (by omega)
+        · have ht : take rem n = rem := by
+            simp only [take]; rw [ite_eq_left (by omega)]; omega
+          rw [ht, Int.sub_self]; exact applyCash_zero ns
+      · have ht : take rem n = 0 := by
+          simp only [take]; rw [ite_eq_right (by omega), ite_eq_right (by omega)]
+        rw [ht, Int.sub_zero]; exact ih _ h0 (by omega)
+
+/-- Cash out is used up when the debits cover it (whatever the credits). -/
+theorem applyCash_exhausts_out (rem : Int) (ns : List Int) (h0 : rem ≤ 0)
+    (h : -rem ≤ debitTotal ns) : (applyCash rem ns).2 = 0 := by
+  induction ns generalizing rem with
+  | nil => simp [applyCash, debitTotal] at h ⊢; omega
+  | cons n ns ih =>
+    simp only [applyCash]
+    simp only [debitTotal] at h
+    by_cases hr : rem = 0
+    · subst hr; simp [take_zero, applyCash_zero]
+    · by_cases hn : 0 < n
+      · by_cases hle : rem ≤ -n
+        · have ht : take rem n = -n := by
+            simp only [take]; rw [ite_eq_right (by omega), ite_eq_left (by omega)]; omega
+          rw [ht]; exact ih _ (by omega) (by omega)
+        · have ht : take rem n = rem := by
+            simp only [take]; rw [ite_eq_right (by omega), ite_eq_left (by omega)]; omega
+          rw [ht, Int.sub_self]; exact applyCash_zero ns
+      · have ht : take rem n = 0 := by
+          simp only [take]; rw [ite_eq_right (by omega), ite_eq_right (by omega)]
+        rw [ht, Int.sub_zero]; exact ih _ h0 (by omega)
+
+/-- Which way the money went (`kernel::OnBehalf`). -/
+inductive OnBehalf where
+  | paid
+  | received
+  deriving DecidableEq, Repr
+
+/-- The other way: what a reversal does. -/
+def OnBehalf.mirror : OnBehalf → OnBehalf
+  | .paid => .received
+  | .received => .paid
+
+/-- The cash the sources take, + in (`kernel::constructive`): paid, the
+smaller of the sources' credits and the uses' debits; received, minus the
+smaller of the sources' debits and the uses' credits. -/
+def onBehalfCash : OnBehalf → List Int → List Int → Int
+  | .paid, s, u => min (creditTotal s) (debitTotal u)
+  | .received, s, u => -min (debitTotal s) (creditTotal u)
+
+/-- `kernel::constructive`: the sources' parts and the uses' parts. -/
+def constructive (w : OnBehalf) (s u : List Int) : List Int × List Int :=
+  ((applyCash (onBehalfCash w s u) s).1, (applyCash (-onBehalfCash w s u) u).1)
+
+/-- **What a member or lender handled for the company nets to zero**
+(`constructive_nets`; Kani `constructive_nets_to_zero`): the sources take
+exactly what the uses give, so an entry's flows still sum to its cash. -/
+theorem constructive_nets (w : OnBehalf) (s u : List Int) :
+    isum (constructive w s u).1 + isum (constructive w s u).2 = 0 := by
+  have hs := applyCash_conserves (onBehalfCash w s u) s
+  have hu := applyCash_conserves (-onBehalfCash w s u) u
+  have cs := creditTotal_nonneg s
+  have ds := debitTotal_nonneg s
+  have cu := creditTotal_nonneg u
+  have du := debitTotal_nonneg u
+  have ⟨xs, xu⟩ : (applyCash (onBehalfCash w s u) s).2 = 0 ∧
+      (applyCash (-onBehalfCash w s u) u).2 = 0 := by
+    cases w with
+    | paid =>
+      simp only [onBehalfCash]
+      exact ⟨applyCash_exhausts_in _ _ (by omega) (by omega),
+        applyCash_exhausts_out _ _ (by omega) (by omega)⟩
+    | received =>
+      simp only [onBehalfCash]
+      exact ⟨applyCash_exhausts_out _ _ (by omega) (by omega),
+        applyCash_exhausts_in _ _ (by omega) (by omega)⟩
+  simp only [constructive]
+  omega
+
+theorem onBehalfCash_mirror (w : OnBehalf) (s u : List Int) :
+    onBehalfCash w.mirror (s.map (fun x => -x)) (u.map (fun x => -x))
+      = -onBehalfCash w s u := by
+  cases w <;> simp only [OnBehalf.mirror, onBehalfCash, creditTotal_neg, debitTotal_neg] <;> omega
+
+/-- **The other way, minus the sources and uses give minus the parts**
+(`constructive_neg`; Kani `constructive_mirrors`): a payment made for the
+company and its reversal drop out together. -/
+theorem constructive_neg (w : OnBehalf) (s u : List Int) :
+    constructive w.mirror (s.map (fun x => -x)) (u.map (fun x => -x))
+      = ((constructive w s u).1.map (fun x => -x), (constructive w s u).2.map (fun x => -x)) := by
+  simp only [constructive, onBehalfCash_mirror]
+  rw [applyCash_neg (onBehalfCash w s u) s, applyCash_neg (-onBehalfCash w s u) u]
+
+/-- Three sections' figures, summed. -/
+def sum3 (xs : List Int) : Int := xs.getD 0 0 + xs.getD 1 0 + xs.getD 2 0
+
+@[simp] theorem sum3_cons (a b c : Int) : sum3 [a, b, c] = a + b + c := by
+  simp [sum3]
+
+/-- **The kernel's parts, by section, net to zero**: split the uses into
+operating ones then investing ones (`kernel::constructive` takes them in
+that order), and the triple (operating, investing, financing = the
+sources) the engine adds to an entry's flows sums to zero. -/
+theorem constructive_sections_net (w : OnBehalf) (s uo ui : List Int) :
+    sum3 [isum ((constructive w s (uo ++ ui)).2.take uo.length),
+      isum ((constructive w s (uo ++ ui)).2.drop uo.length),
+      isum (constructive w s (uo ++ ui)).1] = 0 := by
+  have h := constructive_nets w s (uo ++ ui)
+  have hs := isum_append ((constructive w s (uo ++ ui)).2.take uo.length)
+    ((constructive w s (uo ++ ui)).2.drop uo.length)
+  rw [List.take_append_drop] at hs
+  rw [sum3_cons]
+  omega
+
+/-- Passes add: two triples that net to zero add to one that does. -/
+theorem sum3_add (xs ys : List Int) (hx : sum3 xs = 0) (hy : sum3 ys = 0) :
+    sum3 [xs.getD 0 0 + ys.getD 0 0, xs.getD 1 0 + ys.getD 1 0, xs.getD 2 0 + ys.getD 2 0] = 0 := by
+  rw [sum3_cons]
+  simp only [sum3] at hx hy
+  omega
+
+/-- Two triples, added section by section. -/
+def add3 (xs ys : List Int) : List Int :=
+  [xs.getD 0 0 + ys.getD 0 0, xs.getD 1 0 + ys.getD 1 0, xs.getD 2 0 + ys.getD 2 0]
+
+/-- An entry's flows on the statement: its cash flows, plus `C e`, what a
+member or lender paid or received for it, by section (rule 11). -/
+def stmtFlows (F : List Line → Line → Flow) (C : List Line → List Int) (e : List Line) :
+    List Int :=
+  add3 (flows F e) (C e)
+
+/-- **An entry's statement flows sum to its cash** when what was handled
+for it nets to zero: rule 11 moves no cash (`stmt_flows_sum`). -/
+theorem stmt_flows_sum (F : List Line → Line → Flow) (C : List Line → List Int)
+    (e : List Line) (h : net e = 0) (hC : sum3 (C e) = 0) :
+    sum3 (stmtFlows F C e) = cashOf F e := by
+  have he := entry_flows_sum F e h
+  rw [isum_three _ (flows_length F e)] at he
+  simp only [stmtFlows, add3, sum3_cons]
+  simp only [sum3] at hC
+  omega
+
+theorem getD_neg (xs : List Int) (k : Nat) :
+    (xs.map (fun x => -x)).getD k 0 = -xs.getD k 0 := by
+  induction xs generalizing k with
+  | nil => simp
+  | cons x xs ih => cases k with
+    | zero => simp
+    | succ k => simp only [List.map_cons, List.getD_cons_succ, ih]
+
+/-- **A reversal's statement flows are its original's, negated**, when its
+lines take the original's tags and what was handled for it mirrors
+(`constructive_neg`). -/
+theorem stmt_flows_reversal (F : List Line → Line → Flow) (C : List Line → List Int)
+    (e : List Line) (hF : ∀ l ∈ e, F (reversal e) l.reverse = F e l)
+    (hC : C (reversal e) = (C e).map (fun x => -x)) :
+    stmtFlows F C (reversal e) = (stmtFlows F C e).map (fun x => -x) := by
+  simp only [stmtFlows, add3, flows_reversal F e hF, hC, getD_neg, List.map_cons,
+    List.map_nil, List.cons.injEq, and_true]
+  refine ⟨?_, ?_, ?_⟩ <;> omega
+
+/-- A section's total over some entries: the sum of each entry's cash in
+it (`k` = 0 operating, 1 investing, 2 financing), what a member or lender
+handled for it included. -/
+def sectionTotal (F : List Line → Line → Flow) (C : List Line → List Int) (k : Nat) :
+    List (List Line) → Int
+  | [] => 0
+  | e :: es => (stmtFlows F C e).getD k 0 + sectionTotal F C k es
+
+/-- The entries' cash, summed. -/
+def cashTotal (F : List Line → Line → Flow) : List (List Line) → Int
+  | [] => 0
+  | e :: es => cashOf F e + cashTotal F es
+
+/-- **The sections sum to the change in cash** (plan P3): over any balanced
+entries, operating + investing + financing is the entries' cash, exactly,
+whatever a member or lender handled for them as long as it nets to zero
+within each entry (rule 11, `constructive_nets`). The statement's footing
+(rules.md B-14 rule 9) can't fail on posted entries. -/
+theorem cashflow_sections_sum_to_cash_change (F : List Line → Line → Flow)
+    (C : List Line → List Int) (es : List (List Line)) (h : ∀ e ∈ es, net e = 0)
+    (hC : ∀ e ∈ es, sum3 (C e) = 0) :
+    sectionTotal F C 0 es + sectionTotal F C 1 es + sectionTotal F C 2 es = cashTotal F es := by
+  induction es with
+  | nil => rfl
+  | cons e es ih =>
+    simp only [sectionTotal, cashTotal]
+    have he := stmt_flows_sum F C e (h e (by simp)) (hC e (by simp))
+    simp only [sum3] at he
+    have := ih (fun x hx => h x (by simp [hx])) (fun x hx => hC x (by simp [hx]))
+    omega
+
+/-- When the cash tag follows the account (a line is cash exactly when
+its account is a cash account), an entry's cash is the movement of the
+cash accounts. -/
+theorem secNet_cash_is_movement (f : Line → Flow) (cash : List Nat) (hd : Distinct cash)
+    (hf : ∀ l, f l = .cash ↔ l.account ∈ cash) (ls : List Line) :
+    secNet f .cash ls = sumOver (fun a => movement a ls) cash := by
+  induction ls with
+  | nil => simpa using (sumOver_zero cash).symm
+  | cons l ls ih =>
+    simp only [secNet_cons, movement_cons]
+    rw [sumOver_add, ← ih]
+    by_cases hc : l.account ∈ cash
+    · rw [ite_eq_left ((hf l).2 hc), sumOver_indicator l.account l.signed cash hd hc]
+    · rw [ite_eq_right (fun e => hc ((hf l).1 e)), sumOver_indicator_absent l.account l.signed cash hc]
+
+/-! ### Net income reconciled to operating cash (rules.md B-14 rule 8) -/
+
+/-- Net movement of the lines on revenue and expense accounts (`pl`)
+tagged `k` (`sel = true`), or on balance-sheet accounts (`sel = false`). -/
+def plNet (pl : Nat → Bool) (sel : Bool) (f : Line → Flow) (k : Flow) : List Line → Int
+  | [] => 0
+  | l :: ls => (if pl l.account = sel ∧ f l = k then l.signed else 0) + plNet pl sel f k ls
+
+/-- Net movement of every revenue and expense line. -/
+def plAll (pl : Nat → Bool) : List Line → Int
+  | [] => 0
+  | l :: ls => (if pl l.account = true then l.signed else 0) + plAll pl ls
+
+/-- Net income: revenue less expenses, `-(net of the P&L lines)`. -/
+def netIncome (pl : Nat → Bool) (e : List Line) : Int := -plAll pl e
+
+/-- G: the P&L lines rule 4 puts in investing (gains and losses). -/
+def gainLoss (pl : Nat → Bool) (F : List Line → Line → Flow) (e : List Line) : Int :=
+  plNet pl true (F e) .investing e
+
+/-- W: minus the movement of the operating balance-sheet lines. -/
+def balanceChange (pl : Nat → Bool) (F : List Line → Line → Flow) (e : List Line) : Int :=
+  -plNet pl false (F e) .operating e
+
+/-- X: what no cash, real or handled for the company, settled of the
+operating movement. -/
+def noncashOp (F : List Line → Line → Flow) (C : List Line → List Int) (e : List Line) : Int :=
+  secNet (F e) .operating e + (stmtFlows F C e).getD 0 0
+
+theorem secNet_split (pl : Nat → Bool) (f : Line → Flow) (k : Flow) (ls : List Line) :
+    secNet f k ls = plNet pl true f k ls + plNet pl false f k ls := by
+  induction ls with
+  | nil => rfl
+  | cons l ls ih =>
+    simp only [secNet_cons, plNet, ih]
+    cases pl l.account <;> by_cases h : f l = k <;> simp [h] <;> omega
+
+theorem plAll_split (pl : Nat → Bool) (f : Line → Flow) (ls : List Line)
+    (h : ∀ l ∈ ls, pl l.account = true → f l = .operating ∨ f l = .investing) :
+    plAll pl ls = plNet pl true f .operating ls + plNet pl true f .investing ls := by
+  induction ls with
+  | nil => rfl
+  | cons l ls ih =>
+    simp only [plAll, plNet, ih (fun m hm => h m (by simp [hm]))]
+    cases hp : pl l.account
+    · simp
+    · rcases h l (by simp) hp with hk | hk <;> simp [hk] <;> omega
+
+/-- **Net income reconciles to operating cash**, entry by entry:
+operating cash = NI + G + X + W, when revenue and expense lines are only
+ever operating or investing (rules.md B-14 rule 8; ASC 230-10-45-28 to
+45-30), whatever a member or lender handled for it (rule 11). -/
+theorem operating_reconciliation_ties (pl : Nat → Bool) (F : List Line → Line → Flow)
+    (C : List Line → List Int) (e : List Line)
+    (h : ∀ l ∈ e, pl l.account = true → F e l = .operating ∨ F e l = .investing) :
+    (stmtFlows F C e).getD 0 0
+      = netIncome pl e + gainLoss pl F e + noncashOp F C e + balanceChange pl F e := by
+  have hs := secNet_split pl (F e) .operating e
+  have hp := plAll_split pl (F e) e h
+  simp only [netIncome, gainLoss, noncashOp, balanceChange]
+  omega
+
+/-- The operating section's total over some entries. -/
+def opTotal (pl : Nat → Bool) (F : List Line → Line → Flow) (C : List Line → List Int) :
+    List (List Line) → Int
+  | [] => 0
+  | e :: es => netIncome pl e + gainLoss pl F e + noncashOp F C e + balanceChange pl F e
+      + opTotal pl F C es
+
+/-- **The reconciliation schedule ties to the operating section** over any
+entries: the section's total is NI + G + X + W summed. -/
+theorem operating_reconciliation_ties_all (pl : Nat → Bool) (F : List Line → Line → Flow)
+    (C : List Line → List Int) (es : List (List Line))
+    (h : ∀ e ∈ es, ∀ l ∈ e, pl l.account = true → F e l = .operating ∨ F e l = .investing) :
+    sectionTotal F C 0 es = opTotal pl F C es := by
+  induction es with
+  | nil => rfl
+  | cons e es ih =>
+    simp only [sectionTotal, opTotal]
+    rw [operating_reconciliation_ties pl F C e (h e (by simp)),
+      ih (fun x hx => h x (by simp [hx]))]
+
+end Bookspec