optical_theorem_from_unitarity
plain-language theorem explainer
Probability conservation for transitions in an S-matrix follows from its built-in unitarity in the Recognition Science ledger. A physicist deriving scattering results from ledger balance would cite this to confirm that no probability is lost across all final states for any initial index. The proof is a one-line wrapper applying the probability_conserved lemma.
Claim. For any natural number $n$, any unitary $n$-by-$n$ complex matrix $S$ encoding scattering transitions, and any initial state index $i$, the sum over all final indices $j$ of the transition probability from $i$ to $j$ equals 1.
background
The module derives S-matrix unitarity from Recognition Science ledger conservation, where the S-matrix is a unitary operator on finite-dimensional Hilbert space whose matrix elements give transition amplitudes. Probability of a transition is the squared modulus of the amplitude, taken from the QuantumLedger definition that applies the Born rule to quantum states. This places the result inside the QFT-012 setting: initial ledger entries at early times scatter via recognition events and reappear at late times with total J-cost preserved, forcing the sum of probabilities to one.
proof idea
The proof is a one-line wrapper that applies the probability_conserved lemma directly to the supplied S-matrix and initial index.
why it matters
This result supplies the probability-conservation step that lets the optical theorem follow from ledger symmetry, as noted in the module doc-comment. It sits under the QFT-012 paper proposition that S†S = I arises from balanced double-entry ledger structure rather than being imposed by hand. The declaration closes one link in the chain from T5 J-uniqueness and T6 phi fixed-point through ledger conservation to standard QFT unitarity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.