Documentation claims support for RHNs in MSSM but code does not implement them

[Alex-Zughaid]

⚠️ 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/MSSMNu/AnomalyCancellation/Basic.lean (around line 10) is incorrect.

Current text

# The MSSM with 3 families and RHNs

We define the system of ACCs for the MSSM with 3 families and RHNs.
We define the system of charges for 1-species. We prove some basic lemmas about them.

Why this is wrong

The file's documentation states it defines anomaly cancellation conditions for the MSSM with 3 families and right-handed neutrinos (RHNs). However, the code only implements charge definitions and ACCs for the standard MSSM without RHNs. The MSSMCharges structure and related lemmas like toSpecies split charges into SM fermions and MSSM Higgses but do not include any RHN-specific species or charges.

The correction removes mention of RHNs because the code lacks any definitions that would account for them, such as additional fermion species in MSSMSpecies or corresponding terms in anomaly equations. The current implementation aligns with the standard MSSM, which does not include right-handed neutrinos. This matches the actual Lean declarations, which define only 18 SM fermions plus 2 Higgses in toSMPlusH, without any RHN contributions.

Suggested correction

# The MSSM with 3 families

We define the system of ACCs for the MSSM with 3 families.
We define the system of charges for 1-species. We prove some basic lemmas about them.