Incorrect 'complex' documentation for real Lorentz tensors in Metrics/Basic.lean
#1,532 创建于 2026年8月17日
仓库指标
- 星标
- (642 个星标)
- PR 合并指标
- (平均合并 2天 14小时) (30 天内合并 75 个 PR)
描述
⚠️ 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. -/