⚠️ 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/Particles/SuperSymmetry/SU5/ChargeSpectrum/Map.lean (around line 21) is incorrect.
Current text
There are various properties which are preserved under this mapping:
- Anomaly cancellation.
- The presence of a specific term in the potential.
- Being complete.
Why this is wrong
The documentation in physlib/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Map.lean incorrectly states that "anomaly cancellation" is preserved under the map function, but no lemma in the file supports this assertion. The module defines properties like map_allowsTerm and map_isComplete_iff, which correspond to the documented preservation of potential terms and completeness, respectively. However, there is no declaration or proof related to anomaly cancellation in the code.
The correction removes "anomaly cancellation" from the list of preserved properties, aligning the documentation with the actual implementation. This change ensures that only properties with corresponding lemmas (like map_allowsTerm and map_isComplete_iff) are claimed to be preserved under the mapping. The remaining claims about potential terms and completeness are supported by explicit proofs in the code.
Suggested correction
There are various properties which are preserved under this mapping:
- The presence of a specific term in the potential.
- Being complete.
Summary
The documentation in
Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Map.lean(around line 21) is incorrect.Current text
Why this is wrong
The documentation in
physlib/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Map.leanincorrectly states that "anomaly cancellation" is preserved under themapfunction, but no lemma in the file supports this assertion. The module defines properties likemap_allowsTermandmap_isComplete_iff, which correspond to the documented preservation of potential terms and completeness, respectively. However, there is no declaration or proof related to anomaly cancellation in the code.The correction removes "anomaly cancellation" from the list of preserved properties, aligning the documentation with the actual implementation. This change ensures that only properties with corresponding lemmas (like
map_allowsTermandmap_isComplete_iff) are claimed to be preserved under the mapping. The remaining claims about potential terms and completeness are supported by explicit proofs in the code.Suggested correction