ScatteringEntry
plain-language theorem explainer
ScatteringEntry supplies the record type for a single particle state in a scattering ledger, bundling particle type index, momentum, J-cost value, and its non-negativity witness. QFT researchers deriving unitarity from ledger balance in Recognition Science cite this when building initial and final state lists for conservation arguments. The definition is a direct four-field structure with no computational reduction or lemma applications.
Claim. A scattering entry is a tuple $(n, p, c, h)$ where $n$ is a natural number indexing particle type, $p$ is a real momentum, $c$ is the real J-cost of the state, and $h$ is a proof that $c$ is nonnegative.
background
Recognition Science models scattering via ledger entries whose total J-cost is conserved. J-cost is the non-negative real value returned by the cost function on recognition events, defined in upstream results as derivedCost of a multiplicative recognizer comparator or directly as Cost.Jcost of an event state. Momentum is the native real-valued quantity in RS units. The module derives S-matrix unitarity from the requirement that initial and final ledgers have identical summed J-costs.
proof idea
The declaration is a plain structure definition that introduces the four fields particleType, momentum, cost, and cost_nonneg with no proof body, no tactics, and no lemma applications.
why it matters
ScatteringEntry is the atomic datum type used to construct ScatteringLedger and to state the ledger_cost_conserved theorem that total J-cost is preserved. It supplies the concrete representation needed for the module's derivation of S-matrix unitarity from ledger conservation, the target of the planned PRD paper. The structure directly supports the Recognition Science claim that probability conservation follows from balanced J-cost accounting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.