feat(arap)!: documents read their figures from standing lines; control accounts

refuse hand entries (P4b S1, part A)

Plan P4b (D-45), slice S1, the engine half: rules.md B-38.

- ledger-core: every receivables or payables line carries its document
  (Ledger.line_docs: DocRef, Movement, DocTag), written by the document
  commands in the step that posts it, derived on replay from the existing
  document events (the role's account as it stood then; payments by the
  ordinal rule), copied onto a reversal's mirror. Ledger::stands_on;
  doc_state / invoice_state / bill_state (total, paid, outstanding,
  status Open/Partial/Paid/WrittenOff/Void, overdue days) as of any day;
  ar_aging / ap_aging read them, so reversed payments and voids are right.
  The control guard (add_line, add_line_fx, post_entry,
  register_recurring) refuses untagged lines on receivables/payables,
  exempting a reversal's mirror of a legacy line; replay never refuses.
  Bounds (kernel::running_bounds, bounds_kept) on payments and reversals;
  a document reversal never dated before its entry; deposit/payer accounts
  must be cash-like and hold no role. New API: receive_payment_with /
  pay_bill_with (PaymentDetails: instrument, reference), void_document /
  check_void_document, control_check, payments_recorded,
  standing_payments, replay_reverse_entry. Invoice.amount_paid/status
  remain only as derived caches for the MCP layer until part B.
  cashflow bill_splits reads payments from the tags.
- ledger-store: journal feature document_standing (D-39 gated) for a
  payment accepted only because an earlier one was reversed;
  receive_payment_with / pay_bill_with (instrument journaled as
  entry.instrument_set, reference in the description), void_document;
  replay uses replay_reverse_entry; schema 15 drops the projection's
  amount_paid/status. Fixture p4-arap-before + golden figures written by
  the version before S1, adjudicated in arap_standing.rs.
- ledger-gui: party card, cash "coming up" and company owed totals read
  doc_state as of today (late from the derived state).
- Lean Documents.lean (control_agrees and friends); Kani
  bounds_check_matches_definition,
bounds_kept_is_the_definition_on_books_in_bounds;
  rules B-38, B-18/B-23 amended; bookspec `older = true` for legacy hand
  lines; tests that hand-post to 1200/2000 post as replay or renumbered.

Review fixes (both reviews of part A):
- control_role_of guards only an account the role is assigned to or one
  holding its documents' lines (a chart's own 1200 Equipment or card at
  2000 is free until a document posts there); payment accounts check
  other roles by holds_role (type-checked). The MCP tests that failed on
  the guard (oracle_mcp, spec_projects) pass unchanged.
- standing_payments leaves out reversals (sorted, deduped); replayed
  tags match the movement's side; payments_recorded counts every payment
  event (tagged or not, Ledger.payment_events) and refuses overflow.
- The record caches settled (paid + discounted + written off) and owed
  (Invoice/Bill.owed, never serialized): a void never reads as paid.
- assign_role: receivables/payables refuse moving onto an account with
  untagged lines (RoleAccountHasHandLines) and, on their control account
  holding a balance, say DocumentRoleHoldsBalance (no hand entry named);
  B-23 reworded. The reversal-mirror exemption only takes a hand line
  off (even chain depth); putting it back is refused.
- DocStatus Overpaid and Unattached; aging leaves out credit balances;
  ControlCheck.attention lists out-of-bounds and unattached documents.
- stands_on counts a chain in order; indexes (doc_index, doc_accounts,
  order_pos, reversed_by) keep the derived figures linear.
- Viewer reads a post-dated document as of its own date; one state per
  row. bounds_kept's side-crossing documented as intended.
- Tests: ten new spec_documents scenarios, stronger proptests, store
  proptest arap_props (live = replay = snapshot at every date, closed
  months), fuzz ops void/payments with details, a GUI post-dated test;
  Lean Step.assign / Step.release with unattached_zero kept; model
  limits stated in docs/testing.md and B-38.
