TODO list

Show that the isomorphism between ElectricField d × MagneticField d and ElectricField d × MagneticField d is equivariant with respect to the Lorentz group.

TODO Item

(file : PhysLean.Electromagnetism.MaxwellEquations)

Charge density and current desnity should be generalized to signed measures, in such a way that they are still easy to work with and can be integrated with with tensor notation. See here: https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/Maxwell’s.20Equations

TODO Item

(file : PhysLean.Electromagnetism.MaxwellEquations)

Show that if the charge density is spherically symmetric, then the electric field is also spherically symmetric.

Mathematics ➗

Show 1 TODO items:

TODO Item

(file : PhysLean.Mathematics.LinearMaps)

Replace the definitions in this file with Mathlib definitions.

Meta 🏛️

Show 1 TODO items:

TODO Item

(file : PhysLean.Meta.TransverseTactics)

Find a way to free the environment env in transverseTactics. This leads to memory problems when using transverseTactics directly in loops.

Optics 🔍

Show 0 TODO items:

Particles 💥

Show 48 TODO items:

Informal definition

(GeorgiGlashow.inclSM)

The homomorphism of the Standard Model gauge group into the Georgi-Glashow gauge group, i.e., the group homomorphism SU(3) × SU(2) × U(1) → SU(5) taking (h, g, α) to blockdiag (α ^ 3 g, α ^ (-2) h).

See page 34 of https://math.ucr.edu/home/baez/guts.pdf

Informal Lemma

(GeorgiGlashow.inclSM_ker)

The kernel of the map inclSM is equal to the subgroup StandardModel.gaugeGroupℤ₆SubGroup.

See page 34 of https://math.ucr.edu/home/baez/guts.pdf

Informal definition

(GeorgiGlashow.GaugeGroupI)

The gauge group of the Georgi-Glashow model, i.e., SU(5).

Informal definition

(GeorgiGlashow.embedSMℤ₆)

The group embedding from StandardModel.GaugeGroupℤ₆ to GaugeGroupI induced by inclSM by quotienting by the kernel inclSM_ker.

Informal definition

(PatiSalam.gaugeGroupISpinEquiv)

The equivalence between GaugeGroupI and Spin(6) × Spin(4).

Informal definition

(PatiSalam.GaugeGroupℤ₂)

The gauge group of the Pati-Salam model with a ℤ₂ quotient, i.e., the quotient of GaugeGroupI by the ℤ₂-subgroup gaugeGroupℤ₂SubGroup.

See https://math.ucr.edu/home/baez/guts.pdf

Informal definition

(PatiSalam.gaugeGroupℤ₂SubGroup)

The ℤ₂-subgroup of the un-quotiented gauge group which acts trivially on all particles in the standard model, i.e., the ℤ₂-subgroup of GaugeGroupI with the non-trivial element (-1, -1, -1).

See https://math.ucr.edu/home/baez/guts.pdf

Informal definition

(PatiSalam.GaugeGroupI)

The gauge group of the Pati-Salam model (unquotiented by ℤ₂), i.e., SU(4) × SU(2) × SU(2).

Informal definition

(PatiSalam.inclSM)

