foldl_add_nonneg
plain-language theorem explainer
The lemma shows that the left-fold of adding information costs over any finite list of recognition events, begun from a non-negative accumulator, remains non-negative. It is invoked directly to establish total information cost non-negativity for ledger states. The argument relies on induction over the list structure, reducing each cons step via the non-negativity of the individual event cost.
Claim. Let $es$ be a finite list of recognition events, each with information cost $J(e) = J(x) $ where $x > 0$ is the event ratio. For any accumulator $a ≥ 0$, the iterated sum $a + ∑_{e ∈ es} J(e) ≥ 0$.
background
RecognitionEvent encodes each physical fact as a positive ratio $x > 0$ in the ledger. Its information cost equals the J-cost $J(x)$, which is non-negative by the core properties of the cost function. The module states that information is the physical ledger: every recognition event contributes a definite J-cost ≥ 0, with equality only at balanced ratio $x = 1$ and infinite cost as $x → 0^+$.
proof idea
Proof by induction on the list es. The nil case reduces by simplification. The cons case applies simp to unfold foldl_cons, then invokes the inductive hypothesis on the tail after updating the accumulator; linarith closes the step using the non-negativity of the head event's cost.
why it matters
The lemma directly supports total_info_cost_nonneg (IC-001.13), which asserts non-negative aggregate cost over any ledger state. This reinforces the module claim that J-cost is always non-negative, consistent with J-uniqueness (T5) and the ledger-as-reality interpretation. It closes a basic accumulation step without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.