feat: Effective potential for Weyl fermions (Stacked on #1404) - #1415
Draft
jstoobysmith wants to merge 403 commits into
Draft
jstoobysmith wants to merge 403 commits into
jstoobysmith wants to merge 403 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>
…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
…auge invariant classifiers
…g the product lifts A morphism of local gauge data, `LocalGaugeData.Hom`, is a map of the jet groups and of the Lie algebras compatible with evaluation and constants, the derivatives, the adjoint action and the Maurer–Cartan form. `U1Factor.comap`, `SUFactor.comap`, `Factor.comap` and `Factors.comap` pull factors back along it, with `Hom.lieJ_iteratedDeriv`. The projections of a product are `Hom.fst`, `Hom.snd`, so the four hand-written lifts `U1Factor.inl/inr`, `SUFactor.inl/inr` and `Factor.inl/inr`, `Factors.inr` are removed and `Factors.factors` pulls back along the projections. This resolves the TODO in `Prod.lean` asking for the lifts to be moved. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…and-built SM data Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…conj_lie `JetU1.eq_scalar` joins the scalar-matrix lemmas, and the new `scalar_commutator`, `scalar_conj` and `scalarSelfAdjoint` replace the duplicated field proofs of `u1MatrixJets`. `SUAlgebraOver.conj_lie` has been unused since `MatrixJets`. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…ere it applies General results that lived in the gauge-data layer move to general files: - `Representation.prodMap` (componentwise representation of a product group) to `Mathematics/RepresentationProdMap.lean`; - the zero Lie algebra on `Unit`, previously global instances in `OfFactors.lean`, to `Mathematics/LieAlgebraUnit.lean`; - the scalar-matrix lemmas of `U1.lean` to `Mathematics/DataStructures/Matrix/Scalar.lean`, for any index type (`Matrix.star_scalar`, `map_scalar`, `scalar_smul`, `scalar_eq_conj`, `scalarSelfAdjoint`, `eq_scalar_fin_one`); the commutator lemma is replaced by Mathlib's `Matrix.scalar_commute`; - the real-scalar compatibilities `JetRing.C_real_smul`, `constantCoeff_real_smul`, `pderiv_real_smul`, previously proved separately in `U1.lean` and `SU/Basic.lean`. `specialUnitaryToUnitary` is replaced by Mathlib's `Submonoid.inclusion`, the redundant `Module.Finite` instance on `su(n)` is removed, the fields of `u1MatrixJets` become term proofs, `prod`'s `deriv_coord` becomes one line, and the `OfFactors` instance helpers get docstrings. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…hom, drop an unused import `Hom` is a notion of the structure itself, so it moves to `Basic.lean` with a docstring that says what it is compatible with. `SUFactor.u` becomes `GJ →* Matrix n n JetRing`, like `U1Factor.u` and `MatrixJets.toMatJ`, replacing the `u_one`/`u_mul` fields. `Basic.lean` no longer imports `Relativity.DerivAlgebra`, which it did not use and which pulled the tensor stack into the bottom layer; its overview now lists the coordinate fields and points to `Free`. `Factors.comap` stays recursive, with a note on why. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…by symmetrized data `evalLie_iteratedDeriv_maurerCartan_eq_of_symmetrized_eq_all` is the strong induction that was inlined in `symmetrizedMaurerCartanCoeff_injective`; the overview of `MaurerCartan.lean` now names the step and the full statement correctly. Two local copies of `Multiset.erase_cons_tail_of_mem` are replaced by it, the manual `iteratedDeriv` rewrites by `iteratedDeriv_cons_eq_comp_deriv`, and `evalLie_iteratedDeriv_adjoint` and `symmetrizedMaurerCartanCoeff_surjective` become `lemma`s. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…assifiers and rename the anti-fundamental laws
…reductions Add the shared endpoint `ReducesInvariantsTo.mem_sup_and_forall_eq_self_iff` and the eigenvalue exclusion `reducesInvariantsTo_bot_of_apply_eq_smul`, with the gauge-and-Lorentz form `ReducesInvariantsTo.mem_sup_and_gauge_lorentz_invariant_iff`. Each sector now proves a `ReducesInvariantsTo` statement (`reducesInvariantsTo_kineticSpan`, the gauge and Higgs `reducesInvariantsTo_lorentzContractionEightSpan`, `reducesInvariantsTo_sectorMassWeight_higgs_fermion_eight`), and the graded and filtered classifications join them. The torus sieve and the Lorentz centre-sign lemma are derived from the eigenvalue exclusion; the torus sieve now asks only torus invariance. Remove the unused sorry-based `sector_invariant`, the local peeling helpers, and unused gauge-stability hypotheses of Lorentz-only results; correct the weight-eight gauge span and formal-scope documentation.
…e duplicate helpers Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-authored-by: Codex (GPT-6) <noreply@openai.com>
Co-authored-by: Codex (GPT-6) <noreply@openai.com>
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.