total_info_cost_nonneg
plain-language theorem explainer
Total information cost of any ledger state is nonnegative. Researchers modeling information as physical ledger in Recognition Science cite this as IC-001.13 to ground the nonnegativity of summed J-costs. The proof is a term-mode one-liner that unfolds the total cost definition and applies the foldl nonnegativity helper lemma from a zero base.
Claim. Let $s$ be a ledger state consisting of a finite list of recognition events. Then the total information cost of $s$, defined as the sum of the individual J-costs of its events, satisfies total information cost of $s$ is at least zero.
background
In the InformationIsLedger module a ledger state is a finite list of recognition events, each event a positive ratio whose J-cost quantifies its information content. Total information cost is the accumulated sum of these J-costs via foldl. The module establishes that information is the physical ledger, with every recognition event carrying nonnegative J-cost and the balanced state $x=1$ carrying zero cost.
proof idea
The proof is a term-mode one-liner. It unfolds the definition of total information cost and applies the foldl_add_nonneg lemma to the event list, starting from accumulator zero with the base proof le_refl 0.
why it matters
This result is IC-001.13 and is aggregated into the IC-001 status certificate that certifies the full ledger-is-information claim. It supplies the nonnegativity foundation required by the downstream certificate and aligns with the core list of J-cost properties in the module, including symmetry and the infinite cost of nothingness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.