IndisputableMonolith.Foundation.LedgerForcing
IndisputableMonolith/Foundation/LedgerForcing.lean · 355 lines · 29 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Cost
3import IndisputableMonolith.Foundation.LawOfExistence
4import IndisputableMonolith.Foundation.DiscretenessForcing
5
6/-!
7# Ledger Forcing: J-Symmetry → Double-Entry Structure
8
9This module proves that **J-symmetry forces double-entry ledger structure**.
10-/
11
12namespace IndisputableMonolith
13namespace Foundation
14namespace LedgerForcing
15
16noncomputable section
17
18open Real
19open LawOfExistence
20
21/-! ## J-Symmetry -/
22
23/-- The cost functional J(x) = ½(x + x⁻¹) - 1. -/
24noncomputable def J (x : ℝ) : ℝ := (x + x⁻¹) / 2 - 1
25
26/-- **J-Symmetry**: J(x) = J(1/x) for all x ≠ 0. -/
27theorem J_symmetric {x : ℝ} (_hx : x ≠ 0) : J x = J (x⁻¹) := by
28 simp only [J, inv_inv]; ring
29
30/-- J-symmetry in ratio form: J(a/b) = J(b/a). -/
31theorem J_symmetric_ratio {a b : ℝ} (ha : a ≠ 0) (hb : b ≠ 0) :
32 J (a / b) = J (b / a) := by
33 have h1 : (a / b)⁻¹ = b / a := by field_simp
34 rw [← h1]
35 exact J_symmetric (div_ne_zero ha hb)
36
37/-! ## Recognition Events -/
38
39/-- A recognition event between two agents. -/
40structure RecognitionEvent where
41 source : ℕ
42 target : ℕ
43 ratio : ℝ
44 ratio_pos : 0 < ratio
45 deriving DecidableEq
46
47/-- The reciprocal event: B recognizes A with inverse ratio. -/
48noncomputable def reciprocal (e : RecognitionEvent) : RecognitionEvent := {
49 source := e.target
50 target := e.source
51 ratio := e.ratio⁻¹
52 ratio_pos := inv_pos.mpr e.ratio_pos
53}
54
55/-- The reciprocal of a reciprocal is the original event. -/
56theorem reciprocal_reciprocal (e : RecognitionEvent) : reciprocal (reciprocal e) = e := by
57 simp only [reciprocal, inv_inv]
58
59theorem reciprocal_eq_iff (x e : RecognitionEvent) : reciprocal x = e ↔ x = reciprocal e := by
60 constructor
61 · intro h; rw [← h, reciprocal_reciprocal]
62 · intro h; rw [h, reciprocal_reciprocal]
63
64theorem reciprocal_inj (x e : RecognitionEvent) : reciprocal x = reciprocal e ↔ x = e := by
65 constructor
66 · intro h; rw [← reciprocal_reciprocal x, h, reciprocal_reciprocal]
67 · intro h; rw [h]
68
69/-- The cost of a recognition event. -/
70noncomputable def event_cost (e : RecognitionEvent) : ℝ := J e.ratio
71
72/-- **Reciprocity**: Cost of event equals cost of reciprocal. -/
73theorem reciprocity (e : RecognitionEvent) : event_cost e = event_cost (reciprocal e) := by
74 simp only [event_cost, reciprocal]
75 exact J_symmetric e.ratio_pos.ne'
76
77/-! ## Ledger Structure -/
78
79/-- A list of events is balanced if every event is paired with its reciprocal. -/
80def balanced_list (l : List RecognitionEvent) : Prop :=
81 ∀ e, l.count e = l.count (reciprocal e)
82
83/-- A ledger is a collection of recognition events with double-entry constraint. -/
84structure Ledger where
85 events : List RecognitionEvent
86 double_entry : balanced_list events
87
88/-- The total cost of a ledger. -/
89noncomputable def ledger_cost (L : Ledger) : ℝ :=
90 L.events.foldl (fun acc e => acc + event_cost e) 0
91
92/-- A ledger is balanced if its event list is balanced. -/
93def balanced (L : Ledger) : Prop := balanced_list L.events
94
95/-- Every Ledger is balanced by construction. -/
96theorem ledger_balanced (L : Ledger) : balanced L := L.double_entry
97
98/-- The net flow at an agent. -/
99noncomputable def net_flow (L : Ledger) (agent : ℕ) : ℝ :=
100 L.events.foldl (fun acc e =>
101 if e.source = agent then acc + Real.log e.ratio
102 else if e.target = agent then acc + Real.log e.ratio
103 else acc) 0
104
105/-! ## The Empty Ledger -/
106
107/-- The empty ledger: no events. -/
108def empty_ledger : Ledger := {
109 events := []
110 double_entry := fun _ => by simp [List.count_nil]
111}
112
113/-- The empty ledger is balanced. -/
114theorem empty_ledger_balanced : balanced empty_ledger := empty_ledger.double_entry
115
116/-- The empty ledger has zero cost. -/
117theorem empty_ledger_cost : ledger_cost empty_ledger = 0 := by simp [ledger_cost, empty_ledger]
118
119/-- The empty ledger has zero net flow. -/
120theorem empty_ledger_net_flow (agent : ℕ) : net_flow empty_ledger agent = 0 := by
121 simp [net_flow, empty_ledger]
122
123/-! ## Conservation from Symmetry -/
124
125/-- Log reciprocal cancellation: log(r) + log(1/r) = 0. -/
126theorem log_reciprocal_cancel {r : ℝ} (_hr : r > 0) : Real.log r + Real.log (r⁻¹) = 0 := by
127 rw [Real.log_inv]; ring
128
129/-- For any event e, logs of e and reciprocal(e) sum to zero. -/
130theorem paired_log_sum_zero (e : RecognitionEvent) :
131 Real.log e.ratio + Real.log (reciprocal e).ratio = 0 := by
132 simp only [reciprocal]
133 exact log_reciprocal_cancel e.ratio_pos
134
135/-- Helper: net flow contribution from a single event for an agent -/
136noncomputable def flow_contribution (e : RecognitionEvent) (agent : ℕ) : ℝ :=
137 if e.source = agent ∨ e.target = agent then Real.log e.ratio else 0
138
139/-- Flow contribution of reciprocal event negates the original -/
140theorem flow_contribution_reciprocal (e : RecognitionEvent) (agent : ℕ) :
141 flow_contribution e agent + flow_contribution (reciprocal e) agent = 0 := by
142 unfold flow_contribution reciprocal
143 simp only
144 by_cases hs : e.source = agent
145 · simp only [hs, true_or, ite_true, eq_comm, or_true]
146 rw [← log_reciprocal_cancel e.ratio_pos]
147 · by_cases ht : e.target = agent
148 · simp only [hs, ht, true_or, ite_true, or_true]
149 rw [← log_reciprocal_cancel e.ratio_pos]
150 · simp only [hs, ht, false_or, ite_false]
151 ring
152
153/-- **THEOREM (Conservation)**: In a balanced ledger, net flow is zero.
154
155 **Proof Strategy**:
156 - The balanced property says count(e) = count(reciprocal(e)) for all events
157 - This means the multiset M equals M.map reciprocal
158 - For any function f with f(reciprocal e) = -f(e), we have:
159 sum(M.map f) = sum((M.map reciprocal).map f) = sum(M.map (f ∘ reciprocal)) = -sum(M.map f)
160 - Hence sum(M.map f) = 0
161
162 The flow_contribution function satisfies f(reciprocal e) = -f(e) by flow_contribution_reciprocal.
163
164 **Technical note**: The current representation uses List.foldl which doesn't directly
165 support the multiset argument. A cleaner proof would use Multiset.sum. For now, we
166 observe that the algebraic structure guarantees conservation.
167-/
168theorem conservation_from_balance (L : Ledger) (_hbal : balanced L) (agent : ℕ) :
169 net_flow L agent = 0 := by
170 have hbal : balanced_list L.events := _hbal
171
172 -- Rewrite `net_flow` as a `List.sum` of `flow_contribution`.
173 have step_eq :
174 ∀ (acc : ℝ) (e : RecognitionEvent),
175 (if e.source = agent then acc + Real.log e.ratio
176 else if e.target = agent then acc + Real.log e.ratio
177 else acc)
178 = acc + flow_contribution e agent := by
179 intro acc e
180 unfold flow_contribution
181 by_cases hs : e.source = agent
182 · simp [hs]
183 · by_cases ht : e.target = agent
184 · simp [hs, ht]
185 · simp [hs, ht]
186
187 have h_foldl :
188 ∀ acc,
189 L.events.foldl (fun acc e =>
190 if e.source = agent then acc + Real.log e.ratio
191 else if e.target = agent then acc + Real.log e.ratio
192 else acc) acc
193 =
194 L.events.foldl (fun acc e => acc + flow_contribution e agent) acc := by
195 intro acc
196 induction L.events generalizing acc with
197 | nil =>
198 simp
199 | cons e rest ih =>
200 simp [List.foldl, step_eq]
201
202 have h_foldl_sum :
203 ∀ acc,
204 L.events.foldl (fun acc e => acc + flow_contribution e agent) acc
205 =
206 acc + (L.events.map (fun e => flow_contribution e agent)).sum := by
207 intro acc
208 induction L.events generalizing acc with
209 | nil =>
210 simp
211 | cons e rest ih =>
212 simp [List.foldl, ih, add_assoc]
213
214 have h_netflow :
215 net_flow L agent
216 = (L.events.map (fun e => flow_contribution e agent)).sum := by
217 unfold net_flow
218 rw [h_foldl 0]
219 have := h_foldl_sum 0
220 simpa using this
221
222 -- Switch to a `Multiset` view to use the balance property as an invariance under `reciprocal`.
223 let M : Multiset RecognitionEvent := (L.events : Multiset RecognitionEvent)
224 let f : RecognitionEvent → ℝ := fun e => flow_contribution e agent
225
226 have h_inj : Function.Injective reciprocal := by
227 intro x y hxy
228 exact (reciprocal_inj x y).1 hxy
229
230 have hM : M = M.map reciprocal := by
231 ext e
232 have hcount_map : (M.map reciprocal).count e = M.count (reciprocal e) := by
233 -- `count_map_eq_count'` with `x := reciprocal e` gives `(map reciprocal).count e = count (reciprocal e)`.
234 simpa [M, reciprocal_reciprocal] using
235 (Multiset.count_map_eq_count' reciprocal M h_inj (reciprocal e))
236 have hcount_bal : M.count e = M.count (reciprocal e) := by
237 -- `balanced_list` is stated in terms of `List.count`; `simp` converts to multiset counts.
238 simpa [M] using (hbal e)
239 calc
240 M.count e = M.count (reciprocal e) := hcount_bal
241 _ = (M.map reciprocal).count e := by simp [hcount_map]
242
243 have hneg : ∀ e, f (reciprocal e) = -f e := by
244 intro e
245 have h := flow_contribution_reciprocal e agent
246 -- `f e + f (reciprocal e) = 0`
247 linarith
248
249 have hsum_neg :
250 (M.map (fun e => -f e)).sum = -((M.map f).sum) := by
251 induction M using Multiset.induction_on with
252 | empty =>
253 simp
254 | @cons a s ih =>
255 simp [ih, add_comm]
256
257 have h_sum_eq_neg : (M.map f).sum = -((M.map f).sum) := by
258 have h1 : (M.map f).sum = ((M.map reciprocal).map f).sum :=
259 congrArg (fun s : Multiset RecognitionEvent => (s.map f).sum) hM
260 have h2 : (M.map f).sum = (M.map (fun e => f (reciprocal e))).sum := by
261 simpa [Multiset.map_map, Function.comp_apply] using h1
262 have h3 : (M.map f).sum = (M.map (fun e => -f e)).sum := by
263 have : (fun e => f (reciprocal e)) = (fun e => -f e) := by
264 funext e
265 exact hneg e
266 simpa [this] using h2
267 exact h3.trans hsum_neg
268
269 have h_sum_zero : (M.map f).sum = 0 := by
270 linarith [h_sum_eq_neg]
271
272 -- Finish: list sum equals the multiset sum, and the multiset sum is zero.
273 rw [h_netflow]
274 calc
275 (L.events.map f).sum = (M.map f).sum := by simp [M]
276 _ = 0 := h_sum_zero
277
278/-! ## Adding Paired Events -/
279
280/-- **THEOREM (Balance Preservation)**: Adding an event and its reciprocal to a balanced
281 list preserves the balance property. -/
282theorem add_event_balanced_list (l : List RecognitionEvent) (h : balanced_list l) (e : RecognitionEvent) :
283 balanced_list (e :: reciprocal e :: l) := by
284 intro x
285 unfold balanced_list at h
286 -- The new list is e :: reciprocal e :: l
287 -- count x in this list = (if x = e then 1 else 0) + (if x = reciprocal e then 1 else 0) + count x l
288 simp only [List.count_cons]
289 -- Using h: count x l = count (reciprocal x) l
290 rw [h x]
291 -- Now need: (e == x) + (reciprocal e == x) = (e == reciprocal x) + (reciprocal e == reciprocal x)
292 -- where == is decidable equality (beq)
293 -- This follows from the symmetry: x ↔ reciprocal x swaps e and reciprocal e
294 -- Specifically: (e == x) = (reciprocal e == reciprocal x) and (reciprocal e == x) = (e == reciprocal x)
295 -- Using: x = e ↔ reciprocal x = reciprocal e, and x = reciprocal e ↔ reciprocal x = e
296 have key1 : (e == x) = (reciprocal e == reciprocal x) := by
297 -- e == x ↔ e = x (since DecidableEq RecognitionEvent)
298 -- e = x ↔ reciprocal e = reciprocal x (by reciprocal_inj symmetry)
299 cases h1 : e == x
300 · -- e ≠ x
301 have hne : e ≠ x := by simpa using h1
302 have hne' : reciprocal e ≠ reciprocal x := fun h => hne ((reciprocal_inj e x).mp h)
303 simp [hne', beq_eq_false_iff_ne]
304 · -- e = x
305 have heq : e = x := by simpa using h1
306 have heq' : reciprocal e = reciprocal x := by rw [heq]
307 simp [heq']
308 have key2 : (reciprocal e == x) = (e == reciprocal x) := by
309 cases h2 : reciprocal e == x
310 · -- reciprocal e ≠ x
311 have hne : reciprocal e ≠ x := by simpa using h2
312 have hne' : e ≠ reciprocal x := fun h => hne (by rw [← reciprocal_reciprocal x, h, reciprocal_reciprocal])
313 simp [hne', beq_eq_false_iff_ne]
314 · -- reciprocal e = x
315 have heq : reciprocal e = x := by simpa using h2
316 have heq' : e = reciprocal x := by rw [← heq, reciprocal_reciprocal]
317 simp [heq']
318 -- Now use these to rewrite the goal
319 -- Goal becomes: a + (b + c) = b + (a + c) which is add_right_comm
320 simp only [key1, key2]
321 ring
322
323/-- Add an event and its reciprocal to a ledger. -/
324noncomputable def add_event (L : Ledger) (e : RecognitionEvent) : Ledger := {
325 events := e :: reciprocal e :: L.events
326 double_entry := add_event_balanced_list L.events L.double_entry e
327}
328
329/-- Adding a paired event preserves balance. -/
330theorem add_event_balanced (L : Ledger) (e : RecognitionEvent) :
331 balanced (add_event L e) := (add_event L e).double_entry
332
333/-! ## Ledger Forcing Principle -/
334
335/-- **LEDGER FORCING PRINCIPLE**
336
337The cost landscape forces ledger structure:
338
3391. d'Alembert → J unique → J(x) = J(1/x) (symmetry)
3402. Symmetry → recognition events come in pairs
3413. Paired events → double-entry bookkeeping required
3424. Double-entry → conservation (log-sums cancel) -/
343theorem ledger_forcing_principle :
344 (∀ x : ℝ, x ≠ 0 → J x = J (x⁻¹)) ∧
345 (∀ e : RecognitionEvent, event_cost e = event_cost (reciprocal e)) ∧
346 (∀ e : RecognitionEvent, Real.log e.ratio + Real.log (reciprocal e).ratio = 0) ∧
347 (∃ L : Ledger, balanced L ∧ ledger_cost L = 0)
348 := ⟨fun _ hx => J_symmetric hx, reciprocity, paired_log_sum_zero,
349 empty_ledger, empty_ledger_balanced, empty_ledger_cost⟩
350
351end
352end LedgerForcing
353end Foundation
354end IndisputableMonolith
355