ledgerJlogCost_nonneg
plain-language theorem explainer
The nonnegativity of the J-log cost for any transition between ledger states in d dimensions follows from the nonnegativity of Jlog on each coordinate delta. Researchers modeling variational dynamics or ledger-based energy bounds in Recognition Science cite it to guarantee that posting operations never produce negative cost. The argument splits the total cost into independent debit and credit sums, applies the sum nonnegativity lemma to each, and adds the resulting inequalities.
Claim. For any natural number $d$ and ledger states $L,L'$, the J-log cost of the transition satisfies $0 ≤ ∑_{i∈Fin d} J_{log}((L'_i^{debit}-L_i^{debit})) + ∑_{i∈Fin d} J_{log}((L'_i^{credit}-L_i^{credit}))$, where $J_{log}(t) := J_{cost}(e^t)$ and $J_{cost}(x) = (x + x^{-1})/2 - 1$.
background
The module treats ledger updates as single-unit postings to one account, either debit or credit. LedgerState d is the type Recognition.Ledger (AccountRS d), consisting of a pair of integer vectors (debit, credit) indexed by d accounts. Jlog is defined as Jcost composed with the exponential, so Jlog(t) = ((e^t + e^{-t})/2) - 1, which equals cosh(t) - 1 and is nonnegative for all real t by the upstream lemma Jlog_nonneg.
proof idea
The term proof first invokes classical, then uses Finset.sum_nonneg twice (once on the debit deltas and once on the credit deltas) with the fact Jlog_nonneg. It performs a single dsimp to expose the definition of ledgerJlogCost as the sum of those two sums, and finishes with add_nonneg.
why it matters
This nonnegativity is a foundational property for any cost functional built on ledger postings in the Recognition framework. It ensures the J-cost remains a valid nonnegative quantity under the posting operations that induce one-bit parity changes. The result sits downstream of the Jlog definition and Jlog_nonneg lemma and supports later constructions of variational dynamics on ledger states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.