def Newton.pauliX : Matrix (Fin 2) (Fin 2) ℂ

Pauli matrix σ₁ (X matrix)

Equations

• Newton.pauliX = ![![0, 1], ![1, 0]]

def Newton.pauliY : Matrix (Fin 2) (Fin 2) ℂ

Pauli matrix σ₂ (Y matrix)

Equations

• Newton.pauliY = ![![0, -Complex.I], ![Complex.I, 0]]

def Newton.pauliZ : Matrix (Fin 2) (Fin 2) ℂ

Pauli matrix σ₃ (Z matrix)

Equations

• Newton.pauliZ = ![![1, 0], ![0, -1]]

@[simp]

theorem Newton.pauliX_trace : pauliX.trace = 0

@[simp]

theorem Newton.pauliY_trace : pauliY.trace = 0

@[simp]

theorem Newton.pauliZ_trace : pauliZ.trace = 0

theorem Newton.pauliX_hermitian : pauliX.conjTranspose = pauliX

Pauli matrix σ₁ is Hermitian

theorem Newton.pauliZ_hermitian : pauliZ.conjTranspose = pauliZ

Pauli matrix σ₃ is Hermitian

theorem Newton.pauliY_hermitian : pauliY.conjTranspose = pauliY

Pauli matrix σ₂ is Hermitian

noncomputable def Newton.su2Gen1Matrix : Matrix (Fin 2) (Fin 2) ℂ

Matrix representation of su(2) generator T₁ = -i σ₁ / 2

Equations

• Newton.su2Gen1Matrix = (-Complex.I / 2) • Newton.pauliX

noncomputable def Newton.su2Gen2Matrix : Matrix (Fin 2) (Fin 2) ℂ

Matrix representation of su(2) generator T₂ = -i σ₂ / 2

Equations

• Newton.su2Gen2Matrix = (-Complex.I / 2) • Newton.pauliY

noncomputable def Newton.su2Gen3Matrix : Matrix (Fin 2) (Fin 2) ℂ

Matrix representation of su(2) generator T₃ = -i σ₃ / 2

Equations

• Newton.su2Gen3Matrix = (-Complex.I / 2) • Newton.pauliZ

@[simp]

theorem Newton.su2Gen1Matrix_trace : su2Gen1Matrix.trace = 0

Trace of su(2) generator T₁ is zero

@[simp]

theorem Newton.su2Gen2Matrix_trace : su2Gen2Matrix.trace = 0

Trace of su(2) generator T₂ is zero

@[simp]

theorem Newton.su2Gen3Matrix_trace : su2Gen3Matrix.trace = 0

Trace of su(2) generator T₃ is zero

theorem Newton.su2Gen1Matrix_antiHermitian : su2Gen1Matrix.conjTranspose = -su2Gen1Matrix

su(2) generator T₁ is anti-Hermitian

theorem Newton.su2Gen2Matrix_antiHermitian : su2Gen2Matrix.conjTranspose = -su2Gen2Matrix

su(2) generator T₂ is anti-Hermitian

theorem Newton.su2Gen3Matrix_antiHermitian : su2Gen3Matrix.conjTranspose = -su2Gen3Matrix

su(2) generator T₃ is anti-Hermitian

noncomputable def Newton.su2Gen1 : SuNAlgebra 2

Construct su(2) generator T₁ as SuNAlgebra

Equations

• Newton.su2Gen1 = { matrix := Newton.su2Gen1Matrix, trace_zero := Newton.su2Gen1Matrix_trace, anti_hermitian := Newton.su2Gen1Matrix_antiHermitian }

noncomputable def Newton.su2Gen2 : SuNAlgebra 2

Construct su(2) generator T₂ as SuNAlgebra

Equations

• Newton.su2Gen2 = { matrix := Newton.su2Gen2Matrix, trace_zero := Newton.su2Gen2Matrix_trace, anti_hermitian := Newton.su2Gen2Matrix_antiHermitian }

noncomputable def Newton.su2Gen3 : SuNAlgebra 2

Construct su(2) generator T₃ as SuNAlgebra

Equations

