⚠️ 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. -/
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
coMetricandcontrMetricinphyslib/Physlib/Relativity/Tensors/RealTensor/Metrics/Basic.leanincorrectly 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
ℝTand 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. -/