conservation_from_balance
In a balanced ledger the net flow at any agent vanishes. Number theorists constructing Euler ledgers and physicists deriving conservation from J-symmetry cite this result. The proof rewrites net flow as a sum of flow contributions, establishes that the event multiset equals its image under reciprocal, and invokes the antisymmetry property of flow_contribution to conclude the sum is zero.
claimLet $L$ be a ledger whose events satisfy the balanced-list condition. For any agent $a$, the net flow of $L$ at $a$ equals zero.
background
The module shows that J-symmetry forces double-entry ledger structure. A Ledger consists of a list of RecognitionEvent together with the balanced_list predicate asserting that every event e appears exactly as often as its reciprocal. The flow_contribution function extracts the signed logarithmic increment an event contributes to a given agent's net flow.
proof idea
The proof first equates net_flow to the sum of flow_contribution over the event list by unfolding the foldl definition and using induction on the list. It then switches to a multiset view M of the events. Because balanced_list implies M equals M.map reciprocal (via count equality and injectivity of reciprocal), and because flow_contribution satisfies f(reciprocal e) = -f(e), the sum of f over M equals its own negative and therefore vanishes.
why it matters in Recognition Science
This theorem supplies the conservation law required by the finite Euler ledger construction in ConcreteEulerLedger. It closes the step from J-symmetry to zero net flow in the LedgerForcing module, which itself sits inside the forcing chain that derives double-entry accounting from the Recognition Composition Law. The result touches the open question of extending the argument from finite lists to infinite or continuous ledgers.
scope and limits
- Does not establish conservation for unbalanced ledgers.
- Does not treat ledgers with infinitely many events.
- Does not derive the explicit value of the flow contributions.
- Does not connect the zero net flow to physical conservation laws beyond the ledger model.
Lean usage
theorem finiteEulerLedger_net_flow_zero (σ : ℝ) (hσ : 0 < σ) (support : List Nat.Primes) (agent : ℕ) : LedgerForcing.net_flow (finiteEulerLedger σ hσ support) agent = 0 := by exact LedgerForcing.conservation_from_balance _ (finiteEulerLedger_balanced σ hσ support) agentformal statement (Lean)
168theorem conservation_from_balance (L : Ledger) (_hbal : balanced L) (agent : ℕ) :
169 net_flow L agent = 0 := by
proof body
Tactic-mode proof.
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-- ... 33 more lines elided ...