empty_state_zero_cost
plain-language theorem explainer
The empty ledger state carries zero total information cost. Researchers formalizing Wheeler's it-from-bit principle within Recognition Science would cite this base case. The proof is a one-line wrapper that unfolds the foldl definition of total cost and simplifies the empty-event case directly to zero.
Claim. Let $s$ be the ledger state with empty event list. Then the total information cost satisfies $s.events.foldl (fun acc e => acc + infoCost e) 0 = 0$.
background
The InformationIsLedger module identifies information with the physical ledger of recognition events, where each event is a ratio $x > 0$ carrying J-cost. The total information cost of a ledger state is the sum of individual infoCost values over its events, obtained by foldl starting from zero. This theorem supplies the zero base case. Upstream, the from theorem in PrimitiveDistinction derives the structural conditions on distinctions that generate such events, while the totalInfoCost definition itself is the direct summation operator used throughout the module.
proof idea
The proof is a one-line wrapper. It unfolds totalInfoCost to expose the foldl over the empty list, then applies simp to reduce the addition starting from zero to the identity value 0.
why it matters
This is theorem IC-001.14 in the Information IS the Ledger claim, confirming that no recognition events implies zero information cost and therefore perfect balance. It anchors the zero point of the J-cost function (J(x) = 0 iff x = 1) that appears in the module's core list of results and supports the RS interpretation that the ledger is reality. The result is consistent with T5 J-uniqueness and the forced existence of nonzero cost for any deviation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.