feat(Tensors): HasContrDualBases, the dual-basis class, and the component formulas it collapses

[pariandrea]

The axioms of TensorSpecies do not say what S.contr gives on basis vectors. The general
component formula for a contraction therefore keeps S.contr (b x₁ ⊗ₜ b x₂) as an unevaluated
factor in a double sum, and each species proved its own single-sum formula by evaluating that
factor case by case. This PR states the missing fact once, as a class: at every color the basis at
S.τ c is dual to the basis at c under S.contr c, up to a bijection of labels. The real and
complex Lorentz species instantiate it, and their case-by-case proofs now follow from two general
lemmas (the −57 lines).

The class is a Prop asking only that some label bijection satisfies the δ law, so the label types
at c and S.τ c need not be equal (Fin 4 against Fin 1 ⊕ Fin 3 is allowed). Over a
nontrivial ring the bijection is unique, so the one picked by Classical.choose is canonical, each
species identifies it by a simp lemma, and the double-dual law is a theorem rather than a field.
The functionals v ↦ S.contr c (v ⊗ₜ b (S.τ c) x) are proved to be Module.Basis.dualBasis.

Added

Physlib/Relativity/Tensors/TensorSpecies/DualBasis.lean (new)

• IsContrDualMatching S c e: the bijection e : basisIdx (S.τ c) ≃ basisIdx c satisfies the δ
  law, S.contr c (b c x₁ ⊗ₜ b (S.τ c) x₂) = if x₁ = e x₂ then 1 else 0.
• IsContrDualMatching.unique: over a nontrivial ring two such bijections are equal.
• HasContrDualBases: the class, with one field exists_matching : ∀ c, ∃ e, IsContrDualMatching S c e.
• HasContrDualBases.contrDualIdxEquiv: the bijection, chosen by Classical.choose.
• HasContrDualBases.contr_basis_eq_ite: the δ law for contrDualIdxEquiv.
• HasContrDualBases.contrDualIdxEquiv_eq_of_isContrDualMatching: any bijection satisfying the δ
  law is contrDualIdxEquiv; this is how a species identifies it.
• HasContrDualBases.contrDualIdxEquiv_tau: the bijection at S.τ c is the inverse of the one at
  c, through S.τ (S.τ c) = c, proved from contr_tmul_symm and uniqueness.
• HasContrDualBases.contr_tmul_basis_eq_dualBasis: contracting with b (S.τ c) x is the
  Module.Basis.dualBasis functional at the matched label.

Physlib/Relativity/Tensors/TensorSpecies/Basic.lean

• equivCast_basis: map_basis_eq with the cast written as Equiv.cast, the form
  contr_tmul_symm produces; used in contrDualIdxEquiv_tau.

Physlib/Relativity/Tensors/Contraction/Basis.lean

• Pure.contrPCoeff_basisVector: the contraction coefficient of a basis vector is the δ.
• contrT_basis_repr_apply_eq_sum_dual: a component of a contraction is a single sum over the
  labels at the first contracted index.

Physlib/Relativity/Tensors/RealTensor/Basic.lean

• isContrDualMatching_refl, the instance, and contrDualIdxEquiv_eq_refl (simp): the
  bijection is the identity.
• contrPCoeff_basis, contrT_basis_repr_apply_eq_fin: statements unchanged, proofs now two lines.

Physlib/Relativity/Tensors/ComplexTensor/Basic.lean

• isContrDualMatching_finCongr, the instance, and contrDualIdxEquiv_eq_finCongr (simp): the
  bijection is finCongr repDim_tau.
• contrPCoeff_basis: statement unchanged, proof now three lines.

Removed: none.

Reviewer map

1. DualBasis.lean, sections A to C: the δ law, uniqueness, the class and the chosen bijection.
2. DualBasis.lean, sections D and E, with equivCast_basis: the double-dual law and the link
   to Module.Basis.dualBasis.
3. Contraction/Basis.lean: the two general lemmas.
4. RealTensor/Basic.lean, then ComplexTensor/Basic.lean: the instances and the shortened proofs.

[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.

[jstoobysmith]

One small comment here. Otherwise this looks good.

[jstoobysmith]

I think the doc-string of this result can be made a bit simpler.

[pariandrea]

I simplified the docstring. I did the same for the RealTensor too.

[jstoobysmith]

awaiting-author

[pariandrea]

-awaiting-author

[jstoobysmith]

Approved. Will merge shortly. Many thanks.