• Newton.su2Gen3 = { matrix := Newton.su2Gen3Matrix, trace_zero := Newton.su2Gen3Matrix_trace, anti_hermitian := Newton.su2Gen3Matrix_antiHermitian }

theorem Newton.su2_bracket_12 : ⁅su2Gen1, su2Gen2⁆ = su2Gen3

[T₁, T₂] = T₃

Calculation: [T₁, T₂] = [-iσ₁/2, -iσ₂/2] = (-i/2)² [σ₁, σ₂] = (-1/4)(2i σ₃) = (-i/2) σ₃ = T₃

theorem Newton.su2_bracket_23 : ⁅su2Gen2, su2Gen3⁆ = su2Gen1

[T₂, T₃] = T₁

theorem Newton.su2_bracket_31 : ⁅su2Gen3, su2Gen1⁆ = su2Gen2

[T₃, T₁] = T₂

theorem Newton.su2Gen3_ne_zero : su2Gen3 ≠ 0

su(2) generator T₃ is nonzero

theorem Newton.su2_noncommutative : ⁅su2Gen1, su2Gen2⁆ ≠ 0

Non-commutativity of su(2): [T₁, T₂] ≠ 0

theorem Newton.su2_bracket_21 : ⁅su2Gen2, su2Gen1⁆ = -su2Gen3

[T₂, T₁] = -T₃ (by antisymmetry)

theorem Newton.su2_bracket_32 : ⁅su2Gen3, su2Gen2⁆ = -su2Gen1

[T₃, T₂] = -T₁ (by antisymmetry)

theorem Newton.su2_bracket_13 : ⁅su2Gen1, su2Gen3⁆ = -su2Gen2

[T₁, T₃] = -T₂ (by antisymmetry)

theorem Newton.su2Gen1_ne_zero : su2Gen1 ≠ 0

su2Gen1 is nonzero

theorem Newton.su2Gen2_ne_zero : su2Gen2 ≠ 0

su2Gen2 is nonzero

theorem Newton.su2_adjointSq_21 : ⁅su2Gen2, ⁅su2Gen2, su2Gen1⁆⁆ = -su2Gen1

[T₂, [T₂, T₁]] = [T₂, -T₃] = -[T₂, T₃] = -T₁

theorem Newton.su2_adjointSq_31 : ⁅su2Gen3, ⁅su2Gen3, su2Gen1⁆⁆ = -su2Gen1

[T₃, [T₃, T₁]] = [T₃, T₂] = -T₁

theorem Newton.su2_adjointSq_12 : ⁅su2Gen1, ⁅su2Gen1, su2Gen2⁆⁆ = -su2Gen2

[T₁, [T₁, T₂]] = [T₁, T₃] = -T₂

theorem Newton.su2_adjointSq_32 : ⁅su2Gen3, ⁅su2Gen3, su2Gen2⁆⁆ = -su2Gen2

[T₃, [T₃, T₂]] = [T₃, T₁] = T₂

theorem Newton.su2_adjointSq_13 : ⁅su2Gen1, ⁅su2Gen1, su2Gen3⁆⁆ = -su2Gen3

[T₁, [T₁, T₃]] = [T₁, -T₂] = T₃

theorem Newton.su2_adjointSq_23 : ⁅su2Gen2, ⁅su2Gen2, su2Gen3⁆⁆ = -su2Gen3

[T₂, [T₂, T₃]] = [T₂, T₁] = -T₃

def Newton.gellMann1 : Matrix (Fin 3) (Fin 3) ℂ

Gell-Mann matrix λ₁

Equations

• Newton.gellMann1 = ![![0, 1, 0], ![1, 0, 0], ![0, 0, 0]]

def Newton.gellMann2 : Matrix (Fin 3) (Fin 3) ℂ

Gell-Mann matrix λ₂

Equations

• Newton.gellMann2 = ![![0, -Complex.I, 0], ![Complex.I, 0, 0], ![0, 0, 0]]

def Newton.gellMann3 : Matrix (Fin 3) (Fin 3) ℂ

Gell-Mann matrix λ₃

Equations

• Newton.gellMann3 = ![![1, 0, 0], ![0, -1, 0], ![0, 0, 0]]

def Newton.gellMann4 : Matrix (Fin 3) (Fin 3) ℂ

