Documentation claims anomaly cancellation is preserved under mapping without

⚠️ 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.

Open Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Map.lean around lines 21–24 and compare the documented properties with declarations such as map_allowsTerm and map_isComplete_iff. Confirm that no anomaly-cancellation preservation result is present, then update the list so it only claims the supported properties; done means the documentation matches the implementation.