`amplitude`

definition

show as: view math explainer →

module: IndisputableMonolith.QFT.SMatrixUnitarity
domain: QFT
line: 57 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.QFT.SMatrixUnitarity on GitHub at line 57.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  54  unitary : matrix.conjTranspose * matrix = 1
  55
  56/-- The S-matrix element for transition from state i to state j. -/
  57def amplitude {n : ℕ} (S : SMatrix n) (i j : Fin n) : ℂ := S.matrix i j
  58
  59/-- Transition probability: |S_ij|². -/
  60noncomputable def probability {n : ℕ} (S : SMatrix n) (i j : Fin n) : ℝ :=
  61  ‖amplitude S i j‖^2
  62
  63/-! ## Unitarity and Probability Conservation -/
  64
  65/-- **THEOREM (Unitarity Inverse)**: S is invertible with S⁻¹ = S†.
  66    This is the other direction of unitarity.
  67
  68    For finite-dimensional spaces, S†S = I implies SS† = I.
  69    This is a standard result in linear algebra. -/
  70theorem s_inverse {n : ℕ} (S : SMatrix n) :
  71    S.matrix * S.matrix.conjTranspose = 1 := by
  72  -- Standard linear algebra: for square matrices, left inverse = right inverse
  73  -- Since S†S = I, S† is a left inverse of S, hence also a right inverse
  74  have h := S.unitary  -- S†S = I
  75  -- The key: S†S = I means S is an isometry on finite-dim space
  76  -- Isometries on finite-dim spaces are surjective (unitary), so SS† = I
  77  -- Using Mathlib's Matrix.mul_eq_one_comm for invertible matrices
  78  rwa [Matrix.mul_eq_one_comm] at h
  79
  80/-- **THEOREM (Probability Conservation)**: For any initial state i,
  81    the total probability of ending in any final state is 1.
  82
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.