From 247d029e6dfa022f3d6237a0deea1cff4751e937 Mon Sep 17 00:00:00 2001 From: ZhiKai Pong Date: Sat, 19 Sep 2026 13:32:54 +0100 Subject: [PATCH 1/3] perf(PauliMatrices): cheaper Levi-Civita components in the three-Pauli identities MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The three-Pauli identities (2.26) and (2.27) are proved by `decide +kernel` over all tensor components. The components of `ε4ℂ` were given by `generalizedKroneckerDelta`, a 4x4 determinant, which the kernel evaluated 1024 times per lemma as a sum over permutations with `Equiv.Perm.sign`. - Add `leviCivitaSymbolProd`, the product over pairs `i < j` of the sign of `g j - g i`, and `leviCivitaSymbol_eq_leviCivitaSymbolProd` (any `Fin n`, via `Equiv.Perm.sign_eq_prod_prod_Ioi`). - Add `leviCivita_eq_ofRat_prod` stating the components of `ε4ℂ` with it, and use it in the two identities. - In the two identities rewrite with `I_mul_toComplexNum` only inside the last summand instead of across the whole goal. Identity (2.27) was at the default `maxHeartbeats` limit. Kernel `decide`: 289M -> 73M and 301M -> 78M heartbeats. No statement changed. Co-Authored-By: Claude Fable 5.1 --- Physlib/Mathematics/LeviCivita/Basic.lean | 40 +++++++++++++++++++ .../Relativity/PauliMatrices/Relations.lean | 8 ++-- .../Tensors/LeviCivita/Complex.lean | 11 +++++ 3 files changed, 55 insertions(+), 4 deletions(-) diff --git a/Physlib/Mathematics/LeviCivita/Basic.lean b/Physlib/Mathematics/LeviCivita/Basic.lean index d92afc37cc..e927c6923a 100644 --- a/Physlib/Mathematics/LeviCivita/Basic.lean +++ b/Physlib/Mathematics/LeviCivita/Basic.lean @@ -7,6 +7,7 @@ module public import Physlib.Mathematics.KroneckerDelta.Basic public import Mathlib.LinearAlgebra.Matrix.Permutation +public import Mathlib.GroupTheory.Perm.Fin /-! # The Levi-Civita symbol in general dimension @@ -32,6 +33,9 @@ permutation via `Matrix.det_permutation`. - `leviCivitaSymbol_comp_swap` : antisymmetry under transposition of two indices. - `leviCivitaSymbol_swap_comp` : antisymmetry under transposition of two index values. - `leviCivitaSymbol_eq_zero_iff` : the symbol vanishes exactly on repeated indices. +- `leviCivitaSymbolProd` : the product over pairs `i < j` of the sign of `g j - g i`, for + `g : Fin n → Fin n`. +- `leviCivitaSymbol_eq_leviCivitaSymbolProd` : on `Fin n` the symbol equals this product. ## iii. Table of contents @@ -39,6 +43,7 @@ permutation via `Matrix.det_permutation`. - B. Value on permutations - C. Antisymmetry - D. Vanishing on repeated indices +- E. Closed form on `Fin n` ## iv. References @@ -150,3 +155,38 @@ lemma leviCivitaSymbol_eq_zero_iff {g : ι → ι} : ⟨Equiv.ofBijective g (Finite.injective_iff_bijective.mp hinj), rfl⟩ rw [leviCivitaSymbol_perm] at h exact Units.ne_zero (Equiv.Perm.sign σ) h + +/-! + +## E. Closed form on `Fin n` + +-/ + +/-- The product over pairs `i < j` of the sign of `g j - g i`, for `g : Fin n → Fin n`. +This equals `leviCivitaSymbol g` by `leviCivitaSymbol_eq_leviCivitaSymbolProd` and, unlike +the determinant defining `leviCivitaSymbol`, is cheap to evaluate, e.g. by `decide`. -/ +def leviCivitaSymbolProd {n : ℕ} (g : Fin n → Fin n) : ℤ := + ∏ i, ∏ j ∈ Finset.Ioi i, (if g i < g j then 1 else if g i = g j then 0 else -1) + +/-- On `Fin n` the Levi-Civita symbol is the product over pairs `i < j` of the sign of +`g j - g i`. -/ +lemma leviCivitaSymbol_eq_leviCivitaSymbolProd {n : ℕ} (g : Fin n → Fin n) : + leviCivitaSymbol g = leviCivitaSymbolProd g := by + unfold leviCivitaSymbolProd + by_cases hg : Function.Injective g + · obtain ⟨σ, rfl⟩ : ∃ σ : Equiv.Perm (Fin n), ⇑σ = g := + ⟨Equiv.ofBijective g (Finite.injective_iff_bijective.mp hg), rfl⟩ + rw [leviCivitaSymbol_perm, Equiv.Perm.sign_eq_prod_prod_Ioi] + simp only [Units.coe_prod] + refine Finset.prod_congr rfl fun i _ => Finset.prod_congr rfl fun j hj => ?_ + have hij : σ i ≠ σ j := σ.injective.ne (Finset.mem_Ioi.mp hj).ne + split_ifs <;> simp + · rw [leviCivitaSymbol_eq_zero_of_not_injective hg] + simp only [Function.Injective, not_forall] at hg + obtain ⟨i, j, hgij, hij⟩ := hg + symm + rcases lt_or_gt_of_ne hij with h | h + · exact Finset.prod_eq_zero (Finset.mem_univ i) + (Finset.prod_eq_zero (Finset.mem_Ioi.mpr h) (by simp [hgij])) + · exact Finset.prod_eq_zero (Finset.mem_univ j) + (Finset.prod_eq_zero (Finset.mem_Ioi.mpr h) (by simp [hgij])) diff --git a/Physlib/Relativity/PauliMatrices/Relations.lean b/Physlib/Relativity/PauliMatrices/Relations.lean index fb2f7d47ea..4845a2b5ce 100644 --- a/Physlib/Relativity/PauliMatrices/Relations.lean +++ b/Physlib/Relativity/PauliMatrices/Relations.lean @@ -192,7 +192,7 @@ lemma pauliContr_mul_pauliContrDown_mul_pauliContr : ({ conv_rhs => rw [leviCivita_mul_pauliDual] simp only [contrMetric_eq_ofRat, toTensor_eq_ofRat, prodT_ofRat_ofRat] - simp only [leviCivita_eq_ofRat, pauliCo_eq_ofRat] + simp only [leviCivita_eq_ofRat_prod, pauliCo_eq_ofRat] rw [prodT_ofRat_ofRat, contrT_ofRat, permT_ofRat] apply (Tensor.basis _).repr.injective ext b @@ -200,7 +200,7 @@ lemma pauliContr_mul_pauliContrDown_mul_pauliContr : ({ simp only [map_add, Finsupp.coe_add, Pi.add_apply] simp only [permT_basis_repr_symm_apply, map_neg, Finsupp.coe_neg, Pi.neg_apply, map_smul, Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, ofRat_basis_repr_apply] - rw [Physlib.RatComplexNum.I_mul_toComplexNum] + conv_rhs => arg 2; rw [Physlib.RatComplexNum.I_mul_toComplexNum] apply Physlib.RatComplexNum.toComplexNum_eq_add_neg_add_add_iff.mpr decide +revert +kernel @@ -219,7 +219,7 @@ lemma pauliContrDown_mul_pauliContr_mul_pauliContrDown : ({ prodT_ofRat_ofRat, contrT_ofRat] conv_rhs => simp only [contrMetric_eq_ofRat, toTensor_dualWeyl_eq_ofRat, prodT_ofRat_ofRat] - simp only [leviCivita_eq_ofRat, toTensor_dualAll_eq_ofRat] + simp only [leviCivita_eq_ofRat_prod, toTensor_dualAll_eq_ofRat] rw [prodT_ofRat_ofRat, contrT_ofRat, permT_ofRat] apply (Tensor.basis _).repr.injective ext b @@ -227,7 +227,7 @@ lemma pauliContrDown_mul_pauliContr_mul_pauliContrDown : ({ simp only [map_add, Finsupp.coe_add, Pi.add_apply] simp only [permT_basis_repr_symm_apply, map_neg, Finsupp.coe_neg, Pi.neg_apply, map_smul, Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, ofRat_basis_repr_apply] - rw [Physlib.RatComplexNum.neg_I_mul_toComplexNum] + conv_rhs => arg 2; rw [Physlib.RatComplexNum.neg_I_mul_toComplexNum] apply Physlib.RatComplexNum.toComplexNum_eq_add_neg_add_add_iff.mpr decide +revert +kernel diff --git a/Physlib/Relativity/Tensors/LeviCivita/Complex.lean b/Physlib/Relativity/Tensors/LeviCivita/Complex.lean index af920b47ed..34c1bc588b 100644 --- a/Physlib/Relativity/Tensors/LeviCivita/Complex.lean +++ b/Physlib/Relativity/Tensors/LeviCivita/Complex.lean @@ -101,4 +101,15 @@ lemma leviCivita_eq_ofRat : ε4ℂ = ofRat (fun (b (IsReindexing.inv id leviCivita_isReindexing i))).trans (congrArg (fun x => (b x).val) (hinv i)) +/-- The components of the complex Levi-Civita tensor through `leviCivitaSymbolProd`, the +product form of the Levi-Civita symbol. Unlike the determinant appearing in +`leviCivita_eq_ofRat`, these components are cheap to evaluate, e.g. by `decide`. -/ +lemma leviCivita_eq_ofRat_prod : ε4ℂ = ofRat (fun + b : ComponentIdx (S := complexLorentzTensor) ![Color.up, Color.up, Color.up, Color.up] => + ⟨leviCivitaSymbolProd (fun i => Fin.cast (by fin_cases i <;> rfl) (b i)), 0⟩) := by + rw [leviCivita_eq_ofRat] + refine congrArg ofRat (funext fun b => ?_) + rw [← leviCivitaSymbol_eq_leviCivitaSymbolProd] + rfl + end complexLorentzTensor From ee6bba0b09adc3ad5f2a82f8d203abd0da9bb39a Mon Sep 17 00:00:00 2001 From: ZhiKai Pong Date: Sat, 19 Sep 2026 22:40:49 +0100 Subject: [PATCH 2/3] perf(PauliMatrices): use leviCivita_eq_ofRat_prod in leviCivita_mul_pauliDual MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The component proof of `leviCivita_mul_pauliDual` (#1661) evaluates `ε4ℂ` 2048 times under `decide +kernel`. With `leviCivita_eq_ofRat` each evaluation is a 4x4 determinant; `leviCivita_eq_ofRat_prod` makes it a product of signs. Co-Authored-By: Claude Fable 5.1 --- Physlib/Relativity/PauliMatrices/Relations.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Physlib/Relativity/PauliMatrices/Relations.lean b/Physlib/Relativity/PauliMatrices/Relations.lean index 4845a2b5ce..272810bba9 100644 --- a/Physlib/Relativity/PauliMatrices/Relations.lean +++ b/Physlib/Relativity/PauliMatrices/Relations.lean @@ -166,10 +166,10 @@ lemma leviCivita_mul_pauliDual : ({ε4ℂ | μ ν ρ κ ⊗ σ^^^ | τ(κ) α β = ε4ℂ | μ ν ρ κ ⊗ σ_^^ | κ α β}ᵀ : Prop) := by conv_lhs => - simp only [leviCivita_eq_ofRat, toTensor_dualLorentz_eq_ofRat] + simp only [leviCivita_eq_ofRat_prod, toTensor_dualLorentz_eq_ofRat] rw [prodT_ofRat_ofRat, contrT_ofRat] conv_rhs => - simp only [leviCivita_eq_ofRat, pauliCo_eq_ofRat] + simp only [leviCivita_eq_ofRat_prod, pauliCo_eq_ofRat] rw [prodT_ofRat_ofRat, contrT_ofRat] apply (Tensor.basis _).repr.injective ext b From 75672b47fdd47d63467e6b80eb3d6673a5fc82c9 Mon Sep 17 00:00:00 2001 From: ZhiKai Pong Date: Sun, 20 Sep 2026 22:49:33 +0100 Subject: [PATCH 3/3] refactor(LeviCivita): state the closed form of leviCivitaSymbol without a definition MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Remove the definition `leviCivitaSymbolProd`. The closed form is now the right-hand side of `leviCivitaSymbol_eq_prod_prod_Ioi` (renamed from `leviCivitaSymbol_eq_leviCivitaSymbolProd`), and `leviCivita_eq_ofRat_prod` states the components of `ε4ℂ` with the product written out. Co-Authored-By: Claude Fable 5.1 --- Physlib/Mathematics/LeviCivita/Basic.lean | 20 +++++++------------ .../Tensors/LeviCivita/Complex.lean | 16 ++++++++++----- 2 files changed, 18 insertions(+), 18 deletions(-) diff --git a/Physlib/Mathematics/LeviCivita/Basic.lean b/Physlib/Mathematics/LeviCivita/Basic.lean index e927c6923a..d99bd7b42b 100644 --- a/Physlib/Mathematics/LeviCivita/Basic.lean +++ b/Physlib/Mathematics/LeviCivita/Basic.lean @@ -33,9 +33,8 @@ permutation via `Matrix.det_permutation`. - `leviCivitaSymbol_comp_swap` : antisymmetry under transposition of two indices. - `leviCivitaSymbol_swap_comp` : antisymmetry under transposition of two index values. - `leviCivitaSymbol_eq_zero_iff` : the symbol vanishes exactly on repeated indices. -- `leviCivitaSymbolProd` : the product over pairs `i < j` of the sign of `g j - g i`, for - `g : Fin n → Fin n`. -- `leviCivitaSymbol_eq_leviCivitaSymbolProd` : on `Fin n` the symbol equals this product. +- `leviCivitaSymbol_eq_prod_prod_Ioi` : on `Fin n` the symbol is the product over pairs + `i < j` of the sign of `g j - g i`. ## iii. Table of contents @@ -162,17 +161,12 @@ lemma leviCivitaSymbol_eq_zero_iff {g : ι → ι} : -/ -/-- The product over pairs `i < j` of the sign of `g j - g i`, for `g : Fin n → Fin n`. -This equals `leviCivitaSymbol g` by `leviCivitaSymbol_eq_leviCivitaSymbolProd` and, unlike -the determinant defining `leviCivitaSymbol`, is cheap to evaluate, e.g. by `decide`. -/ -def leviCivitaSymbolProd {n : ℕ} (g : Fin n → Fin n) : ℤ := - ∏ i, ∏ j ∈ Finset.Ioi i, (if g i < g j then 1 else if g i = g j then 0 else -1) - /-- On `Fin n` the Levi-Civita symbol is the product over pairs `i < j` of the sign of -`g j - g i`. -/ -lemma leviCivitaSymbol_eq_leviCivitaSymbolProd {n : ℕ} (g : Fin n → Fin n) : - leviCivitaSymbol g = leviCivitaSymbolProd g := by - unfold leviCivitaSymbolProd +`g j - g i`. Unlike the determinant defining `leviCivitaSymbol`, this product is cheap to +evaluate, e.g. by `decide`. -/ +lemma leviCivitaSymbol_eq_prod_prod_Ioi {n : ℕ} (g : Fin n → Fin n) : + leviCivitaSymbol g = + ∏ i, ∏ j ∈ Finset.Ioi i, (if g i < g j then 1 else if g i = g j then 0 else -1) := by by_cases hg : Function.Injective g · obtain ⟨σ, rfl⟩ : ∃ σ : Equiv.Perm (Fin n), ⇑σ = g := ⟨Equiv.ofBijective g (Finite.injective_iff_bijective.mp hg), rfl⟩ diff --git a/Physlib/Relativity/Tensors/LeviCivita/Complex.lean b/Physlib/Relativity/Tensors/LeviCivita/Complex.lean index 34c1bc588b..4b25942f62 100644 --- a/Physlib/Relativity/Tensors/LeviCivita/Complex.lean +++ b/Physlib/Relativity/Tensors/LeviCivita/Complex.lean @@ -101,15 +101,21 @@ lemma leviCivita_eq_ofRat : ε4ℂ = ofRat (fun (b (IsReindexing.inv id leviCivita_isReindexing i))).trans (congrArg (fun x => (b x).val) (hinv i)) -/-- The components of the complex Levi-Civita tensor through `leviCivitaSymbolProd`, the -product form of the Levi-Civita symbol. Unlike the determinant appearing in -`leviCivita_eq_ofRat`, these components are cheap to evaluate, e.g. by `decide`. -/ +/-- The components of the complex Levi-Civita tensor as the product over pairs `i < j` of the +sign of `b j - b i`, from `leviCivitaSymbol_eq_prod_prod_Ioi`. Unlike the determinant appearing +in `leviCivita_eq_ofRat`, these components are cheap to evaluate, e.g. by `decide`. -/ lemma leviCivita_eq_ofRat_prod : ε4ℂ = ofRat (fun b : ComponentIdx (S := complexLorentzTensor) ![Color.up, Color.up, Color.up, Color.up] => - ⟨leviCivitaSymbolProd (fun i => Fin.cast (by fin_cases i <;> rfl) (b i)), 0⟩) := by + ⟨((∏ i : Fin 4, ∏ j ∈ Finset.Ioi i, + (if (Fin.cast (by fin_cases i <;> rfl) (b i) : Fin 4) < + (Fin.cast (by fin_cases j <;> rfl) (b j) : Fin 4) then 1 + else if (Fin.cast (by fin_cases i <;> rfl) (b i) : Fin 4) = + (Fin.cast (by fin_cases j <;> rfl) (b j) : Fin 4) then 0 else -1) : ℤ) : ℚ), 0⟩) := by rw [leviCivita_eq_ofRat] refine congrArg ofRat (funext fun b => ?_) - rw [← leviCivitaSymbol_eq_leviCivitaSymbolProd] + have h := leviCivitaSymbol_eq_prod_prod_Ioi + (fun i : Fin 4 => (Fin.cast (by fin_cases i <;> rfl) (b i) : Fin 4)) + rw [← h] rfl end complexLorentzTensor