ledger_cost_conserved
plain-language theorem explainer
Ledger conservation asserts that the total J-cost summed over initial scattering entries equals the sum over final entries for any ScatteringLedger L. Researchers deriving S-matrix unitarity from Recognition Science foundations would reference this to link double-entry bookkeeping to probability preservation. The proof reduces to a single field projection from the ledger structure definition.
Claim. For any scattering ledger $L$, the sum of J-costs over its initial entries equals the sum over its final entries: $((L.initial).map cost).sum = ((L.final).map cost).sum$.
background
ScatteringLedger is a structure with initial and final lists of ScatteringEntry records; each entry carries a non-negative J-cost, and the structure itself records that the two sums are identical. The module QFT.SMatrixUnitarity treats this built-in balance as the source of S-matrix unitarity, identifying conserved total J-cost with probability conservation. Upstream, cost is supplied by ObserverForcing.cost as the J-cost of a recognition event and by MultiplicativeRecognizerL4.cost as the derived cost on positive ratios; probability is defined via norm-squared amplitudes in QuantumLedger.probability.
proof idea
One-line wrapper that applies the cost_conserved field of the ScatteringLedger structure.
why it matters
This supplies the conservation law that equates ledger balance with S-matrix unitarity in the QFT-012 derivation. It fills the module target of obtaining unitarity from RS ledger structure, as stated in the module documentation, and supports sibling results on probability conservation and information preservation. The step sits downstream of cost and forcing definitions in the Foundation and Measurement layers and directly implements the Recognition Science claim that double-entry balance forces S†S = 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.