finiteEulerLedger_balanced
plain-language theorem explainer
Every finite Euler ledger built from a positive real exponent and a list of primes satisfies the balanced predicate in the LedgerForcing sense. Researchers mapping prime zeta data to explicit ledger objects in Recognition Science cite this when establishing conservation before sensor indexing or net-flow arguments. The proof is a direct one-line application of the generic ledger_balanced theorem to the finite construction.
Claim. For any real number $σ > 0$ and any finite list of primes, the ledger formed by adding events with ratios $p^{-σ}$ and their reciprocals for each prime $p$ is balanced.
background
The Concrete Euler Ledger module supplies the first arithmetic-to-ledger bridge. The finiteEulerLedger definition recursively constructs a LedgerForcing.Ledger by starting from the empty ledger and successively adding primeEulerEvent objects, each carrying a ratio $p^{-σ}$ together with its reciprocal so that double-entry is preserved at every step. A ledger is balanced precisely when its event list satisfies the balanced_list predicate, which encodes zero net flow at every agent. The upstream ledger_balanced theorem asserts that every Ledger satisfies this property by construction through its double_entry field.
proof idea
The proof is a one-line wrapper that applies the ledger_balanced theorem directly to the finiteEulerLedger σ hσ support term.
why it matters
This result supplies the balance property required by the downstream finiteEulerLedger_net_flow_zero theorem and by sensorEulerLedger_balanced. It realizes the module's stated goal of producing a concrete, balanced arithmetic ledger from Euler terms, complete with an explicit total cost formula in terms of J(p^{-σ}), while remaining short of the full RSPhysicalThesis. The construction sits inside the broader Recognition Science program of deriving ledger objects from arithmetic data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.