Review fixes (CPA and engineering lenses): only an assigned role's
account or one holding document lines is a control account (a chart's
own 1200 asset stays free); a role can't move onto untagged lines or off
document lines (Lean Step.assign); a void's cache never reads as paid;
no Decimal sum panics; per-document indexes keep figures linear; a
replayed tag matches its side; the feature gate counts payment events;
a payment's reversal is never listed as standing; an overpaid document
has its own status; the viewer keeps post-dated documents.

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

verify/lean/Audit.lean

@@ -89,3 +89,10 @@ open Wanderbooks
 #print axioms Prorate.chargeLast_mono
 #print axioms Prorate.kernel_parts_total
 #print axioms Prorate.kernel_parts_nonneg
+#print axioms Documents.control_agrees
+#print axioms Documents.control_agrees_through
+#print axioms Documents.Step.document_unattached
+#print axioms Documents.Step.reverse_moves
+#print axioms Documents.reverse_twice
+#print axioms Documents.Reachable.unattached_zero
+#print axioms Documents.Reachable.control_is_documents

verify/lean/Wanderbooks.lean

@@ -6,3 +6,4 @@ import Wanderbooks.Ledger
 import Wanderbooks.Apportion
 import Wanderbooks.Parties
 import Wanderbooks.Prorate
+import Wanderbooks.Documents

verify/lean/Wanderbooks/Documents.lean

