leanprover-community/physlib
Incorrect initialization of `S` in `ZModCharges` definition
Open
#1,528 opened on Aug 17, 2026
good first issue
Repository metrics
- Stars
- (642 stars)
- PR merge metrics
- (Avg merge 2d 14h) (75 merged PRs in 30d)
Description
⚠️ Found by a local LLM, not a human. This was flagged by an automated documentation-mistake finder (
qwen2.5-coder:7b) 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/ZMod.lean (around line 81) is incorrect.
Current text
def ZModCharges (n : ℕ) [NeZero n] : Finset (ChargeSpectrum (ZMod n)) :=
let S : Finset (ChargeSpectrum (ZMod n)) := ofFinset Finset.univ Finset.univ
S.filter (fun x => IsComplete x ∧ ¬ x.IsPhenoConstrained ∧ ¬ x.YukawaGeneratesDangerousAtLevel 4)
Why this is wrong
The code attempts to create a finite set of charge spectra with values in ZMod n, but the initialization of S is incorrect. ofFinset Finset.univ Finset.univ creates a set with a single element, which is not what is intended.
Suggested correction
def ZModCharges (n : ℕ) [NeZero n] : Finset (ChargeSpectrum (ZMod n)) :=
Finset.univ.filter (fun x => IsComplete x ∧ ¬ x.IsPhenoConstrained ∧ ¬ x.YukawaGeneratesDangerousAtLevel 4)