Incorrect documentation for realLorentzTensor in Basic.lean

⚠️ Found by a local LLM, not a human. This was flagged by an automated documentation-mistake finder (qwen3:14b) and passed 10/10 independent verification runs before filing, but it has not been reviewed by a person. Please check it's a genuine error before acting on it.

Summary

The documentation in Physlib/Relativity/Tensors/RealTensor/Basic.lean (around line 67) is incorrect.

Current text

/-- The tensor structure for complex Lorentz tensors. -/

Why this is wrong

The docstring for realLorentzTensor incorrectly claims it defines "complex Lorentz tensors", but the declaration's name and surrounding context clearly indicate it is for real tensors. The file's comments explicitly mention "Real Lorentz tensors" and the definition uses Lorentz.ContrMod/Lorentz.CoMod, which are real vector spaces.

This discrepancy arises because the docstring was not updated when the definition was renamed from a complex variant to a real one. The correction aligns the documentation with the actual purpose of realLorentzTensor, which is consistent with the file's focus on real tensor structures and the use of ℝ as the scalar field in its type signature.

Suggested correction

/-- The tensor structure for real Lorentz tensors. -/

Open Physlib/Relativity/Tensors/RealTensor/Basic.lean around line 67 and inspect the realLorentzTensor declaration and its surrounding comments. Confirm that the docstring describes real rather than complex Lorentz tensors, then update the wording and verify the file remains valid.