Incorrect 'complex' documentation for real Lorentz tensors in Metrics/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/Metrics/Basic.lean (around line 33) is incorrect.

Current text

/-- The metric `ηᵢᵢ` as a complex Lorentz tensor. -/

Why this is wrong

The documentation for coMetric and contrMetric in physlib/Physlib/Relativity/Tensors/RealTensor/Metrics/Basic.lean incorrectly describes these tensors as "complex Lorentz tensors". This is wrong because both declarations use the type ℝT, which explicitly denotes real-valued tensors. The term "complex" contradicts the type's definition and the context of the file, which focuses on real tensor structures.

The correction changes "complex" to "real", aligning the documentation with the actual type ℝT and the mathematical context of Lorentz tensors in relativity. This ensures consistency between the code's type system and its semantic description, avoiding confusion for users relying on accurate documentation.

Suggested correction

/-- The metric `ηᵢᵢ` as a real Lorentz tensor. -/

Open Physlib/Relativity/Tensors/RealTensor/Metrics/Basic.lean around line 33 and inspect the coMetric and contrMetric documentation alongside their ℝT types. Correct the wording so the tensors are described as real Lorentz tensors, then verify the file remains consistent with the surrounding real-tensor documentation.