Skip to content

feat: Add Quarks#1328

Open
jstoobysmith wants to merge 4 commits into
leanprover-community:masterfrom
jstoobysmith:FermionDirac
Open

feat: Add Quarks#1328
jstoobysmith wants to merge 4 commits into
leanprover-community:masterfrom
jstoobysmith:FermionDirac

Conversation

@jstoobysmith

Copy link
Copy Markdown
Member

Adding quarks to ./StandardModel, defining their representation under the Lorentz group and under the gauge group.

@github-actions

Copy link
Copy Markdown
Contributor

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 awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

@jstoobysmith jstoobysmith requested a review from zhikaip June 30, 2026 14:18

@nateabr nateabr left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Overall everything looks great, just some comments on how we could make this approach standard for other particle fields.

I hope they help :)

Comment thread Physlib/Particles/StandardModel/Fermions/QuarkDoublet.lean
Comment thread Physlib/Particles/StandardModel/Fermions/Quarks.lean Outdated
map_mul' := by intros; simp [map_mul]; rfl

/-!

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe we could define repLorentzGroup with valLineEquiv , such that it can match the style of repGuageGroup .

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done - agreed!

@nateabr

nateabr commented Jul 3, 2026

Copy link
Copy Markdown
Contributor

awaiting-author

@github-actions github-actions Bot added the awaiting-author A reviewer has asked the author a question or requested changes label Jul 3, 2026
@nateabr

nateabr commented Jul 3, 2026

Copy link
Copy Markdown
Contributor

t-particles

@github-actions github-actions Bot added the t-particles Particles label Jul 3, 2026
@jstoobysmith

Copy link
Copy Markdown
Member Author

Many thanks @nateabr

-awaiting-author

@github-actions github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes label Jul 3, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

t-particles Particles

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants