refactor: replace RatComplexNum by Mathlib's GaussianInt - #1682
Conversation
…ssianInt All components that went through `Physlib.RatComplexNum` are 0, ±1, ±i or integer Levi-Civita signs, so Mathlib's `GaussianInt` with `GaussianInt.toComplex` and `GaussianInt.toComplex_injective` replaces it. - Delete `Physlib/Mathematics/RatComplexNum.lean`. - Rename `ComplexTensor/OfRat.lean` to `ComplexTensor/OfGaussianInt.lean`; `ofRat` becomes `ofGaussianInt : (ComponentIdx c → GaussianInt) →ₛₗ[GaussianInt.toComplex] ℂT(c)`, and all `*_ofRat*` lemmas become `*_ofGaussianInt*`; `contr_basis_ratComplexNum` becomes `contr_basis_gaussianInt`. - `pauliContrComponent`, `pauliContrDownComponent` and the Levi-Civita components are now `GaussianInt`-valued. - Replace the `RatComplexNum` helper lemmas in `PauliMatrices/Relations.lean` by inline `show … from` rewrites, and close `toTensor_dualLeft_eq_ofGaussianInt` and `toTensor_dualLorentzLeft_eq_ofGaussianInt` with `congrArg` instead of `congr`. Heartbeats (v4.34): Relations.lean 770,274k -> 707,080k; ToTensor.lean (declarations above 20M) 538.6M -> 521.0M. Kernel `decide` is cheaper on integers than on rationals. Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
`ofGaussianInt f` is now `ofComponents c (fun b => GaussianInt.toComplex (f b))` instead of going through `(Tensor.basis c).repr.symm` and `Finsupp.linearEquivFunOnFinite`; `ofGaussianInt_basis_repr_apply` follows from `componentMap_ofComponents`. Performance neutral (Relations.lean and ToTensor.lean within 0.2%). Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
|
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.
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. |
jstoobysmith
left a comment
There was a problem hiding this comment.
Approved - many thanks. Looks good to me.
1. Switch to
GaussianInt, renameofRat→ofGaussianIntEvery coefficient that went through
Physlib.RatComplexNumis 0, ±1, ±i or an integerLevi-Civita sign, so Mathlib's
GaussianInt(GaussianInt.toComplex,GaussianInt.toComplex_injective) replaces it. No statement about Pauli matrices,metrics, units or the Levi-Civita tensor changes.
Physlib/Mathematics/RatComplexNum.lean(the type, its ring structure,toComplexNumand its helper lemmas).ComplexTensor/OfRat.lean→OfGaussianInt.lean, and every…ofRat…declaration →
…ofGaussianInt…(33 names);contr_basis_ratComplexNum→contr_basis_gaussianInt.pauliContrComponent,pauliContrDownComponentand the Levi-Civita components arenow
GaussianInt-valued.2. Mini-refactor: define
ofGaussianIntviaTensor.ofComponentsofGaussianInt fis nowofComponents c (fun b => GaussianInt.toComplex (f b)), reusingthe existing tensor API instead of going through
(Tensor.basis c).repr.symmandFinsupp.linearEquivFunOnFinite.ofGaussianInt_basis_repr_applynow follows fromcomponentMap_ofComponents. Performance-neutral.Performance (heartbeats, same base)
PauliMatrices/Relations.leanPauliMatrices/ToTensor.lean(declarations > 20M)The gain comes from commit 1: kernel
decideis cheaper on integer than on rationalarithmetic. No declaration got slower.
Reviewer map
Review commit by commit. In commit 1, start with
ComplexTensor/OfGaussianInt.lean,then
PauliMatrices/ToTensor.lean,LeviCivita/Complex.leanandPauliMatrices/Relations.lean; the rest is the mechanical rename. Commit 2 touches onlyOfGaussianInt.lean.Disclaimer: I instructed claude to make these changes and everything looks reasonable to me
🤖 Generated with Claude Code