Comment claims equivalence between `ContrℝModule` and complex-valued vectors
#1,508 建立於 2026年8月11日
倉庫指標
- 星標
- (642 顆星)
- PR 合併指標
- (PR 指標待抓取)
描述
Summary
The documentation in Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Modules.lean (around line 46) is incorrect.
Current text
/-- The equivalence between `ContrℝModule` and `Fin 1 ⊕ Fin d → ℂ`. -/
Why this is wrong
The documentation comment above def toFin1dℝFun asserts an equivalence between ContrℝModule and vectors valued in ℂ. This contradicts the actual definition of the structure, which is named ContrMod rather than ContrℝModule. Additionally, the file header explicitly describes these as "Real Lorentz vectors", indicating a real field.
The implementation defines toFin1dℝFun mapping between ContrMod d and functions into ℝ, not ℂ. Consequently, the scalar field in the type signature of the equivalence is incorrect in the comment.
Updating this comment to reference ContrMod and ℝ aligns the documentation with the code's reality regarding real Lorentz vector modules.
Suggested correction
/-- The equivalence between `ContrMod` and `Fin 1 ⊕ Fin d → ℝ`. -/
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.