⚠️ 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/LeviCivita/Contractions.lean (around line 17) is incorrect.
Current text
the rank-four Levi-Civita tensor `leviCivita` (notation `ε4`) in `d = 3`
Why this is wrong
The documentation claims that ε4 represents a rank-four Levi-Civita tensor in 3-dimensional space. This is incorrect because the rank of a Levi-Civita tensor must match the dimension of the space it inhabits. A rank-four Levi-Civita tensor can only exist in 4-dimensional space, not 3.
The correction changes the description to refer to a rank-three Levi-Civita tensor in 4-dimensional space (d = 4), which aligns with the code's use of Fin 4 indices and the mathematical properties being proved. The file's lemmas (e.g., euclidLeviCivita_symbol_contract_zero) operate on 4-index tensors, confirming the context is 4D space.
The error arose from a mismatch between the tensor's rank, the space dimension, and the notation used in the code, which consistently refers to 4-dimensional indices via Fin 4.
Suggested correction
the rank-three Levi-Civita tensor `leviCivita` (notation `ε4`) in `d = 4`
Summary
The documentation in
Physlib/Relativity/Tensors/LeviCivita/Contractions.lean(around line 17) is incorrect.Current text
Why this is wrong
The documentation claims that
ε4represents a rank-four Levi-Civita tensor in 3-dimensional space. This is incorrect because the rank of a Levi-Civita tensor must match the dimension of the space it inhabits. A rank-four Levi-Civita tensor can only exist in 4-dimensional space, not 3.The correction changes the description to refer to a rank-three Levi-Civita tensor in 4-dimensional space (
d = 4), which aligns with the code's use ofFin 4indices and the mathematical properties being proved. The file's lemmas (e.g.,euclidLeviCivita_symbol_contract_zero) operate on 4-index tensors, confirming the context is 4D space.The error arose from a mismatch between the tensor's rank, the space dimension, and the notation used in the code, which consistently refers to 4-dimensional indices via
Fin 4.Suggested correction