From 812f5d3de7e647607fbedd45c05d46f2e1e26f11 Mon Sep 17 00:00:00 2001 From: ZhiKai Pong Date: Sat, 19 Sep 2026 17:19:10 +0100 Subject: [PATCH 1/2] docs(PauliMatrices): cite the published source for the three-Pauli identities The docstrings of `pauliContr_mul_pauliContrDown_mul_pauliContr` and `pauliContrDown_mul_pauliContr_mul_pauliContrDown` referred to "Equation (2.26)" and "Equation (2.27)" without naming a source. Those numbers come from the 2004 draft linked in #341, in which the two equations differ from the statements proved here. Cite instead equations (2.54) and (2.55) of the published paper, arXiv:0812.1594, which agree with the Lean statements and use the same conventions, and add a References section to the module docstring. Remove the stale "not currently cited" note from that bibliography entry. No declarations are added, removed or changed. Co-Authored-By: Claude Fable 5.1 --- Physlib/Relativity/PauliMatrices/Relations.lean | 16 ++++++++++++---- docs/references.bib | 3 +-- 2 files changed, 13 insertions(+), 6 deletions(-) diff --git a/Physlib/Relativity/PauliMatrices/Relations.lean b/Physlib/Relativity/PauliMatrices/Relations.lean index 806a46097..2a64c08f7 100644 --- a/Physlib/Relativity/PauliMatrices/Relations.lean +++ b/Physlib/Relativity/PauliMatrices/Relations.lean @@ -18,6 +18,12 @@ for the Pauli four-vectors. The current way this result is proved is by using tensor tree manipulations. There is likely a more direct path to this result. +## References + +* Dreiner, Haber and Martin, *Two-component spinor techniques and Feynman rules for quantum + field theory and supersymmetry*, arXiv:0812.1594, equations (2.54) and (2.55), in the + conventions `g = diag(+1, -1, -1, -1)` and `ε⁰¹²³ = +1`. [ref: Dreiner:2008tw] + -/ @[expose] public section @@ -164,9 +170,10 @@ lemma leviCivita_mul_pauliDual : · decide · rfl -/-- Equation (2.26), the three-Pauli identity +/-- The three-Pauli identity `σ^μ barσ^ν σ^ρ = g^{μν} σ^ρ - g^{μρ} σ^ν + g^{νρ} σ^μ - + i ε^{μνρκ} σ_κ`, with barred and lowered forms expressed through index dualization `τ`. -/ + + i ε^{μνρκ} σ_κ`, with barred and lowered forms expressed through index dualization `τ`. +This is equation (2.54) of arXiv:0812.1594. [ref: Dreiner:2008tw] -/ lemma pauliContr_mul_pauliContrDown_mul_pauliContr : ({ σ^^^ | μ α β ⊗ σ^^^ | ν τ(α') τ(β) ⊗ σ^^^ | ρ α' β' = ((((η | μ ν ⊗ σ^^^ | ρ α β') + (-((η | μ ρ ⊗ σ^^^ | ν α β')))) @@ -191,9 +198,10 @@ lemma pauliContr_mul_pauliContrDown_mul_pauliContr : ({ apply Physlib.RatComplexNum.toComplexNum_eq_add_neg_add_add_iff.mpr decide +revert +kernel -/-- Equation (2.27), the conjugate three-Pauli identity +/-- The conjugate three-Pauli identity `barσ^μ σ^ν barσ^ρ = g^{μν} barσ^ρ - g^{μρ} barσ^ν + g^{νρ} barσ^μ - - i ε^{μνρκ} barσ_κ`, with barred and lowered forms expressed through index dualization `τ`. -/ + - i ε^{μνρκ} barσ_κ`, with barred and lowered forms expressed through index dualization `τ`. +This is equation (2.55) of arXiv:0812.1594. [ref: Dreiner:2008tw] -/ lemma pauliContrDown_mul_pauliContr_mul_pauliContrDown : ({ σ^^^ | μ τ(α) τ(β) ⊗ σ^^^ | ν α β' ⊗ σ^^^ | ρ τ(α') τ(β') = ((((η | μ ν ⊗ σ^^^ | ρ τ(α') τ(β)) diff --git a/docs/references.bib b/docs/references.bib index dee4808c2..ded357f7d 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -33,8 +33,7 @@ @article{Dreiner:2008tw doi = {10.1016/j.physrep.2010.05.002}, journal = {Phys. Rept.}, pages = {1-196}, - year = {2010}, - note = {not currently cited by any module; kept for future use} + year = {2010} } @article{Lohitsiri:2019fuu, From 155867e29ed86918dbf4b36a786c95860f574e53 Mon Sep 17 00:00:00 2001 From: ZhiKai Pong Date: Sat, 19 Sep 2026 17:26:52 +0100 Subject: [PATCH 2/2] docs(PauliMatrices): keep the citation in the References section only Drop the explicit reference from the docstrings of the two three-Pauli identities, leaving it in the module References section, and put each displayed formula on a single line so the inline code is not broken across lines. Co-Authored-By: Claude Fable 5.1 --- Physlib/Relativity/PauliMatrices/Relations.lean | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/Physlib/Relativity/PauliMatrices/Relations.lean b/Physlib/Relativity/PauliMatrices/Relations.lean index 2a64c08f7..d272c11bb 100644 --- a/Physlib/Relativity/PauliMatrices/Relations.lean +++ b/Physlib/Relativity/PauliMatrices/Relations.lean @@ -171,9 +171,8 @@ lemma leviCivita_mul_pauliDual : · rfl /-- The three-Pauli identity -`σ^μ barσ^ν σ^ρ = g^{μν} σ^ρ - g^{μρ} σ^ν + g^{νρ} σ^μ - + i ε^{μνρκ} σ_κ`, with barred and lowered forms expressed through index dualization `τ`. -This is equation (2.54) of arXiv:0812.1594. [ref: Dreiner:2008tw] -/ +`σ^μ barσ^ν σ^ρ = g^{μν} σ^ρ - g^{μρ} σ^ν + g^{νρ} σ^μ + i ε^{μνρκ} σ_κ`, +with barred and lowered forms expressed through index dualization `τ`. -/ lemma pauliContr_mul_pauliContrDown_mul_pauliContr : ({ σ^^^ | μ α β ⊗ σ^^^ | ν τ(α') τ(β) ⊗ σ^^^ | ρ α' β' = ((((η | μ ν ⊗ σ^^^ | ρ α β') + (-((η | μ ρ ⊗ σ^^^ | ν α β')))) @@ -199,9 +198,8 @@ lemma pauliContr_mul_pauliContrDown_mul_pauliContr : ({ decide +revert +kernel /-- The conjugate three-Pauli identity -`barσ^μ σ^ν barσ^ρ = g^{μν} barσ^ρ - g^{μρ} barσ^ν + g^{νρ} barσ^μ - - i ε^{μνρκ} barσ_κ`, with barred and lowered forms expressed through index dualization `τ`. -This is equation (2.55) of arXiv:0812.1594. [ref: Dreiner:2008tw] -/ +`barσ^μ σ^ν barσ^ρ = g^{μν} barσ^ρ - g^{μρ} barσ^ν + g^{νρ} barσ^μ - i ε^{μνρκ} barσ_κ`, +with barred and lowered forms expressed through index dualization `τ`. -/ lemma pauliContrDown_mul_pauliContr_mul_pauliContrDown : ({ σ^^^ | μ τ(α) τ(β) ⊗ σ^^^ | ν α β' ⊗ σ^^^ | ρ τ(α') τ(β') = ((((η | μ ν ⊗ σ^^^ | ρ τ(α') τ(β))