feat: Effective potential for Weyl fermions (Stacked on #1404) - #1415
Draft
jstoobysmith wants to merge 381 commits into
Draft
jstoobysmith wants to merge 381 commits into
jstoobysmith wants to merge 381 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
github-project-automation
Bot
moved this to Todo
in Physlib Higgs and Fermionic EFT Lagrangians
nateabr
moved this from Todo
to In Progress
in Physlib Higgs and Fermionic EFT Lagrangians
nateabr
reviewed
Aug 1, 2026
doxtor6
pushed a commit
to jstoobysmith/JTSphyslib
that referenced
this pull request
Aug 3, 2026
…s rep refactor Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
doxtor6
pushed a commit
to jstoobysmith/JTSphyslib
that referenced
this pull request
Aug 3, 2026
Co-Authored-By: Claude Fable 5 <noreply@anthropic.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>
Formalize quantum electrodynamics in Physlib.Particles.QED, built on the photon jet algebra of Physlib.Electromagnetism and a Dirac electron: - Basic: jet algebras of the photon (moved from LeptonGaugeSector/Photon.lean) and the Dirac electron (exterior algebra), their tensor product, the gauge jets with their commutative monoid structure, the gauge, Lorentz and mass-scaling actions, the total derivative, and the evaluation on a potential. - Fields, Lagrangian: the jet coordinates, field strength, gamma matrices, covariant derivatives, Dirac current, equations-of-motion elements and the QED Lagrangian L = -1/4 F^2 + i psibar gamma^mu D_mu psi - m psibar psi. - Theorem files (no definitions): fermion statistics, Bianchi identity, Clifford algebra and hermiticity of the gamma matrices, gauge invariance (including the monoid action law), Lorentz invariance, mass-dimension power counting, completeness of the field strength for gauge invariance, minimal coupling and Noether current conservation, and the evaluation bridges to honest electromagnetism (E and B fields, Maxwell Lagrangian, homogeneous Maxwell equations from the Bianchi identity, the action principle for the inhomogeneous Maxwell equations, and compatibility with concrete gauge and Lorentz transformations). Remaining directions are recorded as TODO items. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…et space Add the generic target space `MatterFieldData.V`, its basis `MatterFieldData.basis` (with `LorentzLabel.basisIndex`, `LorentzLabel.basis`) and the global gauge action `MatrixRep.repGlobal` of a matrix representation of jets, with `repJet_ofConstant` relating it to the jet action on constant jets when the matrices of constant jets are constant. `LeptonDoublet` is now `abbrev LeptonDoublet := Model.leptonDoublet.V`; the wrapper structure, `valEquiv`, `valLinEquiv`, `valIdx` and `jetValLinEquiv` are removed (the wrapper is kept as a comment). `basis`, `repLorentzGroup`, `repGaugeGroupI`, `repJetGaugeGroupI`, `doubletMatrix`, `weakEnd`, `actionMatrix`, `gaugeAlgebraAction`, `jetActionMatrix` and `LeptonDoublet.matterField` are one-line definitions from the datum; `basis_apply`, `repLorentzGroup_tmul`, `repGaugeGroupI_tmul`, `doubletMatrix_ofConstant_map_constantCoeff`, `doubletMatrix_ofConstant` and `weakEnd_tmul` record the explicit forms, and the basis, kernel, descent and component transformation lemmas keep their statements. `leptonDoublet_toMatterField_eq` replaces `leptonDoublet_toMatterFieldOn_eq`. The projections and inclusions of `Fermions/JetAlgebra/Basic.lean` and `IsFermionSector.derivSubmodule` become `noncomputable`, as the tensor-product instances are. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…algebra Add `GaugeFieldData.massWeightScale`, the algebra endomorphism of the local field algebra scaling each generator by `c` to its mass weight, defined through the universal property from `massWeightAssignment`; the graded pieces `massWeightSubmodule` (the common eigenspaces of eigenvalue `c ^ n`) and the filtration `massWeightSubmoduleLE`; the submodules `gaugeInvariants`, `lorentzInvariants` of elements fixed by the jet gauge group and by the Lorentz group, and `invariantsLE`, the invariants of mass weight at most `w`; and `bosonNormSq`, the contraction `φ† φ` of a bosonic species with its conjugate through a basis of its value space. With these the classification of a Lagrangian can be stated for any field datum without model-specific definitions. `FieldData.toGaugeFieldData` and `StandardModel.Model.fieldData` become abbreviations, so that the species types of the card's datum reduce where rewriting needs them. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
… card Add `Physlib/Particles/StandardModel/Challenge.lean`: the classification of the Standard Model Lagrangian in self-contained form, every notion in the statement being the card or generic. `higgsMass_mem_massWeightSubmodule` proves from the card and the generic filtration alone that the Higgs mass term `bosonNormSq H higgs.basis` has mass weight four; `invariantsLE_four`, marked `sorryful`, states the challenge at mass weight four: `fieldData.invariantsLE 4` is spanned by the constant term and the Higgs mass term. The module docstring lists the generic term constructors the statement at mass weight eight still needs. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Extend `Physlib/Particles/StandardModel/Challenge.lean` with self-contained forms of the folder's major theorems, every notion in each statement being the card or generic: `invariantsLE_seven` (no invariant of mass weight five to seven, so the invariants up to weight seven are the constant term and `H† H`); the single-sector classifications `scalarSector_invariantsLE_eight` (`1`, `H† H`, `(H† H)²`), `fermionSector_invariantsLE_eight` and `gaugeSector_invariantsLE_seven` (constants only), through the generic sector subalgebras; `repJet_ofConstant_eq_one_of_center` (a gauge transformation with components `ζ² 1₃`, `ζ³ 1₂`, `ζ` for a sixth root of unity fixes the jets of every species); and `gaugeData_free` (the gauge data of the card is free). All are marked `sorryful`; the module docstring records which results still lack the generic notions needed to state them (the full weight-eight classification, anomaly cancellation, the Higgs potential). Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…g an isomorphism Add to `GaugeFieldData` the lemmas `mem_massWeightSubmodule_apply_iff`, `massWeightSubmodule_map`, `massWeightSubmoduleLE_map`, `mem_massWeightSubmoduleLE_apply_iff`, `gaugeInvariants_map`, `lorentzInvariants_map`, `mem_invariantsLE_apply_iff` and `invariantsLE_map`: an isomorphism of the local field algebras of two field data that intertwines the jet gauge action, the Lorentz action and the mass-weight scaling carries the graded pieces, the filtration and the invariants of mass weight at most `w` of one datum onto those of the other. This is the generic half of the bridge between a model's table and a hand-built datum. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
`FieldData.toGaugeFieldData` and `StandardModel.Model.fieldData` return to being definitions rather than abbreviations: as abbreviations every unification unfolds the datum into its tensor-algebra structure, which makes rewriting on the local field algebra time out. The one proof that needed the species type to reduce, `higgsMass_mem_massWeightSubmodule`, rewrites at default transparency instead. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Add `Physlib/Particles/StandardModel/Solution.lean`. For a datum `T'` over the card's gauge data and an isomorphism `e` of local field algebras respecting the jet gauge action, the Lorentz action and the mass-weight scaling, `invariantsLE_four_iff`, `invariantsLE_seven_iff`, `scalarSector_invariantsLE_eight_iff`, `fermionSector_invariantsLE_eight_iff` and `gaugeSector_invariantsLE_seven_iff` prove that each classification challenge is equivalent to the same statement on `T'`, with the Lagrangian terms carried across by `e` (`map_eq_map_iff`, `map_one_sup_span`). `gaugeData_free_of_hand_built` proves the freeness challenge from the hand-built freeness of the local gauge data. The module docstring records the second half of the bridge, identifying the generic notions on the hand-built datum with those of the existing theorems, which waits on `JetAlgebra/SectorEquiv/Basic.lean` building again. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
The classification challenges of `Challenge.lean` are restated as the existing theorems are: an element of the mass-weight filtration fixed by every jet of gauge transformations and by every Lorentz transformation is exactly a combination of the named terms, with the sector ones adding membership of the sector subalgebra. `GaugeFieldData.invariantsLE_eq_iff` and `invariantsLE_inf_eq_iff` relate this form to the submodule `invariantsLE`, and the equivalences of `Solution.lean` are restated in the same form. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Collaborator
|
test the comment |
…efficient lifts from it
…ta/ to MatterField/ `LocalGaugeData.TransformsIn` (gauge tensors in a representation) and `LocalGaugeData.IsInfinitesimalActionOf` with the covariance of the covariant derivative are statements about a matter representation on `JetRing ⊗ V`, and they import the matter covariant derivative and the gauge-boson realizations. They now live in `MatterField/`, so that `LocalGaugeData/` no longer imports anything above it. Names and namespaces are unchanged; only the module paths and the imports of their users move. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…ta/Factor.lean The factors of a gauge group (`LocalGaugeData.U1Factor`, `SUFactor`, `Factor`, `Factors`) describe the local gauge data, not matter: their fields mention only the gauge jets, the gauge algebra and the jet ring. They move from `MatterField/MatrixRep/Factors.lean` and `MatterField/MatrixRep/Table.lean` into the new `LocalGaugeData/Factor.lean`, and `U1.lean`, `SU/Basic.lean`, `Prod.lean` and `OfFactors.lean` import that file instead of the matrix-representation layer. `MatrixRep/Factors.lean` keeps the charge twist and the fundamental representation. `StandardModel/Basic.lean` imports the table file directly, which it previously received through `OfFactors`. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
`LocalGaugeData/Prod.lean` provides it. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…OfFactors.G `Factors` was both the type of a gauge group presented by its factors, `LocalGaugeData.Factors jets`, and the namespace holding the carriers `Factors.G Γ`, `Factors.𝔤 Γ`, `Factors.G₀ Γ`, `Factors.𝔤J Γ` of the gauge data `ofFactors Γ` of a list of factor symbols. The carriers now live in the namespace `OfFactors`, named after the gauge data they carry, and `Factors.factors`, `Factors.inr` remain the only declarations in the namespace of the type. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
`SUAlgebraOver.conjMap` and its `rfl` lemma existed only to build `SUAlgebraOver.conj`. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…erive su and u1 from it `LocalGaugeData.MatrixJets κ G₀ 𝔤 GJ 𝔤J` records injective maps of the four carriers into `κ × κ` matrices of jets and what each structure map is in matrices (entrywise constant coefficient and inclusion of constants, entrywise derivative and coordinate, conjugation for the adjoint actions, `i (∂_μ U) U†` for the Maurer–Cartan form). From it, `MatrixJets.toLocalGaugeData` proves the laws of `LocalGaugeData` once, `MatrixJets.faithful` proves faithfulness, `MatrixJets.lieJ_iteratedDeriv` computes the iterated derivative entrywise, and `MatrixJets.suFactor` is the canonical `SU`-type factor. The matrix identities it needs (`mapMatrix_C_star`, `star_map_pderiv`, `map_pderiv_star_of_unitary`, `star_mcMatrix`, ...) live in the same file. `SU/Basic.lean` now supplies only the carriers, the structure maps and the Maurer–Cartan form, and defines `su n` as `(suMatrixJets n).toLocalGaugeData`; its faithfulness and canonical factor are the generic ones. `U1.lean` does the same through `u1MatrixJets`, reading a scalar as a `1 × 1` matrix. The identities `mc_cocycle`, `mc_structure`, `deriv_adjoint` and their kin are no longer proved twice. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
`evalLie_adjoint_ofConstantLie_of_eval_eq_one`, `mem_truncationKer_iff`, `eval_eq_one_of_mem_truncationKer`, `evalLie_iteratedDeriv_maurerCartan_eq_zero_of_mem_truncationKer`, `truncationKer_antitone`, `adjointCoeff_eq_one_of_mem_truncationKer`, `adjointCoeff_mul_of_mem_truncationKer_left` and `truncationProjZero_surjective` were referenced nowhere. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…tionale The recursion on the list is deliberate: a single factor keeps its own carrier and the carrier of a list unfolds to the literal product of its factors' carriers. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…rix.lean `mapMatrix_C_star`, `mapMatrix_C_smul`, `mapMatrix_constantCoeff_smul`, `star_map_pderiv`, `map_pderiv_smul`, `map_pderiv_sub`, `map_pderiv_star_of_unitary` and `star_mcMatrix` are facts about matrices of power series, not about gauge data. They move from `LocalGaugeData/MatrixJets.lean` to `Relativity/JetRing/Matrix.lean`, in the `JetRing` namespace. `MatrixJets.faithful` becomes a `lemma`. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…factor mass weight proofs
This branch has not been deployed
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
4 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.