theorem
proved
probability_conserved
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.QFT.SMatrixUnitarity on GitHub at line 86.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
Model -
of -
A -
of -
probability -
as -
of -
of -
A -
A -
amplitude -
probability -
s_inverse -
SMatrix -
amplitude -
S -
probability
used by
formal source
83 Proof: From SS† = I (s_inverse), (SS†)_ii = Σ_j S_ij × conj(S_ij) = Σ_j |S_ij|² = 1.
84
85 Technical: requires careful handling of Complex.normSq/star/‖·‖² conversions. -/
86theorem probability_conserved {n : ℕ} (S : SMatrix n) (i : Fin n) :
87 (Finset.univ.sum fun j => probability S i j) = 1 := by
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. -/
114structure ScatteringEntry where
115 /-- Particle type (index). -/
116 particleType : ℕ