finiteEulerLedger_net_flow_zero
plain-language theorem explainer
The theorem shows that any finite Euler ledger built from a positive real exponent σ and a finite list of primes has zero net flow at every agent. Researchers constructing arithmetic-to-ledger bridges in Recognition Science cite it to confirm conservation before moving to sensor-indexed cases. The proof is a one-line wrapper that invokes the generic conservation_from_balance theorem on the pre-proved balanced property of the Euler ledger.
Claim. For any real number σ > 0 and any finite list of primes, let L be the ledger whose events consist of the pairs (p^{-σ}, reciprocal) for each prime p in the list. Then the net flow of L at every agent equals zero.
background
The Concrete Euler Ledger module constructs an explicit LedgerForcing.Ledger from prime data. The definition finiteEulerLedger builds the ledger recursively by adding primeEulerEvent objects, each carrying ratio p^{-σ} together with its reciprocal; this guarantees the balanced property by construction. The net_flow definition sums Real.log(ratio) contributions only from events where the given agent appears as source or target. The upstream conservation_from_balance theorem states that any balanced ledger satisfies net_flow = 0 because the balanced condition equates the multiset of events with its reciprocal image, forcing the signed sum to cancel.
proof idea
The proof is a one-line wrapper that applies conservation_from_balance to the balanced ledger supplied by finiteEulerLedger_balanced.
why it matters
This declaration completes the zero-net-flow step for the finite Euler ledger, supplying the concrete conservation fact required by the downstream sensorEulerLedger_net_flow_zero theorem. It realizes the module's stated bridge object: a real arithmetic ledger with double-entry balance and zero net flow obtained from the generic LedgerForcing conservation theorem. Within the Recognition framework it advances the arithmetic-to-ledger identification without yet reaching RSPhysicalThesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.