auto-task(StandardModel.Representations): record TODO for Standard Model fermion content as left-handed Weyl fermions - #1322
Conversation
…del fermion content as left-handed Weyl fermions Co-authored-by: Claude <noreply@anthropic.com>
|
Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally. If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks. If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip. Important: If a reviewer adds an |
Summary
Records a single
TODOin the Standard Model representations file for the structureholding the Standard Model's fermionic content, expressed entirely as left-handed
Weyl fermions.
The TODO was written by a human (the task author); Claude placed it in the
correct file and section of the library and verified the build and linters.
Original request
What changed
In
Physlib/Particles/StandardModel/Representations.lean, added:The required
public import Physlib.Meta.TODO.Basicwas added, since this file onlyimported pure Mathlib and the
TODOcommand did not otherwise elaborate.Why this location
Representations.leandefines the representations appearing in the Standard Model(
repU1,fundamentalSU2) and lives alongsideBasic.leanwhich defines the globalgauge group
GaugeGroupI. The fermion-content structure is exactly the matter thattransforms in these representations, so this is the most specific existing home. The
TODO text refers to the relevant existing definitions (
Fermion.LeftHandedWeyl,GaugeGroupI,repU1,fundamentalSU2) so a future contributor has the buildingblocks to hand. No equivalent TODO already existed.
Verification
lake buildsucceeds with no new errors, warnings,sorrys, or axioms.lake exe runPhyslibLinters— clean../scripts/lint-style.sh— clean.No declarations were implemented or proved; this PR only records the TODO.
Human review