leanprover-community/physlib
Incorrect initialization of `S` in `ZModCharges` definition
Offen
#1.528 geöffnet am 17.08.2026
good first issue
Repository-Metriken
- Stars
- (642 Sterne)
- PR-Merge-Metriken
- (Durchschn. Merge 2T 14h) (75 gemergte PRs in 30 T)
Beschreibung
⚠️ 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)