Contraction of indices of Pauli matrix.

The main result of this file is pauliMatrix_contract_pauliMatrix which states that η_{μν} σ^{μ α dot β} σ^{ν α' dot β'} = 2 ε^{αα'} ε^{dot β dot β'}.

The current way this result is proved is by using tensor tree manipulations. There is likely a more direct path to this result.

theorem PauliMatrix.pauliCo_contr_pauliContr : (TensorSpecies.Tensor.contrT 4 0 3 ⋯) ((TensorSpecies.Tensor.prodT (TensorSpecies.Tensorial.toTensor pauliCo)) (TensorSpecies.Tensorial.toTensor (TensorSpecies.Tensorial.toTensor pauliMatrix))) = (TensorSpecies.Tensor.permT ![0, 2, 1, 3] ⋯) (2 • (TensorSpecies.Tensor.prodT (TensorSpecies.Tensorial.toTensor complexLorentzTensor.leftMetric)) (TensorSpecies.Tensorial.toTensor complexLorentzTensor.rightMetric))

The statement that σᵥᵃᵇ σᵛᵃ'ᵇ' = 2 εᵃᵃ' εᵇᵇ'.

theorem PauliMatrix.pauliCoDown_trace_pauliCo : (TensorSpecies.Tensor.contrT 2 1 3 ⋯) ((TensorSpecies.Tensor.contrT 4 2 4 ⋯) ((TensorSpecies.Tensor.prodT (TensorSpecies.Tensorial.toTensor pauliCoDown)) (TensorSpecies.Tensorial.toTensor pauliCo))) = (TensorSpecies.Tensor.permT ![0, 1] ⋯) (2 • TensorSpecies.Tensorial.toTensor complexLorentzTensor.coMetric)

theorem PauliMatrix.pauliCo_trace_pauliCoDown : (TensorSpecies.Tensor.contrT 2 1 3 ⋯) ((TensorSpecies.Tensor.contrT 4 2 4 ⋯) ((TensorSpecies.Tensor.prodT (TensorSpecies.Tensorial.toTensor pauliCo)) (TensorSpecies.Tensorial.toTensor pauliCoDown))) = (TensorSpecies.Tensor.permT ![0, 1] ⋯) (2 • TensorSpecies.Tensorial.toTensor complexLorentzTensor.coMetric)

theorem PauliMatrix.pauliContr_mul_pauliContrDown_add : (TensorSpecies.Tensor.contrT 4 2 4 ⋯) ((TensorSpecies.Tensor.prodT (TensorSpecies.Tensorial.toTensor (TensorSpecies.Tensorial.toTensor pauliMatrix))) (TensorSpecies.Tensorial.toTensor pauliContrDown)) + (TensorSpecies.Tensor.permT ![2, 1, 0, 3] ⋯) ((TensorSpecies.Tensor.contrT 4 2 4 ⋯) ((TensorSpecies.Tensor.prodT (TensorSpecies.Tensorial.toTensor (TensorSpecies.Tensorial.toTensor pauliMatrix))) (TensorSpecies.Tensorial.toTensor pauliContrDown))) = (TensorSpecies.Tensor.permT ![0, 2, 1, 3] ⋯) (2 • (TensorSpecies.Tensor.prodT (TensorSpecies.Tensorial.toTensor complexLorentzTensor.contrMetric)) (TensorSpecies.Tensorial.toTensor complexLorentzTensor.leftAltLeftUnit))

theorem PauliMatrix.auliContrDown_pauliContr_mul_add : (TensorSpecies.Tensor.contrT 4 2 4 ⋯) ((TensorSpecies.Tensor.prodT (TensorSpecies.Tensorial.toTensor pauliContrDown)) (TensorSpecies.Tensorial.toTensor (TensorSpecies.Tensorial.toTensor pauliMatrix))) + (TensorSpecies.Tensor.permT ![2, 1, 0, 3] ⋯) ((TensorSpecies.Tensor.contrT 4 2 4 ⋯) ((TensorSpecies.Tensor.prodT (TensorSpecies.Tensorial.toTensor pauliContrDown)) (TensorSpecies.Tensorial.toTensor (TensorSpecies.Tensorial.toTensor pauliMatrix)))) = (TensorSpecies.Tensor.permT ![0, 2, 1, 3] ⋯) (2 • (TensorSpecies.Tensor.prodT (TensorSpecies.Tensorial.toTensor complexLorentzTensor.contrMetric)) (TensorSpecies.Tensorial.toTensor complexLorentzTensor.altRightRightUnit))