@@ -0,0 +1,280 @@
+import Wanderbooks.Entry
+
+/-!
+# Documents are the subledgers of their control accounts (rules.md B-38)
+
+Every ledger line may carry the document it belongs to (an invoice or a
+bill: `Ledger.line_docs`, `arap::DocTag`). A document's figures are the
+sum of its tagged lines; a control account's balance is the sum of every
+line on it. Mirrors `Ledger::doc_state` (outstanding), `control_check`,
+the control guard (`check_control_lines`: every line a command posts on a
+control account carries its document) and `reverse_entry` (a mirror line
+copies its original's tag).
+
+The headline, `control_agrees`: for every account and any lines at all,
+the account's balance is the sum over the documents of what each carries
+on it, plus its untagged ("unattached") lines. Both sides sum the same
+lines, so it is an identity, not a reconciliation, and it holds through
+any date, since a date is a filter on the lines. A document is one `Nat`
+here: an injective coding of `DocRef` (invoices and bills in one id
+space), which is all the sums need. Then, over the commands:
+a document step (an invoice, a bill, a payment, or any entry whose
+control lines are tagged) never moves what is unattached; a reversal
+moves each document, and what is unattached, by exactly the opposite of
+the lines it mirrors (B-38 INVARIANT 3); so books built by these steps
+alone have nothing unattached on a control account, ever
+(`Reachable.unattached_zero`).
+-/
+
+namespace Wanderbooks.Documents
+
+open Wanderbooks
+
+/-- A posted line, its day, and the document it carries (`none`: none). -/
+structure TLine where
+  line : Line
+  date : Nat
+  doc : Option Nat
+  deriving DecidableEq
+
+/-- A line's signed amount on account `a` (zero on another account). -/
+def onAcct (a : Nat) (l : TLine) : Int := if l.line.account = a then l.line.signed else 0
+
+/-- Account `a`'s balance over some lines (the general ledger). -/
+def gl (a : Nat) : List TLine → Int
+  | [] => 0
+  | l :: ls => onAcct a l + gl a ls
+
+/-- What document `d`'s lines on account `a` sum to (`doc_lines`). -/
+def docSum (a d : Nat) : List TLine → Int
+  | [] => 0
+  | l :: ls => (if l.doc = some d then onAcct a l else 0) + docSum a d ls
+
+/-- Account `a`'s lines that carry no document. -/
+def unattached (a : Nat) : List TLine → Int
+  | [] => 0
+  | l :: ls => (if l.doc = none then onAcct a l else 0) + unattached a ls
+
+@[simp] theorem gl_nil (a : Nat) : gl a [] = 0 := rfl
+@[simp] theorem docSum_nil (a d : Nat) : docSum a d [] = 0 := rfl
+@[simp] theorem unattached_nil (a : Nat) : unattached a [] = 0 := rfl
+
+theorem gl_append (a : Nat) (xs ys : List TLine) : gl a (xs ++ ys) = gl a xs + gl a ys := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih => simp only [List.cons_append, gl, ih]; omega
+
+theorem docSum_append (a d : Nat) (xs ys : List TLine) :
+    docSum a d (xs ++ ys) = docSum a d xs + docSum a d ys := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih => simp only [List.cons_append, docSum, ih]; omega
+
+theorem unattached_append (a : Nat) (xs ys : List TLine) :
+    unattached a (xs ++ ys) = unattached a xs + unattached a ys := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih => simp only [List.cons_append, unattached, ih]; omega
+
+/-- Every document some lines carry is among `ds`. -/
+def Covers (ds : List Nat) (ls : List TLine) : Prop :=
+  ∀ l ∈ ls, ∀ k, l.doc = some k → k ∈ ds
+
+/-- **The control account agrees with its documents** (B-38 INVARIANT 1):
+for any lines, any account, and any distinct document ids covering the
+lines' tags, the balance is the documents' sum plus what is unattached. -/
+theorem control_agrees (a : Nat) (ds : List Nat) (hd : Distinct ds) :
+    ∀ ls : List TLine, Covers ds ls →
+      gl a ls = sumOver (fun d => docSum a d ls) ds + unattached a ls := by
+  intro ls
+  induction ls with
+  | nil => intro _; simp [sumOver_zero]
+  | cons l ls ih =>
+    intro hc
+    have hc' : Covers ds ls := fun m hm => hc m (List.mem_cons_of_mem _ hm)
+    simp only [gl, docSum, unattached]
+    rw [sumOver_add, ih hc']
+    cases h : l.doc with
+    | none =>
+      simp [sumOver_zero] <;> omega
+    | some k =>
+      have hk : k ∈ ds := hc l (List.mem_cons_self ..) k h
+      have e : sumOver (fun d => if some k = some d then onAcct a l else 0) ds
+          = sumOver (fun d => if k = d then onAcct a l else 0) ds :=
+        sumOver_congr _ _ ds (fun d _ => by simp)
+      simp only [e, sumOver_indicator k (onAcct a l) ds hd hk]
+      simp <;> omega
+
+/-- The lines dated on or before day `D`. -/
+def through (D : Nat) (ls : List TLine) : List TLine := ls.filter (fun l => decide (l.date ≤ D))
+
+theorem Covers.through {ds : List Nat} {ls : List TLine} (h : Covers ds ls) (D : Nat) :
+    Covers ds (through D ls) := fun l hl => h l (List.mem_filter.1 hl).1
+
+/-- **The same through any day**: GL(A, D) = Σ_docs outstanding(d, D) +
+unattached(A, D). -/
+theorem control_agrees_through (a : Nat) (ds : List Nat) (hd : Distinct ds) (ls : List TLine)
+    (hc : Covers ds ls) (D : Nat) :
+    gl a (through D ls) = sumOver (fun d => docSum a d (through D ls)) ds
+      + unattached a (through D ls) :=
+  control_agrees a ds hd _ (hc.through D)
+
+/-! ## The commands -/
+
+/-- A line mirrored by a reversal: its side flipped, its day the
+reversal's, its document kept (`reverse_entry_steps` copies the tag). -/
+def mirror (D : Nat) (l : TLine) : TLine := { l with line := l.line.reverse, date := D }
+
+theorem onAcct_mirror (a D : Nat) (l : TLine) : onAcct a (mirror D l) = -onAcct a l := by
+  unfold onAcct mirror
+  by_cases h : l.line.account = a
+  · simp [Line.reverse, h]
+    have := Line.reverse_signed l.line
+    simp [Line.reverse] at this
+    exact this
+  · simp [Line.reverse, h]
+
+theorem docSum_mirror (a d D : Nat) (ls : List TLine) :
+    docSum a d (ls.map (mirror D)) = -docSum a d ls := by
+  induction ls with
+  | nil => simp
+  | cons l ls ih =>
+    simp only [List.map_cons, docSum, ih, onAcct_mirror]
+    have : (mirror D l).doc = l.doc := rfl
+    rw [this]
+    by_cases h : l.doc = some d <;> simp [h] <;> omega
+
+theorem unattached_mirror (a D : Nat) (ls : List TLine) :
+    unattached a (ls.map (mirror D)) = -unattached a ls := by
+  induction ls with
+  | nil => simp
+  | cons l ls ih =>
+    simp only [List.map_cons, unattached, ih, onAcct_mirror]
+    have : (mirror D l).doc = l.doc := rfl
+    rw [this]
+    by_cases h : l.doc = none <;> simp [h] <;> omega
+
+/-- Every line of `ls` on a control account carries a document: what the
+control guard requires of every entry a command posts. -/
+def Tagged (control : List Nat) (ls : List TLine) : Prop :=
+  ∀ l ∈ ls, l.line.account ∈ control → l.doc ≠ none
+
+/-- The books: the control accounts (the receivables and payables roles)
+and every posted line, in order. -/
+structure Books where
+  control : List Nat
+  lines : List TLine
+
+/-- What the engine allows (S1): a document command, or any entry whose
+control lines are all tagged (`Step.document`); a reversal of posted
+lines, mirror for mirror, each keeping its tag (`Step.reverse`), dated on
+or after them (B-38, "Dating rules"); assigning a document role an
+account all of whose lines are documents' (`Step.assign`:
+`check_assign_role` SCENARIO 6 refuses one holding an untagged line); and
+an account leaving the control accounts once it holds no document's line
+(`Step.release`: an assigned role moved off an account no document posted
+to; an account holding a document's line stays guarded,
+`control_role_of`). -/
+inductive Step : Books → Books → Prop
+  | document (B : Books) (e : List TLine) (h : Tagged B.control e) :
+      Step B { B with lines := B.lines ++ e }
+  | reverse (B : Books) (e : List TLine) (he : ∀ l ∈ e, l ∈ B.lines) (D : Nat) :
+      Step B { B with lines := B.lines ++ e.map (mirror D) }
+  | assign (B : Books) (c : Nat) (h : ∀ l ∈ B.lines, l.line.account = c → l.doc ≠ none) :
+      Step B { B with control := c :: B.control }
+  | release (B : Books) (c : Nat) (h : ∀ l ∈ B.lines, l.line.account = c → l.doc = none) :
+      Step B { B with control := B.control.erase c }
+
+/-- **A document step never moves what is unattached** on a control
+account: no command adds an untagged control line. -/
+theorem Step.document_unattached (B : Books) (e : List TLine) (h : Tagged B.control e)
+    (a : Nat) (ha : a ∈ B.control) : unattached a (B.lines ++ e) = unattached a B.lines := by
+  rw [unattached_append]
+  suffices unattached a e = 0 by omega
+  induction e with
+  | nil => rfl
+  | cons l ls ih =>
+    simp only [unattached]
+    rw [ih (fun m hm => h m (List.mem_cons_of_mem _ hm))]
+    by_cases hn : l.doc = none
+    · have hacc : l.line.account ≠ a := fun e => h l (List.mem_cons_self ..) (e ▸ ha) hn
+      simp [hn, onAcct, hacc]
+    · simp [hn]
+
+/-- **A reversal moves each document by exactly the opposite of its lines
+it mirrors** (B-38 INVARIANT 3), and what is unattached likewise: only
+reversing a legacy hand line changes it. -/
+theorem Step.reverse_moves (B : Books) (e : List TLine) (D a d : Nat) :
+    docSum a d (B.lines ++ e.map (mirror D)) = docSum a d B.lines - docSum a d e
+      ∧ unattached a (B.lines ++ e.map (mirror D)) = unattached a B.lines - unattached a e := by
+  rw [docSum_append, docSum_mirror, unattached_append, unattached_mirror]
+  omega
+
+/-- **Reversing a reversal restores every document** (B-10): the lines,
+mirrored twice, sum as the originals did. -/
+theorem reverse_twice (a d D D' : Nat) (e : List TLine) :
+    docSum a d ((e.map (mirror D)).map (mirror D')) = docSum a d e := by
+  rw [docSum_mirror, docSum_mirror]; omega
+
+/-- States reachable from books with no lines. -/
+inductive Reachable : Books → Prop
+  | empty (control : List Nat) : Reachable ⟨control, []⟩
+  | step {B B' : Books} : Reachable B → Step B B' → Reachable B'
+
+theorem Reachable.tagged {B : Books} (r : Reachable B) : Tagged B.control B.lines := by
+  induction r with
+  | empty => intro l hl; simp at hl
+  | step _ s ih =>
+    cases s with
+    | document e h =>
+      intro l hl hc
+      rcases List.mem_append.1 hl with hl | hl
+      · exact ih l hl hc
+      · exact h l hl hc
+    | reverse e he D =>
+      intro l hl hc
+      rcases List.mem_append.1 hl with hl | hl
+      · exact ih l hl hc
+      · obtain ⟨m, hm, rfl⟩ := List.mem_map.1 hl
+        exact ih m (he m hm) (by simpa [mirror, Line.reverse] using hc)
+    | assign c h =>
+      intro l hl hc
+      rcases List.mem_cons.1 hc with hc | hc
+      · exact h l hl hc
+      · exact ih l hl hc
+    | release c h =>
+      intro l hl hc
+      exact ih l hl (List.mem_of_mem_erase hc)
+
+/-- **Nothing is ever unattached on a control account** in books these
+steps build, through any day, roles assigned and released included:
+every control line is a document's. (Books an earlier version wrote, with
+hand lines, are covered by the identity `control_agrees` alone; an
+account becoming a control account by its first document, holding lines
+from before, is outside the model: `control_check` lists those lines.) -/
+theorem Reachable.unattached_zero {B : Books} (r : Reachable B) (a : Nat) (ha : a ∈ B.control)
+    (D : Nat) : unattached a (through D B.lines) = 0 := by
+  have ht := r.tagged
+  have : ∀ ls : List TLine, (∀ l ∈ ls, l ∈ B.lines) → unattached a ls = 0 := by
+    intro ls
+    induction ls with
+    | nil => intro _; rfl
+    | cons l ls ih =>
+      intro hs
+      simp only [unattached]
+      rw [ih (fun m hm => hs m (List.mem_cons_of_mem _ hm))]
+      by_cases hn : l.doc = none
+      · have hacc : l.line.account ≠ a :=
+          fun e => ht l (hs l (List.mem_cons_self ..)) (e ▸ ha) hn
+        simp [hn, onAcct, hacc]
+      · simp [hn]
+  exact this _ (fun l hl => (List.mem_filter.1 hl).1)
+
+/-- **So the control account is its documents**, exactly, on every day:
+GL(A, D) = Σ_docs outstanding(d, D). -/
+theorem Reachable.control_is_documents {B : Books} (r : Reachable B) (a : Nat)
+    (ha : a ∈ B.control) (ds : List Nat) (hd : Distinct ds) (hc : Covers ds B.lines) (D : Nat) :
+    gl a (through D B.lines) = sumOver (fun d => docSum a d (through D B.lines)) ds := by
+  rw [control_agrees_through a ds hd B.lines hc D, r.unattached_zero a ha D]; omega
+
+end Wanderbooks.Documents