feat: Effective potential for Weyl fermions (Stacked on #1404) - #1415
Draft
jstoobysmith wants to merge 270 commits into
Draft
feat: Effective potential for Weyl fermions (Stacked on #1404)#1415jstoobysmith wants to merge 270 commits into
jstoobysmith wants to merge 270 commits into
Conversation
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.
jstoobysmith
marked this pull request as draft
July 15, 2026 10:35
…T Lagrangian
Fill all eleven remaining sorries in
Physlib/Particles/PureFermionic/EFTLagrangianExclDeriv.lean:
- coeff_fermionic_selection_rule: via termOfList_zero_of_not_nodup. The
IsInvariant hypothesis is dropped: the rule holds for any potential.
- coeff_odd_selection_rule: fermion parity, via the new rep_neg_one_apply
(the special case z = -1 of the diagonal family below).
- mem_allTermsWithIrrepContent_iff: via multisetsOfCard.
- eq_sum_irrepCoeff, eq_sum_massDimCoeff: via a new generic regrouping
lemma eq_sum_fiber_coeff (decomposition of the support sum along any
classifying map with specified fibers).
- irrepCoeff_rep, irrepCoeff_rep_apply_fieldSpecification: via
rep_termOfList_eq_sum_of_toIrrep, through a shared monomial helper.
- irrepCoeff_ψ_barψ_eq_zero_of_isInvariant: no Lorentz-invariant operator
mixes ψ with barψ. Proved with the new diagonal family
diagSL (z : ℂˣ) : SL(2,ℂ) at z = 2i: the scaling factors of the four
mixed pairs are 1/4, -1, -1 and 4, all ≠ 1, so
coeff_U1_selection_rule applies. (Real diagonal elements, i.e. pure
boosts, are insufficient: they scale the off-diagonal pairs by 1.)
A TODO records that diagSL, diagSL_inv, diagSL_neg_one and twoI should
move to Physlib.Relativity.SL2C.Basic when this development is split.
Repair the mass-dimension section, which did not compile:
- allTermsWithMassDimension is now the computable multisetsOfMassDim
from the new file Physlib/Mathematics/MultisetsOfMassDim.lean
(Finset.sym enumeration bounded by ⌊m / d_min⌋, with an ℕ-scaled
decide-friendly variant and a denominator-clearing bridge lemma, as
discussed on Zulip). upperBoundNumberOfFields is superseded by
massDimCardBound.
- massDimCoeff is defined as a sum of coeff over this fixed finset, so
linearity holds by construction (removing the map_add'/map_smul'
sorries).
- decide examples: {ψ 0, ψ 1} has mass dimension 3; the quartic does not.
Also:
- fix the stale import Physlib.Particles.PureFermionic.EffectivePotential
in Physlib.lean (renamed to EFTLagrangianExclDeriv), which broke the
full-library build;
- add docstrings to all previously undocumented definitions;
- add simp evaluation lemmas so definitions stay opaque downstream
(toIrrep_ψ, toIrrep_barψ, massDimension_eq, massDimensionNat_eq,
diagSL_inv, diagSL_neg_one, diagScale_neg_one, diagScale_twoI_ψ,
diagScale_twoI_barψ) and the structural fact sum_map_massDimension.
The changes passed a ten-angle rubric review (correctness, reuse, scope,
attribution, api-design, generality, placement, naming, documentation,
proof-quality); the review's requested changes (private bound lemmas,
authors header, defeq and simp-annotation hygiene, structure comments)
are incorporated, with the SL2C placement recorded as a TODO.
Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
…ayer Adds Physlib/ClassicalFieldTheory, a self-contained generalisation of the jet-algebra machinery of the Standard Model to an arbitrary gauge group: - JetAlgebra/: jets, jet component spaces, and the `IsFieldAlgebra` typeclass unifying bosonic (symmetric) and fermionic (exterior) field algebras, with jet derivatives, Lorentz, gauge and mass-weight actions. - GaugeTheory/GaugeJet: the `GaugeJet` class of jets of a gauge group (evaluation, constants, derivative, adjoint, Maurer–Cartan form), with the Taylor–Leibniz and truncation extensions. - GaugeTheory/GaugeBoson, GaugeField, Matter: gauge bosons valued in a Lie algebra, the `IsGaugeField` transformation law, covariant derivatives, and `MatterField` bundling the data of a matter field. Supporting lemmas in Mathematics/MultisetAntidiagonal and the multiset basis of DerivAlgebraReal. Two duplicate root-namespace declarations in the old Standard Model files are dropped in favour of the generic ones. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017JtScjMeuHHQSbNfQxqhpx
…/JTSphyslib into AddPotentialAlgebra
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
3 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.