ledgerUnitarityConnection
plain-language theorem explainer
Ledger cost balance is defined as equivalent to probability normalization and to S†S = I. Researchers deriving QFT scattering amplitudes from Recognition Science ledger rules would cite this link. The declaration is introduced as a direct string assertion of the three-way equivalence.
Claim. Ledger cost balance is equivalent to probability normalization, which is equivalent to $S^†S = I$.
background
The module QFT.SMatrixUnitarity derives S-matrix unitarity from Recognition Science ledger conservation. The S-matrix maps initial to final states, with unitarity encoding probability conservation and information preservation. Ledger conservation means every credit has a matching debit so total J-cost is preserved across scattering events. Upstream, cost is the J-cost of a recognition event (ObserverForcing.cost) and the derived cost of a multiplicative recognizer comparator (MultiplicativeRecognizerL4.cost).
proof idea
This is a definitional abbreviation that directly asserts the equivalence string without lemmas or tactics.
why it matters
The definition supplies the core insight for the QFT-012 paper proposition that ledger double-entry structure forces S-matrix unitarity. It sits inside the Recognition Science framework where conservation follows from the balanced ledger and connects to probability_conserved in the same module. No downstream theorems yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.