The homomorphism of the Standard Model gauge group into the Pati-Salam gauge group, i.e., the group homomorphism SU(3) × SU(2) × U(1) → SU(4) × SU(2) × SU(2) taking (h, g, α) to (blockdiag (α h, α ^ (-3)), g, diag (α ^ 3, α ^(-3)).

See page 54 of https://math.ucr.edu/home/baez/guts.pdf

Informal Lemma

(PatiSalam.inclSM_ker)

The kernel of the map inclSM is equal to the subgroup StandardModel.gaugeGroupℤ₃SubGroup.

See footnote 10 of https://arxiv.org/pdf/2201.07245

Informal definition

(PatiSalam.embedSMℤ₃)

The group embedding from StandardModel.GaugeGroupℤ₃ to GaugeGroupI induced by inclSM by quotienting by the kernel inclSM_ker.

Informal Lemma

(PatiSalam.sm_ℤ₆_factor_through_gaugeGroupℤ₂SubGroup)

The group StandardModel.gaugeGroupℤ₆SubGroup under the homomorphism embedSM factors through the subgroup gaugeGroupℤ₂SubGroup.

Informal definition

(PatiSalam.embedSMℤ₆Toℤ₂)

The group homomorphism from StandardModel.GaugeGroupℤ₆ to GaugeGroupℤ₂ induced by embedSM.

Informal definition

(Spin10Model.inclGeorgiGlashow)

The inclusion of the Georgi-Glashow gauge group into Spin(10), i.e., the Lie group homomorphism from SU(n) → Spin(2n) discussed on page 46 of https://math.ucr.edu/home/baez/guts.pdf for n = 5.

Informal definition

(Spin10Model.inclSMThruGeorgiGlashow)

The inclusion of the Standard Model gauge group into Spin(10), i.e., the composition of inclGeorgiGlashow and GeorgiGlashow.inclSM.

Informal definition

(Spin10Model.inclPatiSalam)

The inclusion of the Pati-Salam gauge group into Spin(10), i.e., the lift of the embedding SO(6) × SO(4) → SO(10) to universal covers, giving a homomorphism Spin(6) × Spin(4) → Spin(10). Precomposed with the isomorphism, PatiSalam.gaugeGroupISpinEquiv, between SU(4) × SU(2) × SU(2) and Spin(6) × Spin(4).

See page 56 of https://math.ucr.edu/home/baez/guts.pdf

Informal Lemma

(Spin10Model.inclSM_eq_inclSMThruGeorgiGlashow)

The inclusion inclSM is equal to the inclusion inclSMThruGeorgiGlashow.

Informal definition

(Spin10Model.inclSM)

The inclusion of the Standard Model gauge group into Spin(10), i.e., the composition of embedPatiSalam and PatiSalam.inclSM.

See page 56 of https://math.ucr.edu/home/baez/guts.pdf

Informal definition

(Spin10Model.GaugeGroupI)

The gauge group of the Spin(10) model, i.e., the group Spin(10).

TODO Item

(file : PhysLean.Particles.BeyondTheStandardModel.TwoHDM.Basic)

Prove bounded properties of the 2HDM potential. See e.g. https://inspirehep.net/literature/201299 and https://arxiv.org/pdf/hep-ph/0605184.

TODO Item

(file : PhysLean.Particles.BeyondTheStandardModel.TwoHDM.Basic)

Within the definition of the 2HDM potential. The structure Potential should be renamed to TwoHDM and moved out of the TwoHDM namespace. Then toFun should be renamed to potential.

Informal Lemma

(TwoHDM.prodMatrix_to_higgsField)

Given any smooth map f from spacetime to 2-by-2 complex matrices landing on positive semi-definite matrices, there exist smooth Higgs fields Φ1 and Φ2 such that f is equal to prodMatrix Φ1 Φ2.

See https://arxiv.org/pdf/hep-ph/0605184

Informal Lemma

(TwoHDM.prodMatrix_invariant)

The map prodMatrix is invariant under the simultaneous action of gaugeAction on the two Higgs fields.

Informal Lemma

(StandardModel.gaugeGroup_lie)

For every q in GaugeGroupQuot the group GaugeGroup q is a Lie group.

TODO Item

(file : PhysLean.Particles.StandardModel.Basic)

Redefine the gauge group as a quotient of SU(3) x SU(2) x U(1) by a subgroup of ℤ₆.

Informal definition

(StandardModel.GaugeGroupℤ₆)

The smallest possible gauge group of the Standard Model, i.e., the quotient of GaugeGroupI by the ℤ₆-subgroup gaugeGroupℤ₆SubGroup.

See https://math.ucr.edu/home/baez/guts.pdf

Informal definition

(StandardModel.GaugeGroup)

The (global) gauge group of the Standard Model given a choice of quotient, i.e., the map from GaugeGroupQuot to Type which gives the gauge group of the Standard Model for a given choice of quotient.

See https://math.ucr.edu/home/baez/guts.pdf

Informal definition

(StandardModel.GaugeGroupℤ₃)

The gauge group of the Standard Model with a ℤ₃-quotient, i.e., the quotient of GaugeGroupI by the ℤ₃-subgroup gaugeGroupℤ₃SubGroup.

See https://math.ucr.edu/home/baez/guts.pdf

Informal Lemma

(StandardModel.gaugeGroupI_lie)

The gauge group GaugeGroupI is a Lie group.

Informal definition

(StandardModel.gaugeTransformI)

A global section of gaugeBundleI.

Informal definition

(StandardModel.gaugeBundleI)

The trivial principal bundle over SpaceTime with structure group GaugeGroupI.

Informal definition

(StandardModel.gaugeGroupℤ₂SubGroup)

The ℤ₂subgroup of the un-quotiented gauge group which acts trivially on all particles in the standard model, i.e., the ℤ₂-subgroup of GaugeGroupI derived from the ℤ₂ subgroup of gaugeGroupℤ₆SubGroup.

See https://math.ucr.edu/home/baez/guts.pdf

Informal definition

(StandardModel.gaugeGroupℤ₃SubGroup)

The ℤ₃-subgroup of the un-quotiented gauge group which acts trivially on all particles in the standard model, i.e., the ℤ₃-subgroup of GaugeGroupI derived from the ℤ₃ subgroup of gaugeGroupℤ₆SubGroup.

See https://math.ucr.edu/home/baez/guts.pdf

Informal definition

(StandardModel.gaugeGroupℤ₆SubGroup)

The subgroup of the un-quotiented gauge group which acts trivially on all particles in the standard model, i.e., the ℤ₆-subgroup of GaugeGroupI with elements (α^2 * I₃, α^(-3) * I₂, α), where α is a sixth complex root of unity.

See https://math.ucr.edu/home/baez/guts.pdf

Informal definition

(StandardModel.GaugeGroupℤ₂)

The gauge group of the Standard Model with a ℤ₂ quotient, i.e., the quotient of GaugeGroupI by the ℤ₂-subgroup gaugeGroupℤ₂SubGroup.

See https://math.ucr.edu/home/baez/guts.pdf

TODO Item

(file : PhysLean.Particles.StandardModel.HiggsBoson.Basic)

Make HiggsBundle an associated bundle.

Informal Lemma

(StandardModel.HiggsField.zero_is_zero_section)

The zero Higgs field is the zero section of the Higgs bundle, i.e., the HiggsField zero defined by ofReal 0 is the constant zero-section of the bundle HiggsBundle.

TODO Item

(file : PhysLean.Particles.StandardModel.HiggsBoson.GaugeAction)

Prove invariance of potential under global gauge action.

Informal Lemma

(StandardModel.HiggsVec.guage_orbit)

There exists a g in GaugeGroupI such that rep g φ = φ' iff ‖φ‖ = ‖φ'‖.

TODO Item

(file : PhysLean.Particles.StandardModel.HiggsBoson.GaugeAction)

Prove ⟪φ1, φ2⟫_H invariant under the global gauge action. (norm_map_of_mem_unitary)

TODO Item

(file : PhysLean.Particles.StandardModel.HiggsBoson.GaugeAction)

Currently this only contains the action of the global gauge group. Generalize to include the full action of the gauge group.

TODO Item

(file : PhysLean.Particles.StandardModel.HiggsBoson.GaugeAction)

Define the global gauge action on HiggsField.

Informal definition

(StandardModel.HiggsField.gaugeAction)

The action of gaugeTransformI on HiggsField acting pointwise through HiggsVec.rep.

Informal Lemma

(StandardModel.HiggsVec.stability_group)

The subgroup of gaugeGroup := SU(3) × SU(2) × U(1) which preserves every HiggsVec by the action of StandardModel.HiggsVec.rep is given by SU(3) × ℤ₆ where ℤ₆ is the subgroup of SU(2) × U(1) with elements (α^(-3) * I₂, α) where α is a sixth root of unity.

Informal Lemma

(StandardModel.HiggsField.guage_orbit)

There exists a g in gaugeTransformI such that gaugeAction g φ = φ' iff φ(x)^† φ(x) = φ'(x)^† φ'(x).

Informal Lemma

(StandardModel.HiggsVec.stability_group_single)

The Higgs boson breaks electroweak symmetry down to the electromagnetic force, i.e., the stability group of the action of rep on ![0, Complex.ofReal ‖φ‖], for non-zero ‖φ‖, is the SU(3) × U(1) subgroup of gaugeGroup := SU(3) × SU(2) × U(1) with the embedding given by (g, e^{i θ}) ↦ (g, diag (e ^ {3 * i θ}, e ^ {- 3 * i θ}), e^{i θ}).

Informal Lemma

(StandardModel.HiggsField.gauge_orbit_surject)

For every smooth map f from SpaceTime to ℝ such that f is positive semidefinite, there exists a Higgs field φ such that f = φ^† φ.

Informal Lemma

(StandardModel.HiggsField.Potential.isBounded_iff_of_𝓵_zero)

When there is no quartic coupling, the potential is bounded iff the mass squared is non-positive, i.e., for P : Potential then P.IsBounded iff P.μ2 ≤ 0. That is to say - P.μ2 * ‖φ‖_H^2 x is bounded below iff P.μ2 ≤ 0.

QFT 🌊

Show 7 TODO items:

TODO Item

(file : PhysLean.QFT.AnomalyCancellation.Basic)

Anomaly cancellation conditions can be derived formally from the gauge group and fermionic representations using e.g. topological invariants. Include such a definition.

TODO Item

(file : PhysLean.QFT.AnomalyCancellation.Basic)

Anomaly cancellation conditions can be defined using algebraic varieties. Link such an approach to the approach here.

TODO Item

(file : PhysLean.QFT.AnomalyCancellation.PureU1.BasisLinear)

The definition of coordinateMap here may be improved by replacing Finsupp.equivFunOnFinite with Finsupp.linearEquivFunOnFinite. Investigate this.

TODO Item

(file : PhysLean.QFT.AnomalyCancellation.PureU1.Even.BasisLinear)

Replace the definition of join with a Mathlib definition, most likely Sum.elim.

TODO Item

(file : PhysLean.QFT.AnomalyCancellation.PureU1.Odd.BasisLinear)

Replace the definition of join with a Mathlib definition, most likely Sum.elim.

TODO Item

(file : PhysLean.QFT.AnomalyCancellation.PureU1.Permutations)

Remove pairSwap, and use the Mathlib defined function Equiv.swap instead.

TODO Item

(file : PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.NormalOrder)

Split the following two lemmas up into smaller parts.

Quantum Mechanics ⚛️

Show 2 TODO items:

TODO Item

(file : PhysLean.QuantumMechanics.FiniteTarget.Basic)

Define a smooth structure on FiniteTarget.

TODO Item

(file : PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Basic)

The momentum operator should be moved to a more general file.

Relativity ⏳

Show 36 TODO items:

TODO Item

(file : PhysLean.Relativity.Lorentz.Algebra.Basis)

Define the standard basis of the Lorentz algebra.

TODO Item

(file : PhysLean.Relativity.Lorentz.Bispinors.Basic)

To increase the speed of these files (vecNodeE complexLorentzTensor .up p).tensor | μ is written out expliclity. Notation should be introduced so that we can just write p | μ or similar without slowing things down. This can be done by redefining bispinors in terms of actual tensors.

Informal Lemma

(complexLorentzTensor.coBispinorUp_eq_metric_contr_coBispinorDown)

{coBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ coBispinorDown p | α' β' }ᵀ.

proof: expand coBispinorDown and use fact that metrics contract to the identity.

Informal Lemma

(complexLorentzTensor.contrBispinorUp_eq_metric_contr_contrBispinorDown)

{contrBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ contrBispinorDown p | α' β' }ᵀ.

Proof: expand contrBispinorDown and use fact that metrics contract to the identity.

TODO Item

(file : PhysLean.Relativity.Lorentz.ComplexTensor.Basic)

The lemma repDim_τ should hold for any Tensor Species not just complex Lorentz tensors.

TODO Item

(file : PhysLean.Relativity.Lorentz.ComplexTensor.Basis)

Replace basisVector in this file with TensorSpecies.tensorBasis. All of the results here should be generalized to TensorSpecies.tensorBasis.

TODO Item

(file : PhysLean.Relativity.Lorentz.Group.Basic)

Define the Lie group structure on the Lorentz group.

TODO Item

(file : PhysLean.Relativity.Lorentz.Group.Boosts.Generalized)

Show that generalised boosts are in the restricted Lorentz group.

TODO Item

(file : PhysLean.Relativity.Lorentz.Group.Boosts.Generalized)

Make toLorentz the definition of a generalised boost. This will involve refactoring this file.

TODO Item

(file : PhysLean.Relativity.Lorentz.Group.Orthochronous)

Prove topological properties of the Orthochronous Lorentz Group.

TODO Item

(file : PhysLean.Relativity.Lorentz.Group.Restricted)

Add definition of the restricted Lorentz group.

TODO Item

(file : PhysLean.Relativity.Lorentz.Group.Restricted)

Prove restricted Lorentz group equivalent to connected component of identity of the Lorentz group.

TODO Item

(file : PhysLean.Relativity.Lorentz.Group.Restricted)

Prove that every member of the restricted Lorentz group is combiniation of a boost and a rotation.

Informal definition

(LorentzGroup.Restricted)

The subgroup of the Lorentz group consisting of elements which are proper and orthochronous.

TODO Item

(file : PhysLean.Relativity.Lorentz.Group.Rotations)

Generalize the inclusion of rotations into LorentzGroup to arbitrary dimension.

TODO Item

(file : PhysLean.Relativity.Lorentz.RealTensor.Derivative)

Prove that the derivative obeys the following equivariant property with respect to the Lorentz group. For a function f : ℝT(d, cm) → ℝT(d, cn) then Λ • (∂ f (x)) = ∂ (fun x => Λ • f (Λ⁻¹ • x)) (Λ • x).

Informal Lemma

(Lorentz.SL2C.toRestrictedLorentzGroup)

The homomorphism from SL(2, ℂ) to the restricted Lorentz group.

TODO Item

(file : PhysLean.Relativity.Lorentz.SL2C.Basic)

Define homomorphism from SL(2, ℂ) to the restricted Lorentz group.

Informal Lemma

(Fermion.rightHandedWeylAltEquiv_equivariant)

The linear equivalence rightHandedWeylAltEquiv is equivariant with respect to the action of SL(2,C) on rightHandedWeyl and altRightHandedWeyl.

Informal definition

(Fermion.rightHandedWeylAltEquiv)

The linear equivalence between rightHandedWeyl and altRightHandedWeyl given by multiplying an element of rightHandedWeyl by the matrix εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]].

