feat(PhyslibAlpha/Particles): The effective potential of the 2HDM#1357
feat(PhyslibAlpha/Particles): The effective potential of the 2HDM#1357jstoobysmith wants to merge 25 commits into
Conversation
Co-Authored-By: Claude <claude@users.noreply.github.com>
Co-Authored-By: Claude <claude@users.noreply.github.com>
Co-Authored-By: Claude <claude@users.noreply.github.com>
Co-Authored-By: Claude <claude@users.noreply.github.com>
Co-Authored-By: Claude <claude@users.noreply.github.com>
Co-Authored-By: Claude <claude@users.noreply.github.com>
Co-Authored-By: Claude <claude@users.noreply.github.com>
Co-Authored-By: Claude <claude@users.noreply.github.com>
Co-Authored-By: Claude <claude@users.noreply.github.com>
Co-Authored-By: Claude <claude@users.noreply.github.com>
Co-Authored-By: Claude <claude@users.noreply.github.com>
Co-Authored-By: Claude <claude@users.noreply.github.com>
Co-Authored-By: Claude <claude@users.noreply.github.com>
Co-Authored-By: Claude <claude@users.noreply.github.com>
Co-Authored-By: Claude <claude@users.noreply.github.com>
prompt> Continue Co-Authored-By: Claude <claude@users.noreply.github.com>
prompt: Tidy up the files removing everything which is unnessary in proving effectivePotential_is_polynomial_gramVector Co-Authored-By: Claude <claude@users.noreply.github.com>
Prompt: Reorganize the proof so we follow the API structure of Physlib. This means: Rephrase things in terms of results on physically meaningful definitions, make sure all the results around one definition sit within the same place within the project. Co-Authored-By: Claude <claude@users.noreply.github.com>
prompt: "The first fundamental Theorm" is not physics focused, nor does it correspond to building lemmas around physically relevant definitions. Please do this throughout this directory. To bring the physics back to the front you may also need to rename some things Co-Authored-By: Claude <claude@users.noreply.github.com>
jstoobysmith
added
the
PhyslibAlpha
|
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 |
1 participant
The effective potential of the 2HDM model, formalised using AI (Claude Opus 4.8) taking about 10 hours. Some commits have the prompts which lead to them in their comments (the earlier ones do not).
I wrote the initial theorem and gave some minor guidance when it got stuck.