feat: Effective potential for Weyl fermions (Stacked on #1404) - #1415
Draft
jstoobysmith wants to merge 119 commits into
Draft
feat: Effective potential for Weyl fermions (Stacked on #1404)#1415jstoobysmith wants to merge 119 commits into
jstoobysmith wants to merge 119 commits into
Conversation
Prompt: I want you to: 1. Fill out the sorries in this file. 2. Define a instance of a `Star` on `potentialAlgebra` defined by conjugating Left and Right weyl fermions, and using CliffordAlgebra.reverse 3. Define a representation of the Lorentz group on potentialAlgebra. 4. Define the majorana mass for a LeftHandedWeyl. 5. Show it is Lorentz invariant. Co-Authored-By: Claude <claude@users.noreply.github.com>
Your definition of majoranaMass is wrong. In particular it does not even take in a fermion as an argument. I wouldn't not define leftBilinear as it does not make any sense - again also no fermions there. > Really you should be using contractions. and the dual maps 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>
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 |
jstoobysmith
changed the title
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
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>
Left Claude running overnight Co-Authored-By: Claude <claude@users.noreply.github.com>
claude prompt: /goal I want you to clean up the files in the ./QED/JetAlgebra directory. I want you to make sure: 1. All lemmas and results sit in a sensible place (following the usual API conventions of Physlib/Mathlib). 2. No lemmas are repeated. 3. The story is complete, and makes sense, and the documentation is not too verbose. 4. Everything builds. 5. A minimal amount of concrete definitions are made (there are lots of pointless definitions). Co-Authored-By: Claude <claude@users.noreply.github.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Adds `Physlib/Particles/QED/Photon.lean`, an experiment relating the formal
jet-algebra description of QED to the concrete electromagnetism of
`Physlib.Electromagnetism`.
The jet algebra is built directly on `ElectromagneticPotential` rather than on
the B boson: the `B` boson is the gauge boson of `U(1)_Y` before electroweak
symmetry breaking, whereas the photon is the mixed combination
`A = cos θ_W B + sin θ_W W³`, so identifying them would also drag in the
Standard Model charge normalisation `6Y`, which has no meaning for `U(1)_em`.
Accordingly the file imports only `Physlib.Electromagnetism`.
Contents:
* `JetGenerators` / `JetAlgebra` — the formal jet coordinates `∂_s A_μ`,
indexed by a multiset of directions, and the real polynomials in them.
* `fieldStrength`, `maxwellTerm` — the formal `∂_s F_{μν}` and `F_{μν} F^{μν}`.
* `gaugeAction` — the `U(1)_em` gauge action `∂_s A_μ ↦ ∂_s A_μ + ∂_s ∂_μ χ`,
parametrised by the symmetrised derivatives of the gauge function. Gauge
jets compose by addition (`gaugeAction_comp`).
* `gaugeAction_fieldStrength` — gauge invariance of the field strength. The
two shifts are indexed by `s + {μ} + {ν}` and `s + {ν} + {μ}`, so the proof
is exactly the commutativity of multiset addition: Clairaut's theorem is
built into the indexing rather than assumed.
* `derivMultiset`, `evalPotential` — the iterated derivative along a multiset,
in the canonical sorted order, and the evaluation of the jet algebra at a
chosen potential, sending `∂_s A_μ` to `∂_s A_μ` with the index lowered.
* `evalPotential_maxwellTerm` — the formal Maxwell term evaluates, on any
differentiable potential, to `-4 μ₀` times
`ElectromagneticPotential.kineticTerm`.
* `evalPotential_fieldStrength_gaugeTransform`,
`evalPotential_maxwellTerm_gaugeTransform` — the formal gauge invariance
matches the library's concrete `A ↦ A + ∂χ`.
The file contains no `sorry`. It is not added to `Physlib.lean`, matching the
rest of `Physlib/Particles/QED/`.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
claude Fable was used to help proof some results. All other content was, in the end, human written. I did experiment with getting claude to write things initially, but these were reverted.
This adds the effective potential for a left-handed Weyl fermion written as an element of the suitable Exterior algebra. It also proves the general form of an effective potential which is invariant under the Lorentz group, this is related to the Majorana mass.