total_defect_nonneg'
plain-language theorem explainer
Any ledger configuration of positive real entries has non-negative total defect, defined as the sum of per-entry J-costs. Researchers formalizing the constrained minimization update rule cite this to confirm the energy functional is bounded below. The proof is a one-line wrapper invoking the corresponding non-negativity theorem from the InitialCondition module.
Claim. For any natural number $N$ and any configuration $c$ of $N$ positive real entries, the total defect satisfies $0 ≤ ∑_{i} defect(c_i)$, where $defect(x)$ is the individual J-cost of each entry.
background
The Variational Dynamics module defines the ledger update as the argmin of total defect over feasible configurations that preserve total log-ratio. A configuration is a structure holding an array of $N$ positive real ratios. Total defect is the sum of individual defects drawn from LawOfExistence, each of which is non-negative with equality only at unity.
proof idea
The proof is a one-line wrapper that applies the total_defect_nonneg theorem from InitialCondition, which itself uses Finset.sum_nonneg together with per-entry defect_nonneg.
why it matters
This supplies the lower bound required before stating the variational minimization that produces the next ledger state. It closes the basic non-negativity step imported from InitialCondition and aligns with the J-cost minimum at the identity configuration in the forcing chain. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.