TODO Item

(file : PhysLean.Relativity.SpaceTime.Basic)

SpaceTime should be refactored into a structure, or similar, to prevent casting.

TODO Item

(file : PhysLean.Relativity.SpaceTime.CliffordAlgebra)

Prove algebra generated by gamma matrices is isomorphic to Clifford algebra.

TODO Item

(file : PhysLean.Relativity.Special.TwinParadox.Basic)

Find the conditions for which the age gap for the twin paradox is zero.

TODO Item

(file : PhysLean.Relativity.Tensors.OverColor.Discrete)

Find a better place for this.

TODO Item

(file : PhysLean.Relativity.Tensors.OverColor.Iso)

In equivToHomEq the tactic try {simp; decide}; try decide can probably be made more efficent.

Informal definition

(IndexNotation.OverColor.forgetLift)

The natural isomorphism between lift (C := C) ⋙ forget and Functor.id (Discrete C ⥤ Rep k G).

Informal Lemma

(TensorSpecies.contractSelfField_tensorTree)

The contraction ⟪ψ, φ⟫ₜₛ is related to the tensor tree {ψ | μ ⊗ (S.dualRepIsoDiscrete c).hom φ | μ}ᵀ.

Informal Lemma

(TensorSpecies.contractSelfField_non_degenerate)

