probability_conserved
plain-language theorem explainer
probability_conserved establishes that for any finite-dimensional S-matrix S and initial index i the sum of transition probabilities over all final states equals one. A QFT researcher normalizing scattering amplitudes or deriving the optical theorem would cite it to confirm row-stochasticity of |S_ij|². The tactic proof reduces the sum directly to the ii diagonal of the unitarity relation SS† = I, then converts the complex terms to real squared norms via mul_conj and ofReal_injective.
Claim. For any natural number $n$, any $n$-dimensional S-matrix $S$ (a complex matrix obeying $S S^† = I$), and any initial index $i$, the sum over final indices $j$ of the squared modulus $|S_{ij}|^2$ equals 1.
background
In this module the S-matrix is introduced as a structure whose matrix field is an $n$-by-$n$ complex matrix equipped with the field unitary asserting that its conjugate transpose times itself equals the identity matrix. Probability for the transition from state $i$ to state $j$ is defined by unfolding to the squared modulus of the corresponding matrix element, matching the Born-rule definition probability in QuantumLedger. The surrounding QFT-012 setting derives S-matrix unitarity from Recognition Science ledger conservation, where the balanced double-entry ledger forces total J-cost preservation and thereby probability normalization.
proof idea
The proof begins by unfolding probability and amplitude to expose the sum as the ii diagonal entry of S times S.conjTranspose. It invokes s_inverse S to replace that product by the identity matrix, extracts the diagonal via one_apply_eq, then rewrites the entry as a sum of S_ij * star(S_ij). Each term is converted to the real value ‖S_ij‖² by Complex.mul_conj and normSq_eq_norm_sq; Finset.sum_congr lifts the equality to the full sum. The final step rewrites the complex sum as the image under ofReal of the real sum and applies Complex.ofReal_injective.
why it matters
The result is invoked directly by unitarity_means_probability_conserved and optical_theorem_from_unitarity inside the same module, and supplies the concrete link in ledgerUnitarityConnection that equates ledger cost balance with probability normalization and S†S = I. It fills the central step of the PRD paper proposition that unitarity follows from ledger structure in Recognition Science. The derivation touches the open mapping from discrete ledger events to continuous scattering amplitudes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.