pith. sign in
theorem

conservation_from_balance

proved
show as:

Why this theorem is linked from The entropy of bulk quantum fields and the entanglement wedge of an evaporating black hole unclear

Pith linked this Lean declaration because the review connected a specific passage in the paper to this theorem. The relation tag says how strong that connection is; it is not a generic placeholder.

Turning on a coupling between one boundary and a further external auxiliary system which functions as a heat sink allows a two-sided otherwise-eternal black hole to evaporate on one side.

Relation between the paper passage and the cited Recognition theorem.

module
IndisputableMonolith.Foundation.LedgerForcing
domain
Foundation
line
168 · github
papers citing
35 papers (below)

plain-language theorem explainer

A balanced ledger of recognition events has zero net flow at every agent. Researchers deriving conservation laws from J-symmetry in discrete models cite this result. The proof rewrites net flow as a sum of flow contributions over events, switches to a multiset view invariant under the reciprocal map, and invokes the negation property of flow contributions under reciprocity to force the sum to zero.

Claim. If $L$ is a ledger whose events satisfy the balanced count condition and $a$ is an agent, then the net flow of $L$ at $a$ equals zero.

background

The LedgerForcing module shows that J-symmetry forces double-entry ledger structure. A Ledger consists of a list of RecognitionEvent together with the balanced_list predicate that enforces equal counts for each event and its reciprocal. Net flow at an agent sums the flow_contribution of each event, which adds or subtracts the logarithm of the event ratio according to whether the agent is source or target. The balanced hypothesis asserts that the multiset of events equals its image under the reciprocal automorphism. Upstream results supply the reciprocal definition from CostAlgebra and the add_assoc, add_comm lemmas used to manipulate the summation rewrites.

proof idea

The tactic proof first rewrites the foldl definition of net_flow into an explicit sum of flow_contribution terms via step_eq and two foldl lemmas. It then forms the multiset M of events and proves M equals M.map reciprocal by count equality from balanced_list together with injectivity of reciprocal. The relation flow_contribution_reciprocal supplies f(reciprocal e) = -f(e). The sum of f over M therefore equals its own negative, so the sum vanishes.

why it matters

This theorem supplies the conservation law used by finiteEulerLedger_net_flow_zero to conclude zero net flow for every finite Euler ledger. It realizes the double-entry invariance forced by J-symmetry, linking the Recognition Composition Law to ledger-level conservation. The result closes one step in the forcing chain from J-uniqueness to discrete accounting structure.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.