merge: P4b S7, bad debts (branch S7, 4b4fecb9)

The fourth of the paused branches: Ledger::write_off and the bad_debts
control role, invoice.written_off with its evidence filed in the same
store call, books.write_off_invoice, the write-off on the timeline and
in Needs attention, Lean writeOff_within_bounds, rules.md B-41 and the
bookspec examples. Twenty-eight files conflicted with the S4.4, S5 and
S6 merges; resolved as plan 8.0.2 says, keeping both sides' appends with
their seams restored, and: the scope table at 125; S7's law numbered 37;
B-41 placed before B-42; the handbook's step 4 and recovery procedures
folded into the one invoices-and-bills section; S7's wire tests in their
own module with the confirm S4.4's contract needs; S7's copy of the
payment steps dropped (S6 replaced them with Ledger::settle) and its
write-off journaled through S6's journal_auto_lines; in the old-books
fixture S7's hand-written write-off moved to a second invoice, since
S6's hand-written payment settles invoice 1 in full.

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

verify/lean/Audit.lean

@@ -99,3 +99,5 @@ open Wanderbooks
 #print axioms Documents.Step.markSent_changes_no_figure
 #print axioms Documents.Reachable.unattached_zero
 #print axioms Documents.Reachable.control_is_documents
+#print axioms Documents.Step.writeOff_unattached
+#print axioms Documents.writeOff_within_bounds

verify/lean/Wanderbooks/Documents.lean

@@ -18,12 +18,17 @@ 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
+a document step (an invoice, a bill, a payment, a write-off, 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`).
+
+A write-off (S7, B-41) is a document step too: its control line carries the
+document and its expense line is off the control accounts. And it never
+takes a document below zero: `writeOff_within_bounds` reads the date-sum
+before and after it.
 -/
 
 namespace Wanderbooks.Documents
@@ -117,6 +122,10 @@ theorem control_agrees (a : Nat) (ds : List Nat) (hd : Distinct ds) :
 /-- 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 through_append (D : Nat) (xs ys : List TLine) :
+    through D (xs ++ ys) = through D xs ++ through D ys := by
+  simp [through, List.filter_append]
+
 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
 
@@ -171,6 +180,30 @@ def Tagged (control : List Nat) (ls : List TLine) : Prop :=
 /-- The books: the control accounts (the receivables and payables roles),
 every posted line in order, and the sends recorded (each on its invoice;
 plan P4b S5). -/
+/-- A tagged list moves nothing that is unattached on a control account:
+no line it adds on one carries no document. -/
+theorem unattached_zero_of_tagged {control : List Nat} {e : List TLine} (h : Tagged control e)
+    {a : Nat} (ha : a ∈ control) : unattached a e = 0 := by
+  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]
+
+/-- The two lines a write-off of `amount` posts on day `D` (plan P4b S7):
+the document's control line credited, tagged with the document (the
+receivable falls), and the same amount of bad-debt expense debited,
+untagged (the deduction). -/
+def writeOffLines (control expense d D : Nat) (amount : Int) : List TLine :=
+  [ { line := { account := control, side := .credit, amount := amount }, date := D, doc := some d },
+    { line := { account := expense, side := .debit, amount := amount }, date := D, 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
@@ -183,8 +216,9 @@ def Books.docs (B : Books) : List Nat :=
 /-- 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`:
+or after them (B-38, "Dating rules"); writing off a bad debt, for at most
+what the document is owed (`Step.writeOff`, S7); 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
@@ -195,6 +229,11 @@ inductive Step : Books → Books → Prop
       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) }
+  | writeOff (B : Books) (control expense d D : Nat) (amount : Int)
+      (hc : control ∈ B.control) (hne : control ≠ expense)
+      (h : Tagged B.control (writeOffLines control expense d D amount))
+      (hb : amount ≤ docSum control d (through D B.lines)) :
+      Step B { B with lines := B.lines ++ writeOffLines control expense d D amount }
   | 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) :
@@ -209,17 +248,16 @@ inductive Step : Books → Books → Prop
 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]
+  rw [unattached_append, unattached_zero_of_tagged h ha]; omega
+
+/-- **A write-off never moves what is unattached**: its control line carries
+the document (a `Step.document` in shape), and its expense line is off the
+control accounts, so no control account gains an untagged line (B-41). -/
+theorem Step.writeOff_unattached (B : Books) (control expense d D : Nat) (amount : Int)
+    (h : Tagged B.control (writeOffLines control expense d D amount)) (a : Nat)
+    (ha : a ∈ B.control) :
+    unattached a (B.lines ++ writeOffLines control expense d D amount) = unattached a B.lines := by
+  rw [unattached_append, unattached_zero_of_tagged h ha]; omega
 
 /-- **A settlement is a document step**: its entry's every control line
 carries its document (a payment or a discount), so the books' rules for
@@ -287,6 +325,11 @@ theorem Reachable.tagged {B : Books} (r : Reachable B) : Tagged B.control B.line
       · 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)
+    | writeOff control expense d D amount hc hne h hb =>
+      intro l hl hc'
+      rcases List.mem_append.1 hl with hl | hl
+      · exact ih l hl hc'
+      · exact h l hl hc'
     | assign c h =>
       intro l hl hc
       rcases List.mem_cons.1 hc with hc | hc
@@ -330,4 +373,25 @@ theorem Reachable.control_is_documents {B : Books} (r : Reachable B) (a : 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
 
+/-! ## Writing off a bad debt (B-41, plan P4b S7) -/
+
+/-- What a write-off of `amount` does to the document's own sum through
+`D`: the control line it posts there is a credit tagged with the document,
+and the expense line carries none and is on another account. -/
+theorem docSum_writeOffLines (control expense d D : Nat) (amount : Int) :
+    docSum control d (through D (writeOffLines control expense d D amount)) = -amount := by
+  simp [writeOffLines, through, docSum, onAcct, Line.signed]
+
+/-- **A write-off of at most what is owed leaves nothing owed below zero**
+(B-41 INVARIANT 1, over the date-sum `docSum … through D`): the credit it
+posts on the control line is the amount, so what the document owes through
+the write-off's day is what it owed less the amount, and that is never
+below zero. Reversing the write-off adds the amount back
+(`reverse_twice`), which is the same-year recovery (D-49). -/
+theorem writeOff_within_bounds (B : Books) (control expense d D : Nat) (amount : Int)
+    (h : amount ≤ docSum control d (through D B.lines)) :
+    0 ≤ docSum control d (through D (B.lines ++ writeOffLines control expense d D amount)) := by
+  rw [through_append, docSum_append, docSum_writeOffLines]
+  omega
+
 end Wanderbooks.Documents