P3: party totals by what moved the money, once (defects 14, 11, 24)

Each party's part of an entry is signed as its own account would show it,
with a direction and its cash and in-kind amounts; a reversal is its
original negated. Totals on a cash or all basis: for a member, all equals
the members' equity statement and cash the K-1's cash. Money is cash,
cards and the financing accounts, and a liability credit never pays its
own creditor (creditor_of), so accruals and declared distributions count
once. tin_last4 from the TIN or W-9 facts.

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

verify/lean/Audit.lean

@@ -67,3 +67,7 @@ open Wanderbooks
 #print axioms cashflow_reversal_nets
 #print axioms Reachable.cashflow_foots
 #print axioms Reachable.cashflow_is_change_in_cash
+#print axioms reverseTarget_involutive
+#print axioms capitalTarget_odd
+#print axioms partyTarget_odd
+#print axioms sumOver_movement_reversal

verify/lean/Wanderbooks.lean

@@ -4,3 +4,4 @@ import Wanderbooks.Statements
 import Wanderbooks.Closing
 import Wanderbooks.Ledger
 import Wanderbooks.Apportion
+import Wanderbooks.Parties

verify/lean/Wanderbooks/Parties.lean

@@ -0,0 +1,215 @@
+import Wanderbooks.Entry
+
+/-!
+# A party's part of an entry (rules.md B-35)
+
+Mirrors `kernel::party_target` and `kernel::reverse_target`, and proves
+what makes a reversal the exact opposite of what it reverses: the target
+is odd (but for the debits fallback, where a sign means nothing, and a
+member's entry whose cash isn't its money: an expense booked straight to
+capital, a debt converted, a distribution still owed), reversing a target
+twice gives it back, and a reversal's movement over any set of accounts
+(a member's equity, say) is the original's negated.
+-/
+
+namespace Wanderbooks
+
+/-- Which way an entry moved value with its parties (`kernel::Direction`). -/
+inductive Direction where
+  | paid
+  | received
+  | neither
+  deriving DecidableEq, Repr
+
+/-- Paid and received swap; neither stays neither. -/
+def Direction.flip : Direction → Direction
+  | .paid => .received
+  | .received => .paid
+  | .neither => .neither
+
+@[simp] theorem Direction.flip_flip (d : Direction) : d.flip.flip = d := by
+  cases d <;> rfl
+
+/-- The direction of a signed amount (`Direction::of`). -/
+def Direction.of (a : Int) : Direction :=
+  if 0 < a then .paid else if a < 0 then .received else .neither
+
+theorem Direction.of_neg (a : Int) : Direction.of (-a) = (Direction.of a).flip := by
+  unfold Direction.of
+  by_cases h1 : 0 < a
+  · rw [ite_eq_right (show ¬ (0 < -a) by omega), ite_eq_left (show -a < 0 by omega), ite_eq_left h1]; rfl
+  · by_cases h2 : a < 0
+    · rw [ite_eq_left (show 0 < -a by omega), ite_eq_right h1, ite_eq_left h2]; rfl
+    · rw [ite_eq_right (show ¬ (0 < -a) by omega), ite_eq_right (show ¬ (-a < 0) by omega), ite_eq_right h1,
+        ite_eq_right h2]; rfl
+
+/-- `kernel::PartyTarget`. -/
+structure PartyTarget where
+  amount : Int
+  direction : Direction
+  cash : Int
+  inKind : Int
+  deriving DecidableEq, Repr
+
+/-- `kernel::reverse_target`: every amount negated, paid and received
+swapped. -/
+def reverseTarget (t : PartyTarget) : PartyTarget :=
+  ⟨-t.amount, t.direction.flip, -t.cash, -t.inKind⟩
+
+/-- **Reversing a reversal gives the original back** (B-9). -/
+theorem reverseTarget_involutive (t : PartyTarget) :
+    reverseTarget (reverseTarget t) = t := by
+  cases t; simp [reverseTarget]
+
+/-- A magnitude. -/
+def magnitude (e : Int) : Int := if e < 0 then -e else e
+
+theorem magnitude_neg (e : Int) : magnitude (-e) = magnitude e := by
+  unfold magnitude
+  by_cases h : e < 0
+  · rw [ite_eq_right (show ¬ (-e < 0) by omega), ite_eq_left h]
+  · by_cases h' : -e < 0
+    · rw [ite_eq_left h', ite_eq_right h]; omega
+    · rw [ite_eq_right h', ite_eq_right h]; omega
+
+/-- The magnitude `m` with the sign of `like`. -/
+def withSign (like m : Int) : Int := if like < 0 then -m else m
+
+theorem withSign_neg (e m : Int) (he : e ≠ 0) : withSign (-e) m = -withSign e m := by
+  unfold withSign
+  by_cases h : e < 0
+  · rw [ite_eq_right (show ¬ (-e < 0) by omega), ite_eq_left h]; omega
+  · rw [ite_eq_left (show -e < 0 by omega), ite_eq_right h]
+
+/-- What of a member's capital movement `e` counts, as (cash, in kind)
+(`kernel::party_target` INVARIANTS 1-2): of a contribution (`e < 0`), the
+property in it, at most `|e|`, in kind and the rest cash; of a
+distribution, the money it paid (`net`, at most `e`) as cash, then the
+property it gave, at most what is left, in kind. The rest of a
+distribution is still owed and counts as nothing. -/
+def capitalParts (e property net : Int) : Int × Int :=
+  if e < 0 then
+    (magnitude e - min (max property 0) (magnitude e), min (max property 0) (magnitude e))
+  else
+    (min (max net 0) (magnitude e),
+      min (max property 0) (magnitude e - min (max net 0) (magnitude e)))
+
+/-- The capital case of `kernel::party_target` (a member's entry moving
+equity `e ≠ 0`), signed as `e`; neither when nothing counts. -/
+def capitalTarget (e property net : Int) : PartyTarget :=
+  ⟨e, if (capitalParts e property net).1 + (capitalParts e property net).2 = 0 then .neither
+    else Direction.of e,
+    withSign e (capitalParts e property net).1, withSign e (capitalParts e property net).2⟩
+
+/-- The rest of `kernel::party_target`: money moved, else the parties'
+own-account movement, else the debits; neither moves nothing. -/
+def moneyTarget (net own debits : Int) : PartyTarget :=
+  if net ≠ 0 then ⟨net, Direction.of net, net, 0⟩
+  else ⟨if own ≠ 0 then own else debits, .neither, 0, 0⟩
+
+/-- `kernel::party_target`. -/
+def partyTarget (capital : Option (Int × Int)) (net own debits : Int) : PartyTarget :=
+  match capital with
+  | some (e, p) => if e ≠ 0 then capitalTarget e p net else moneyTarget net own debits
+  | none => moneyTarget net own debits
+
+/-- A member's entry whose cash is exactly its money: the money moved the
+member's way (paid out on a distribution, received on a contribution) is
+what isn't property. Not so for an expense booked straight to capital, a
+debt converted, or a distribution still owed: the reversal arm, never the
+lines, gives their reversals a target. -/
+def cashIsMoney (e property net : Int) : Prop :=
+  min (max (if 0 < e then net else -net) 0) (magnitude e) =
+    magnitude e - min (max property 0) (magnitude e)
+
+/-- Not vacuous: a cash contribution, a property contribution, and a
+distribution of money and property each have their cash as their money. -/
+example : cashIsMoney (-100) 0 (-100) ∧ cashIsMoney (-100) 100 0 ∧ cashIsMoney 100 40 60 := by
+  unfold cashIsMoney magnitude
+  decide
+
+/-- Negating a member's entry whose cash is its money keeps what counts. -/
+theorem capitalParts_neg (e p net : Int) (he : e ≠ 0) (h : cashIsMoney e p net) :
+    capitalParts (-e) p (-net) = capitalParts e p net := by
+  unfold cashIsMoney at h
+  unfold capitalParts
+  rw [magnitude_neg]
+  by_cases hn : e < 0
+  · rw [ite_eq_right (show ¬ (0 < e) by omega)] at h
+    rw [ite_eq_right (show ¬ (-e < 0) by omega), ite_eq_left hn, h]
+    congr 1
+    omega
+  · rw [ite_eq_left (show 0 < e by omega)] at h
+    rw [ite_eq_left (show -e < 0 by omega), ite_eq_right hn, h]
+    congr 1
+    omega
+
+/-- **A member's capital target is odd** whenever its cash is its money. -/
+theorem capitalTarget_odd (e p net : Int) (he : e ≠ 0) (h : cashIsMoney e p net) :
+    capitalTarget (-e) p (-net) = reverseTarget (capitalTarget e p net) := by
+  unfold capitalTarget reverseTarget
+  rw [capitalParts_neg e p net he h, withSign_neg _ _ he, withSign_neg _ _ he]
+  congr 1
+  by_cases hc : (capitalParts e p net).1 + (capitalParts e p net).2 = 0
+  · simp [hc, Direction.flip]
+  · simp [hc, Direction.of_neg]
+
+/-- With money moved, or the parties' own accounts moved, the rest of the
+target is odd too. -/
+theorem moneyTarget_odd (net own debits : Int) (h : net ≠ 0 ∨ own ≠ 0) :
+    moneyTarget (-net) (-own) debits = reverseTarget (moneyTarget net own debits) := by
+  unfold moneyTarget reverseTarget
+  by_cases hn : net = 0
+  · have ho : own ≠ 0 := by omega
+    have : ¬ (-own = 0) := by omega
+    simp [hn, ho, this, Direction.flip]
+  · have : ¬ (-net = 0) := by omega
+    simp [hn, this, Direction.of_neg]
+
+/-- **The target is odd** (rules.md B-35 item 3, B-9): negating an entry's
+lines negates its capital movement, its money net and its own-account
+movement, while the property beside a capital movement comes from the
+other side of the lines and keeps its size; the result is the original's
+`reverseTarget`, but for the debits fallback (nothing moved: a sign means
+nothing there) and a member's entry whose cash isn't its money. The
+engine's reversal arm, not the lines, gives every reversal its target. -/
+theorem partyTarget_odd (capital : Option (Int × Int)) (net own debits : Int)
+    (h : (∃ e p, capital = some (e, p) ∧ e ≠ 0 ∧ cashIsMoney e p net) ∨
+      ((∀ e p, capital = some (e, p) → e = 0) ∧ (net ≠ 0 ∨ own ≠ 0))) :
+    partyTarget (capital.map fun c => (-c.1, c.2)) (-net) (-own) debits =
+      reverseTarget (partyTarget capital net own debits) := by
+  cases capital with
+  | none =>
+    simp only [Option.map, partyTarget]
+    apply moneyTarget_odd
+    rcases h with ⟨_, _, hc, _⟩ | ⟨_, h⟩
+    · cases hc
+    · exact h
+  | some c =>
+    obtain ⟨e, p⟩ := c
+    simp only [Option.map, partyTarget]
+    by_cases he : e = 0
+    · have : ¬ (-e ≠ 0) := by omega
+      simp only [he, ne_eq, not_true_eq_false, ite_false, Int.neg_zero]
+      apply moneyTarget_odd
+      rcases h with ⟨e', p', hc, he', _⟩ | ⟨_, h⟩
+      · simp at hc; omega
+      · exact h
+    · have : -e ≠ 0 := by omega
+      simp only [ne_eq, he, this, not_false_eq_true, ite_true]
+      rcases h with ⟨e', p', hc, _, hm⟩ | ⟨hz, _⟩
+      · simp only [Option.some.injEq, Prod.mk.injEq] at hc
+        obtain ⟨rfl, rfl⟩ := hc
+        exact capitalTarget_odd e p net he hm
+      · exact absurd (hz e p rfl) he
+
+/-- **A reversal's movement over any accounts is the original's negated**
+(so the equity movement a member's target reads flips with it): summed
+over a set of accounts, `movement_reversal` account by account. -/
+theorem sumOver_movement_reversal (as : List Nat) (ls : List Line) :
+    sumOver (fun a => movement a (reversal ls)) as = -sumOver (fun a => movement a ls) as := by
+  have : (fun a => movement a (reversal ls)) = (fun a => -movement a ls) := by
+    funext a; exact movement_reversal a ls
+  rw [this, sumOver_neg]
+
+end Wanderbooks