Skip to content

refactor: Add invariants theorem for Higgs potential#1173

Open
jstoobysmith wants to merge 3 commits into
leanprover-community:masterfrom
jstoobysmith:vectorCovectorReps
Open

refactor: Add invariants theorem for Higgs potential#1173
jstoobysmith wants to merge 3 commits into
leanprover-community:masterfrom
jstoobysmith:vectorCovectorReps

Conversation

@jstoobysmith

Copy link
Copy Markdown
Member

Adding the theorem which says that the Higgs potential is the most general potential up to order 4 which is invariant under the SM action.

@jstoobysmith jstoobysmith added RFC Request for comment t-particles Particles labels Jun 12, 2026
@github-actions

Copy link
Copy Markdown
Contributor

Thank you for this PR, which will now be reviewed. 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 want to bring attention to this PR, please write a message on this
thread of the Lean Zulip.

@morrison-daniel

Copy link
Copy Markdown
Collaborator

Can't give a full review yet, but I think some of this should be separated into other lemmas. For example, define V' and p' in general and then pretty much each of your have statements can be its own lemma.

@morrison-daniel morrison-daniel self-assigned this Jun 14, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

RFC Request for comment t-particles Particles

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants