perf(PauliMatrices): evaluate Levi-Civita components as a product of signs

[zhikaip]

In a heartbeat profile of all 585 files on master, the three most expensive files are WickContraction/TimeCond.lean (1,756k), WickContraction/Join.lean (1,241k) and PauliMatrices/Relations.lean (1,185k). The next file is at 705k, and a typical file is at 3k–40k. They also sit at the ends of the two longest import chains, so they bound the parallel build time. #1662 deals with the two Wick files; this PR deals with Relations.lean.

The three-Pauli identities are proved by decide +kernel over all components. leviCivita_eq_ofRat gives the components of ε4ℂ as a generalizedKroneckerDelta, i.e. a 4×4 determinant, which the kernel evaluates through permutation sums. This PR adds the closed form ∏_{i<j} sign (g j - g i) for the Levi-Civita symbol on Fin n and uses it for the components instead. Evaluating all 256 components of ε4ℂ costs the kernel 40.3M heartbeats in the determinant form and 4.3M in the product form. The PR also restricts two rws that traversed the whole goal to the summand they apply to.

Added:

• leviCivitaSymbolProd (def) and leviCivitaSymbol_eq_leviCivitaSymbolProd, in Mathematics/LeviCivita/Basic.lean
• leviCivita_eq_ofRat_prod, in Tensors/LeviCivita/Complex.lean

Nothing is removed and no statement changes. Three proofs change: pauliContr_mul_pauliContrDown_mul_pauliContr, pauliContrDown_mul_pauliContr_mul_pauliContrDown and leviCivita_mul_pauliDual.

Relations.lean, thousand heartbeats	Before	After
whole file	1,185,316	743,601 (−37%)
pauliContr_mul_pauliContrDown_mul_pauliContr	408,138	171,955
pauliContrDown_mul_pauliContr_mul_pauliContrDown	517,382	236,754
leviCivita_mul_pauliDual	~29,000	100,824

Relation to #1661. The current proof of leviCivita_mul_pauliDual hits a kernel timeout on v4.34, and #1661 (commit 191842c) replaces it with a proof by decide +kernel over components, using leviCivita_eq_ofRat. That proof evaluates ε4ℂ 2048 times (256 components × the contracted index × both sides), and every evaluation is a determinant: by the figures above, about 320M heartbeats of kernel work for ε4ℂ alone, which would make this small lemma as expensive as one of the three-Pauli identities before this PR. This PR takes the same proof and states it with leviCivita_eq_ofRat_prod, which brings that part down to about 34M; the whole lemma then measures 100,824k. That is the last row of the table. It is a regression against the present proof, accepted because the present proof does not survive v4.34. I have checked that this branch builds on v4.34 when merged onto #1661. The two PRs will conflict in this one proof; the resolution is to keep the leviCivita_eq_ofRat_prod version, after which 191842c is no longer needed.

Disclaimer: I instructed Claude to investigate and find opportunities to speed up build times; the changes look reasonable to me.

🤖 Generated with Claude Code

[github-actions]

Thank you for this pull-request (PR). If this is your first PR, welcome to the community!

Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.

1. Some automated checks will be run on your PR. You can see the results of these checks at the buttom of your PR page. If any of these checks fail, you will need to fix the issues before your PR can be merged. You can learn more about these here, including how to run them locally, which is sometimes quicker than relying on the GitHub Actions. If you have never had a PR merged before, you may have to wait for a reviewer to manually start these checks (this is for security).

2. A reviewer will look at your PR and may ask you to make changes. This may happen a couple of days after you submit your PR, so you may need to be patient. But it should not be longer than that - if it is please bring it to the attention of the community on the Zulip. The level of review will depend on where your PR is submitted. If it is submitted to ./Physlib or ./QuantumInfo, the review will be more thorough than if it is submitted to ./PhyslibAlpha. You can find out more about what the review process is looking for in our review guidelines. If a reviewer adds an awaiting-author label to your PR, address the review comments, then please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

3. The reviewer will either approve your PR, or request more changes (in which case we return to step 2). Once your PR is approved, it will be merged by a maintainer, this should happen shortly after approval, though you may get more comments at this stage.

Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages.

If you have any problems or questions, please reach out to the community on the Zulip.

[zhikaip]

Highlighting the following: this PR will conflict will the version bump in #1661, and the current changes are based on the proposed change there. Either order of merging works, but I think merging this first helps with performance (I forked the #1661 branch and it takes painfully long to build the file)

[zhikaip]

After the version bump my 16GB RAM PC simply cannot build Relativity/PauliMatrices/Relations.lean on master (stuck at the decide steps), so I think this change is a massive performance improvement.

A related question: is there any reason why you introduced RatComplexNum? It seems like Mathlib's GaussianInt suffices for this purpose (all the component tables are 0, ±1, ±i), and that would be a further speed-up if we completely replace the RatComplexNum API.

[jstoobysmith]

I think if Mathlib GaussianInt works, then we should use that instead of RatComplexNum. Is this up to date with the bump? If so, I'll approve it, and I'll leave you to merge it.