feat: Effective potential for Weyl fermions (Stacked on #1404) - #1415
Draft
jstoobysmith wants to merge 360 commits into
Draft
jstoobysmith wants to merge 360 commits into
jstoobysmith wants to merge 360 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 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>
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>
…efs with explicit instances
… the LocalGaugeCovFieldAlgebra subalgebra
… rearrange results
… a charge tuple The internal index of a row is now the product of the nontrivial SU(n) representation indices only: singlets and U(1) positions contribute no factor, and the trivial representation is dropped rather than tensored in. Charges.rep is assembled in two steps, the Kronecker product Charges.suRep over the nontrivial dimensions Charges.dims, then the U(1) twists Charges.twist. The quark row is indexed by Fin 3 × Fin 2 and the lepton row by Fin 2, matching the existing QuarkDoublet and LeptonDoublet; the consistency file checks both index types by rfl and both matrices against QuarkDoublet.jetGaugeMatrix and LeptonDoublet.doubletMatrix without reindexing. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01V7CBqQ2HL9cLsgfbfuvqNa
…auge data StandardModel.localGaugeData is now Model.gaugeData, the package that LocalGaugeData.ofFactors assembles from the factor list [.SU 3, .SU 2, .U1]. The hand-built structure literal and the hand-written faithfulness proof are kept as comments for reference; every bridging rule of section B still holds by rfl, since each field of the assembled package is definitionally the existing Standard Model construction, and faithfulness is inherited from the generic instance. Verified by rebuilding the Standard Model chain up to and including FieldData and the species files; JetAlgebra/SectorEquiv/Basic.lean fails identically on the unmodified head and is unrelated to this change. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01V7CBqQ2HL9cLsgfbfuvqNa
… the lepton doublet Regroup the table layer as agreed on Zulip: a field is its Lorentz label and its charge tuple, `MatterFieldData Γ := LorentzLabel × Charges Γ`, so that the lepton doublet reads `(.L, .singlet, .fund, -3)`; `MatterFieldData.toMatterField` compiles it to a `MatterField` (or, through an identification `e` of the target space, `toMatterFieldOn e`); the field data of a model, `FieldData Γ Fields := Fields → ℕ × MatterFieldData Γ`, compiles to a `GaugeFieldData`. The row and table types are replaced by these. The dimension functions become abbreviations so that the index of a datum reduces to its `Fin` product at reducible transparency. The Standard Model card `StandardModel/Basic.lean` now names its six fields as values and its table as the generation counts; the species counts still close by `decide`. The pilot file `Model/LeptonDoublet.lean` holds only theorems about the lepton doublet datum: it is indexed by `Fin 2`, its gauge jets and gauge algebra act by the hand-built `LeptonDoublet.doubletMatrix` and `actionMatrix`, and on the target space `LeptonDoublet` identified with its tensor-product value, the matter field the general theory derives from the datum is `LeptonDoublet.matterField` itself (`leptonDoublet_toMatterFieldOn_eq`). Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01V7CBqQ2HL9cLsgfbfuvqNa
… table's datum Define `LeptonDoublet.valIdx`, the identification of the hand-built target space with the target space of `StandardModel.Model.leptonDoublet`, and redefine along it `repLorentzGroup`, `repJetGaugeGroupI`, `doubletMatrix`, `weakEnd`, `actionMatrix`, `gaugeAlgebraAction`, `jetActionMatrix` and `LeptonDoublet.matterField` as the Lorentz action, jet action, matrix of jets, endomorphisms, action matrices and matter field the general theory derives from the datum. The hand-built definitions are kept as comments, with `repLorentzGroup_apply`, `doubletMatrix_eq`, `actionMatrix_eq`, `jetActionMatrix_eq` and `repJetGaugeGroupI_eq_doubletMatrix` recording their formulas. `isInfinitesimalActionOf`, `repCoeff_eq`, `repJetGaugeGroupI_smul`, `jetActionMatrix_map_cc_foldl`, the `weakEnd` algebra lemmas and `gaugeAlgebraAction_comm_repLorentzGroup` become the generic `MatrixRep` results; the hand-written infinitesimal-action proof and the weak-matrix derivative and equivariance identities are commented out. `Model/LeptonDoublet.lean` now records the identities, which hold by `rfl`. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@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 |
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.