Comment claims equivalence between `ContrℝModule` and complex-valued vectors
#1 508 ouverte le 11 août 2026
Métriques du dépôt
- Stars
- (642 étoiles)
- Métriques de merge PR
- (Métriques PR en attente)
Description
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.