feat(core): prove the accounting laws (Kani + Lean); fix three engine gaps

The money arithmetic every invariant rests on now lives in one kernel,
ledger-core/src/kernel.rs: signing a line, totals, net, per-account
movements, reversal, normal balances, trial-balance columns, closing
lines, and the rounding plug for member splits. It is generic over a
checked `Amount` trait. The engine runs it on Decimal (validate,
movements, reverse_entry, account_balance, close_period_to, allocate,
trial_balance): there is one copy of the arithmetic, and it is the one
under proof.

Three layers, docs/verification.md maps every law to its proofs:

- Kani (src/proofs.rs): 17 harnesses prove the kernel at i64 for every
  input up to 4 lines over 3 accounts. An entry is accepted exactly
  when it is two or more positive, in-range lines whose debits equal
  credits; accepted entries net to zero; grouping by account loses
  nothing; a reversal mirrors and cancels its original; trial-balance
  columns balance iff the books net to zero; closing lines zero their
  accounts and a close balances however the net is split; the plug
  makes parts sum to the whole. No panics, no overflow. kani::cover!
  shows the proofs are not vacuous.
- Lean 4 (verify/lean): 24 headline theorems for books of any size. The
  ledger is a state machine (add account, draft, post, reverse, open,
  close), and in every reachable state the books net to zero, the trial
  balance balances (as of any date), and the accounting equation holds.
  Posting only appends ("posted is forever"), closed periods are
  frozen, a close zeroes revenue and expenses and credits exactly the net
  income, and period statements add up. Audit.lean shows standard axioms
  only, no sorry.
- Bridge (tests/kernel_bridge.rs): the Decimal and i64 kernels agree.

What the proofs found (each one missed by every test, fuzzer, and
mutant):

- The engine accepted negative line amounts; only MCP refused them. Now
  NegativeAmountLine: direction is the side's job.
- Summing lines near Decimal::MAX panicked. Lines are now capped at one
  quadrillion and ten decimal places (AmountOutOfRange), which keeps
  every realistic sum exact, and the kernel's sums are checked.
- FX conversion (foreign_amount * fx_rate) could panic the same way; it
  is now a checked multiply.
- Kani itself: 0.68 mis-models symbolic-length copy_from_slice
  (model-checking/kani#4904) and reported a reversal that doesn't net to
  zero. The counterexample, replayed natively, passes, and a 15-line
  standalone crate reproduces the bug. Harnesses avoid bulk copies, and
  a should_panic canary will flag the upstream fix.

`just prove` runs it all (Kani memory- and time-capped, fails on an
unsatisfiable cover or a non-standard Lean axiom). AGENTS.md now makes
formal coverage part of every core change.

Also, docs: GnuCash is *an* oracle, never *the* oracle (Stephen). The
spec is accounting principles, proved. Golden files are recomputed from
principles. External implementations (GnuCash, the old Sheet, QBO/Xero)
are cross-checks whose disagreements get adjudicated, never obeyed.
docs/oracle.md gains "Who is right"; AGENTS, README, architecture,
roadmap, parity, and STATUS are reworded to match.

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

verify/lean/.gitignore

@@ -0,0 +1 @@
+.lake/

verify/lean/Audit.lean

@@ -0,0 +1,32 @@
+import Wanderbooks
+
+/-! `just prove` runs this file: each headline theorem's axioms are printed,
+and must be only Lean's standard three (`propext`, `Quot.sound`,
+`Classical.choice`) or fewer. No `sorryAx`, nothing assumed. -/
+
+open Wanderbooks
+
+#print axioms Accepted.net_zero
+#print axioms sum_movements
+#print axioms movement_with_reversal
+#print axioms accepted_reversal_iff
+#print axioms accounting_equation
+#print axioms balance_after_line
+#print axioms trial_balance_iff
+#print axioms closingEntry_net
+#print axioms closingEntry_zeroes
+#print axioms closingEntry_accepted
+#print axioms net_closings_is_net_income
+#print axioms plugLast_total
+#print axioms plugLast_keeps
+#print axioms Reachable.inv
+#print axioms Reachable.books_net_zero
+#print axioms Reachable.trial_balance
+#print axioms Reachable.trial_balance_through
+#print axioms Reachable.accounting_equation
+#print axioms Reachable.accounting_equation_through
+#print axioms Steps.extends
+#print axioms Steps.frozen
+#print axioms close_zeroes
+#print axioms close_credits_net_income
+#print axioms statements_add_up

verify/lean/Wanderbooks.lean

@@ -0,0 +1,5 @@
+import Wanderbooks.Basic
+import Wanderbooks.Entry
+import Wanderbooks.Statements
+import Wanderbooks.Closing
+import Wanderbooks.Ledger

verify/lean/Wanderbooks/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 Wanderbooks
+
+/-- 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 := Wanderbooks.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 Wanderbooks

verify/lean/Wanderbooks/Closing.lean

@@ -0,0 +1,320 @@
+import Wanderbooks.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 Wanderbooks
+
+/-- 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]
+
+end Wanderbooks

verify/lean/Wanderbooks/Entry.lean

@@ -0,0 +1,117 @@
+import Wanderbooks.Basic
+
+/-!
+# Entries: acceptance, movements, reversals
+
+Mirrors `kernel::check_lines`, `kernel::movements`, `kernel::reversal`,
+and `JournalEntry::validate`.
+-/
+
+namespace Wanderbooks
+
+/-- 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 Wanderbooks

verify/lean/Wanderbooks/Ledger.lean

@@ -0,0 +1,446 @@
+import Wanderbooks.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`.
+-/
+
+namespace Wanderbooks
+
+/-- 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. -/
+structure Ledger where
+  chart : Chart
+  posted : List Entry
+  drafts : List Entry
+  periods : List Period
+
+/-- 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 }
+
+/-- 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
+
+/-- **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) :=
+  Wanderbooks.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) :=
+  Wanderbooks.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⟩
+
+/-- 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
+
+end Wanderbooks

verify/lean/Wanderbooks/Statements.lean

@@ -0,0 +1,104 @@
+import Wanderbooks.Entry
+
+/-!
+# Balances and statements
+
+Mirrors `kernel::normal_balance`, `kernel::columns`,
+`Ledger::account_balance`, and `reports::trial_balance`.
+-/
+
+namespace Wanderbooks
+
+/-- 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
+
+end Wanderbooks

verify/lean/lake-manifest.json

@@ -0,0 +1,6 @@
+{"version": "1.3.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "wanderbooks",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

verify/lean/lakefile.toml

@@ -0,0 +1,5 @@
+name = "wanderbooks"
+defaultTargets = ["Wanderbooks"]
+
+[[lean_lib]]
+name = "Wanderbooks"

verify/lean/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.34.1