Gell-Mann matrix λ₄

Equations

• Newton.gellMann4 = ![![0, 0, 1], ![0, 0, 0], ![1, 0, 0]]

def Newton.gellMann5 : Matrix (Fin 3) (Fin 3) ℂ

Gell-Mann matrix λ₅

Equations

• Newton.gellMann5 = ![![0, 0, -Complex.I], ![0, 0, 0], ![Complex.I, 0, 0]]

def Newton.gellMann6 : Matrix (Fin 3) (Fin 3) ℂ

Gell-Mann matrix λ₆

Equations

• Newton.gellMann6 = ![![0, 0, 0], ![0, 0, 1], ![0, 1, 0]]

def Newton.gellMann7 : Matrix (Fin 3) (Fin 3) ℂ

Gell-Mann matrix λ₇

Equations

• Newton.gellMann7 = ![![0, 0, 0], ![0, 0, -Complex.I], ![0, Complex.I, 0]]

def Newton.gellMann8_unnorm : Matrix (Fin 3) (Fin 3) ℂ

Gell-Mann matrix λ₈ (unnormalized)

Equations

• Newton.gellMann8_unnorm = ![![1, 0, 0], ![0, 1, 0], ![0, 0, -2]]

def Newton.su2StructureConstant (a b c : Fin 3) : ℝ

su(2) structure constants: Levi-Civita symbol

Equations

• One or more equations did not get rendered due to their size.

theorem Newton.su2StructureConstant_antisymm (a b c : Fin 3) : su2StructureConstant b a c = -su2StructureConstant a b c

su(2) structure constants are totally antisymmetric

theorem Newton.su2_has_noncommuting_pair : ∃ (A : SuNAlgebra 2) (B : SuNAlgebra 2), ⁅A, B⁆ ≠ 0

For N = 2, su(2) has noncommuting elements

noncomputable def Newton.embedMatrix2 (M : Matrix (Fin 2) (Fin 2) ℂ) (N : ℕ) : Matrix (Fin (N + 2)) (Fin (N + 2)) ℂ

Embed a 2×2 matrix into the upper-left block of an (N+2)×(N+2) matrix

Equations

• Newton.embedMatrix2 M N i j = if hi : ↑i < 2 then if hj : ↑j < 2 then M ⟨↑i, hi⟩ ⟨↑j, hj⟩ else 0 else 0

theorem Newton.embedMatrix2_trace (M : Matrix (Fin 2) (Fin 2) ℂ) (N : ℕ) : (embedMatrix2 M N).trace = M.trace

Trace preservation for embedded matrix

theorem Newton.embedMatrix2_antiHermitian (M : Matrix (Fin 2) (Fin 2) ℂ) (hM : M.conjTranspose = -M) (N : ℕ) : (embedMatrix2 M N).conjTranspose = -embedMatrix2 M N

Anti-Hermitian property preservation for embedded matrix

noncomputable def Newton.embedSu2 (A : SuNAlgebra 2) (N : ℕ) : SuNAlgebra (N + 2)

Embed an su(2) element into su(N+2)

Equations

• Newton.embedSu2 A N = { matrix := Newton.embedMatrix2 A.matrix N, trace_zero := ⋯, anti_hermitian := ⋯ }

theorem Newton.embedSu2_bracket (A B : SuNAlgebra 2) (N : ℕ) : ⁅embedSu2 A N, embedSu2 B N⁆ = embedSu2 ⁅A, B⁆ N

Embedding preserves Lie bracket

theorem Newton.embedSu2_ne_zero (A : SuNAlgebra 2) (hA : A ≠ 0) (N : ℕ) : embedSu2 A N ≠ 0

Embedding preserves nonzero elements

theorem Newton.exists_noncommuting_elements (N : ℕ) (hN : N ≥ 2) : ∃ (A : SuNAlgebra N) (B : SuNAlgebra N), ⁅A, B⁆ ≠ 0

For N ≥ 2, su(N) has noncommuting elements

Proof by embedding su(2) into su(N). For N = 2, directly constructed from Pauli matrices. For N > 2, we use embedding of su(2) into the upper-left 2×2 block.