Docstring falsely claims tensorial notation definitions exist in Pauli Matrix file

Summary

The documentation in Physlib/Relativity/PauliMatrices/Basic.lean (around line 10) is incorrect.

Current text

/-!

## Pauli matrices

The pauli matrices are defined ultimately through
- `pauliMatrix` which is a map `Fin 1 ⊕ Fin 3 → Matrix (Fin 2) (Fin 2) ℂ`.
  The notation `σ` can be used as short hand.

A tensorial structure is put on `Fin 1 ⊕ Fin 3 → Matrix (Fin 2) (Fin 2) ℂ` to allow the
use of index notation. We then define the following notation:

- `σ^^^` is the tensorial version of the Pauli matrices, which is a complex Lorentz tensor
  of type `ℂT[.up, .upL, .upR]`.

and the following abbreviations:
- `σ_^^` is the Pauli matrices as a complex Lorentz tensor of type `ℂT[.down, .upL, .upR]`.
- `σ___` is the Pauli matrices as a complex Lorentz tensor of type `ℂT[.down, .downR, .downL]`.
- `σ^__` is the Pauli matrices as a complex Lorentz tensor of type `ℂT[.up, .downR, .downL]`.

-/

Why this is wrong

The documentation correctly identifies that pauliMatrix and the shorthand notation σ are defined within this file's PauliMatrix namespace. However, it falsely claims that tensorial notations like σ^^^, σ_^^, σ___, and σ^__ exist to support index notation. These specific definitions are absent from the code.

The fix removes these assertions about undefined abbreviations while preserving the accurate context for pauliMatrix.

Suggested correction

/-!

## Pauli matrices

The pauli matrices are defined ultimately through
- `pauliMatrix` which is a map `Fin 1 ⊕ Fin 3 → Matrix (Fin 2) (Fin 2) ℂ`.
  The notation `σ` can be used as short hand.

A tensorial structure is put on `Fin 1 ⊕ Fin 3 → Matrix (Fin 2) (Fin 2) ℂ` to allow the
use of index notation.

-/

---

Found with a local LLM pass over Physlib documentation (qwen3.5:9b); 10 of 10 independent verification runs agreed this is a genuine error before filing. Please sanity-check before merging.