probability_conserved
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not construct an S-matrix from ledger axioms.
- Does not compute numerical values for specific scattering channels.
- Does not address loop corrections or renormalization.
- Does not prove the converse implication without the unitary field.
Lean usage
theorem optical_theorem_from_unitarity {n : ℕ} (S : SMatrix n) (i : Fin n) : (Finset.univ.sum fun j => probability S i j) = 1 := probability_conserved S iformal statement (Lean)
86theorem probability_conserved {n : ℕ} (S : SMatrix n) (i : Fin n) :
87 (Finset.univ.sum fun j => probability S i j) = 1 := by
proof body
Tactic-mode proof.
88 unfold probability amplitude
89 -- From s_inverse: SS† = I, so (SS†)_ii = Σ_j |S_ij|² = 1
90 have h := s_inverse S
91 have h_diag : (S.matrix * S.matrix.conjTranspose) i i = 1 := by
92 simp only [h, Matrix.one_apply_eq]
93 simp only [Matrix.mul_apply, Matrix.conjTranspose_apply] at h_diag
94 -- h_diag: Σ_j S_ij * star(S_ij) = 1 (as ℂ)
95 -- For z ∈ ℂ: z * star z = Complex.normSq z = ‖z‖² (real)
96 have h_eq : ∀ j, S.matrix i j * star (S.matrix i j) = ↑(‖S.matrix i j‖^2) := fun j => by
97 rw [mul_comm, Complex.star_def, Complex.mul_conj]
98 simp only [Complex.ofReal_pow, Complex.normSq_eq_norm_sq]
99 have h_sum_eq : (Finset.univ.sum fun j => S.matrix i j * star (S.matrix i j)) =
100 (Finset.univ.sum fun j => (↑(‖S.matrix i j‖^2) : ℂ)) := by
101 apply Finset.sum_congr rfl
102 intro j _
103 exact h_eq j
104 rw [h_sum_eq] at h_diag
105 -- Now h_diag : Σ_j ↑(‖S_ij‖²) = (1 : ℂ)
106 have h_sum : (↑(Finset.univ.sum fun j => ‖S.matrix i j‖^2) : ℂ) = 1 := by
107 rw [← h_diag]
108 simp only [Complex.ofReal_sum]
109 exact Complex.ofReal_injective h_sum
110
111/-! ## Ledger Model of Scattering -/
112
113/-- A ledger entry representing a particle state. -/