ScatteringLedger
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not encode the scattering dynamics or interaction Hamiltonian.
- Does not introduce amplitudes, phases, or the S-matrix operator itself.
- Does not enforce probability normalization beyond total cost equality.
- Does not treat continuous spectra or infinite-particle states.
Lean usage
theorem ledger_cost_conserved (L : ScatteringLedger) : (L.initial.map ScatteringEntry.cost).sum = (L.final.map ScatteringEntry.cost).sum := L.cost_conservedformal statement (Lean)
125structure ScatteringLedger where
126 /-- Initial state entries. -/
127 initial : List ScatteringEntry
128 /-- Final state entries. -/
129 final : List ScatteringEntry
130 /-- Total cost is conserved. -/
131 cost_conserved : (initial.map ScatteringEntry.cost).sum =
132 (final.map ScatteringEntry.cost).sum
133
134/-- **THEOREM (Ledger Conservation)**: The total J-cost is preserved in scattering. -/