ScatteringLedger
plain-language theorem explainer
ScatteringLedger packages an initial list of particle states and a final list together with the requirement that their summed J-costs are identical. Researchers deriving S-matrix unitarity from Recognition Science ledger balance cite this record when showing that cost conservation implies probability conservation. The definition is a direct structure whose only non-data field is the conservation equality itself.
Claim. A scattering ledger consists of lists $I$ and $F$ of scattering entries together with the equality $C$ asserting that the sum of J-costs over $I$ equals the sum of J-costs over $F$. Each entry carries a particle type index, a real momentum, and a non-negative J-cost.
background
The module QFT.SMatrixUnitarity derives S-matrix unitarity from Recognition Science ledger conservation. A ScatteringEntry is the basic record holding particleType : ℕ, momentum : ℝ, cost : ℝ, and the proof that cost ≥ 0. The cost field is supplied by upstream definitions: cost in MultiplicativeRecognizerL4 returns the derived cost of a comparator on positive ratios, while cost in ObserverForcing returns the J-cost of a recognition event. The module doc states that the ledger functions as a balanced double-entry system in which every credit has a matching debit, so that total J-cost is conserved and this conservation is identified with S†S = 1.
proof idea
The declaration is a structure definition with no proof body. It simply records the three fields initial, final, and cost_conserved; the conservation statement is asserted directly as a field of the structure rather than derived.
why it matters
ScatteringLedger supplies the central object for the downstream theorem ledger_cost_conserved, which extracts the conservation equality and feeds the argument that ledger balance implies S-matrix unitarity. It realizes the paper proposition on unitarity from ledger structure in the QFT-012 section. The construction sits inside the Recognition Science forcing chain after T5 (J-uniqueness) and T6 (phi fixed point), using the Recognition Composition Law to guarantee that J-cost is additive across scattering events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.