pith. machine review for the scientific record. sign in
def definition def or abbrev high

ledgerUnitarityConnection

show as:
view Lean formalization →

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.

claimLedger 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 143def ledgerUnitarityConnection : String :=

proof body

Definition body.

 144  "Ledger cost balance ⟺ Probability normalization ⟺ S†S = I"
 145
 146/-- **THEOREM**: Probability conservation is equivalent to unitarity.
 147    We showed probability_conserved follows from S†S = I. -/

depends on (9)

Lean names referenced from this declaration's body.