The contraction of two vectors of the same color is non-degenerate, i.e., ⟪ψ, φ⟫ₜₛ = 0 for all φ implies ψ = 0.

Proof: the basic idea is that being degenerate contradicts the assumption of having a unit in the tensor species.

Informal Lemma

(TensorSpecies.dualRepIso_unitTensor_fst)

Acting with dualRepIso on the fst component of a unitTensor returns a metric.

Informal Lemma

(TensorSpecies.dualRepIso_metricTensor_snd)

Acting with dualRepIso on the snd component of a metricTensor returns a unitTensor.

Informal definition

(TensorSpecies.dualRepIso)

Given a i : Fin n the isomorphism between S.F.obj (OverColor.mk c) and S.F.obj (OverColor.mk (Function.update c i (S.τ (c i)))) induced by dualRepIsoDiscrete acting on the i-th component of the color.

Informal Lemma

(TensorSpecies.dualRepIso_unitTensor_snd)

Acting with dualRepIso on the snd component of a unitTensor returns a metric.

Informal Lemma

(TensorSpecies.dualRepIso_metricTensor_fst)

Acting with dualRepIso on the fst component of a metricTensor returns a unitTensor.

TODO Item

(file : PhysLean.Relativity.Tensors.Tree.Basic)

Fill in the other relationships between tensor trees and tensor basis.

Informal Lemma

(TensorTree.constVecNode_eq_vecNode)

A constVecNode has equal tensor to the vecNode with the map evaluated at 1.

Informal Lemma

(TensorTree.constTwoNode_eq_twoNode)

A constTwoNode has equal tensor to the twoNode with the map evaluated at 1.

Statistical Mechanics 🎲

Show 0 TODO items:

Thermodynamics 🔥

Show 0 TODO items:

Other ❓

Show 0 TODO items:

PhysLean: Digitalizing Physics in Lean 4

A project to digitalize results from physics into Lean 4.

TODO list

Classical Mechanics ⚙️

Condensed Matter 🧊

Cosmology 🌌

Electromagnetism ⚡

Mathematics ➗

Meta 🏛️

Optics 🔍

Particles 💥

QFT 🌊

Quantum Mechanics ⚛️

Relativity ⏳

Statistical Mechanics 🎲

Thermodynamics 🔥

Other ❓