TODO list

This file is created automatically using `TODO ...` commands within PhysLean. Feel free to tackle any of the items here.

Classical Mechanics ⚙️

Hide 13 TODO items:

Semiformal result

(force)

The force of the classical harmonic oscillator defined as - dU(x)/dx where U(x) is the potential energy.

See on GitHub Tag: 6YBYP

Semiformal result

(force_is_linear)

The force on the classical harmonic oscillator is - k x.

See on GitHub Tag: 6YB2U

Semiformal result

(EquationOfMotion)

The definition of the equation of motion for the classical harmonic oscillator defined through the Euler-Lagrange equations.

See on GitHub Tag: 6ZTP5

Semiformal result

(equationOfMotion_iff_newtons_second_law)

The equations of motion are satisfied if and only if Newton’s second law holds.

See on GitHub Tag: 6YBEI

Semiformal result

(ExtremaOfAction)

The proposition on a trajectory which is true if that trajectory is an extrema of the action.

semiformal implmentation notes:

• This is not expected to be easy to define.

See on GitHub Tag: 6YBIG

Semiformal result

(equationOfMotion_iff_extremaOfAction)

A trajectory x : ℝ → ℝ satsifies the equation of motion if and only if it is an extrema of the action.

Implementation note: This result depends on other semi-formal results which will need defining before this.

See on GitHub Tag: 6YBQH

TODO Item

(file : PhysLean.ClassicalMechanics.HarmonicOscillator.Basic)

Create a new folder for the damped harmonic oscillator, initially as a place-holder.

See on GitHub Tag: 6VZHC

TODO Item

(file : PhysLean.ClassicalMechanics.HarmonicOscillator.Solution)

Implement other initial condtions. For example:

• initial conditions at a given time.
• Two positions at different times.
• Two velocities at different times. And convert them into the type InitialConditions above (which may need generalzing a bit to make this possible).

See on GitHub Tag: 6VZME

TODO Item

(file : PhysLean.ClassicalMechanics.HarmonicOscillator.Solution)

For the classical harmonic oscillator find the time for which it returns to it’s initial position and velocity.

See on GitHub Tag: 6VZI3

TODO Item

(file : PhysLean.ClassicalMechanics.HarmonicOscillator.Solution)

For the classical harmonic oscillator find the times for which it passes through zero.

See on GitHub Tag: 6VZJB

TODO Item

(file : PhysLean.ClassicalMechanics.HarmonicOscillator.Solution)

For the classical harmonic oscillator find the velocity when it passes through zero.

See on GitHub Tag: 6VZJH

Semiformal result

(sol_equationOfMotion)

The solutions for any initial condition solve the equation of motion.

See on GitHub Tag: 6YATB

Semiformal result

(sol_unique)

The solutions to the equation of motion for a given set of initial conditions are unique.

Semiformal implmentation:

• One may needed the added condition of smoothness on x here.
• EquationOfMotion needs defining before this can be proved.

See on GitHub Tag: 6VZJO

Condensed Matter 🧊

Hide 0 TODO items:

Cosmology 🌌

Hide 10 TODO items:

Semiformal result

(SpatialGeometry)

The inductive type with three constructors:

• Spherical (k : ℝ)
• Flat
• Saddle (k : ℝ)

See on GitHub Tag: 6ZZLH

Semiformal result

(S)

For s corresponding to

• Spherical k, S s r = k * sin (r / k)
• Flat, S s r = r,
• Saddle k, S s r = k * sin (r / k).

Semiformal implementation note: There is likely a better name for this function.

See on GitHub Tag: 6ZZTV

Informal Lemma

(Cosmology.SpatialGeometry.limit_S_saddle)

The limit of S (Saddle k) r as k → ∞ is equal to S (Flat) r.

See on GitHub Tag: 6ZZ3D

Informal Lemma

(Cosmology.SpatialGeometry.limit_S_sphere)

The limit of S (Sphere k) r as k → ∞ is equal to S (Flat) r.

See on GitHub Tag: 62A4R

Semiformal result

(FLRW)

The structure FLRW is defined to contain the physical parameters of the Friedmann-Lemaître-Robertson-Walker metric. That is, it contains

• The scale factor a(t)
• An element of SpatialGeometry.

Semiformal implementation note: It is possible that we should restirct a(t) to be smooth or at least twice differentiable.

See on GitHub Tag: 6Z2AV

Informal definition

(Cosmology.FLRW.hubbleConstant)

The hubble constant defined in terms of the scale factor as (dₜ a) / a.

The notation H is used for the hubbleConstant.

Semiformal implementation note: Implement also scoped notation.

See on GitHub Tag: 6Z2NB

Informal definition

(Cosmology.FLRW.decelerationParameter)

The deceleration parameter defined in terms of the scale factor as - (dₜdₜ a) a / (dₜ a)^2.

The notation q is used for the decelerationParameter.

Semiformal implementation note: Implement also scoped notation.

See on GitHub Tag: 6Z2UE

Informal Lemma

(Cosmology.FLRW.decelerationParameter_eq_one_plus_hubbleConstant)

The deceleration parameter is equal to - (1 + (dₜ H)/H^2).

See on GitHub Tag: 6Z23H

Informal Lemma

(Cosmology.FLRW.time_evolution_hubbleConstant)

The time evolution of the hubble parameter is equal to dₜ H = - H^2 (1 + q).

See on GitHub Tag: 6Z3BS

Informal Lemma

(Cosmology.FLRW.hubbleConstant_decrease_iff)

There exists a time at which the hubble constant decreases if and only if there exists a time where the deceleration parameter is less then -1.

See on GitHub Tag: 6Z3FS

Electromagnetism ⚡

Hide 5 TODO items:

TODO Item

(file : PhysLean.Electromagnetism.FieldStrength.Basic)

Define the dual field strength.

See on GitHub Tag: 6V2OU

Semiformal result

(lorentzAction)

The Lorentz action on the electric and magnetic fields.

See on GitHub Tag: 6WNUS

Semiformal result

(toElectricMagneticField_equivariant)

The equivalence toElectricMagneticField is equivariant with respect to the group action.

(In this semiformal result lorentzActionTemp should be replaced with lorentzAction.)

See on GitHub Tag: 6V2O4

TODO Item

(file : PhysLean.Electromagnetism.MaxwellEquations)

Charge density and current density 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

See on GitHub Tag: 6V2UZ

TODO Item

(file : PhysLean.Electromagnetism.MaxwellEquations)

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

See on GitHub Tag: 6V2VD

Mathematics ➗

Hide 1 TODO items:

TODO Item

(file : PhysLean.Mathematics.LinearMaps)

Replace the definitions in this file with Mathlib definitions.

See on GitHub Tag: 6VZLZ

Meta 🏛️

Hide 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.

See on GitHub Tag: 6VZEW

Optics 🔍

Hide 0 TODO items:

Particles 💥

Hide 49 TODO items:

Informal definition

(GeorgiGlashow.GaugeGroupI)

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

See on GitHub Tag: 6V2WM

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

See on GitHub Tag: 6V2WS

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

See on GitHub Tag: 6V2W2

Informal definition

(GeorgiGlashow.embedSMℤ₆)

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

See on GitHub Tag: 6V2XA

Informal definition

(PatiSalam.GaugeGroupI)

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

See on GitHub Tag: 6V2Q2

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

See on GitHub Tag: 6V2RH

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

See on GitHub Tag: 6V2RQ

Informal definition

(PatiSalam.embedSMℤ₃)

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

See on GitHub Tag: 6V2RY

Informal definition

(PatiSalam.gaugeGroupISpinEquiv)

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

See on GitHub Tag: 6V2R7

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

See on GitHub Tag: 6V2SG

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

See on GitHub Tag: 6V2SM

Informal Lemma

(PatiSalam.sm_ℤ₆_factor_through_gaugeGroupℤ₂SubGroup)

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

See on GitHub Tag: 6V2SV

Informal definition

(PatiSalam.embedSMℤ₆Toℤ₂)

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

See on GitHub Tag: 6V2S4

TODO Item

(file : PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.DimSevenPlane)

Remove the definitions of elements (SM 3).Charges B₀, B₁ etc, here are use only B : Fin 7 → (SM 3).Charges.

See on GitHub Tag: 7SQUT

Informal definition

(Spin10Model.GaugeGroupI)

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

See on GitHub Tag: 6V2X7

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

See on GitHub Tag: 6V2YG

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

See on GitHub Tag: 6V2YO

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.

See on GitHub Tag: 6V2YU

Informal definition

(Spin10Model.inclSMThruGeorgiGlashow)

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

See on GitHub Tag: 6V2YZ

Informal Lemma

(Spin10Model.inclSM_eq_inclSMThruGeorgiGlashow)

The inclusion inclSM is equal to the inclusion inclSMThruGeorgiGlashow.

See on GitHub Tag: 6V2Y6

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.

See on GitHub Tag: 6V2TZ

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.

See on GitHub Tag: 6V2UD

Informal Lemma

(TwoHDM.prodMatrix_invariant)

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

See on GitHub Tag: 6V2VS

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

See on GitHub Tag: 6V2V2

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 ℤ₆.

See on GitHub Tag: 6V2FP

Semiformal result

(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

See on GitHub Tag: 6V2FZ

Semiformal result

(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

See on GitHub Tag: 6V2GA

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

See on GitHub Tag: 6V2GH

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

See on GitHub Tag: 6V2GO

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

See on GitHub Tag: 6V2GV

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

See on GitHub Tag: 6V2G3

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

See on GitHub Tag: 6V2HF

Informal Lemma

(StandardModel.gaugeGroupI_lie)

The gauge group GaugeGroupI is a Lie group.

See on GitHub Tag: 6V2HL

Informal Lemma

(StandardModel.gaugeGroup_lie)

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

See on GitHub Tag: 6V2HR

Informal definition

(StandardModel.gaugeBundleI)

The trivial principal bundle over SpaceTime with structure group GaugeGroupI.

See on GitHub Tag: 6V2HX

Informal definition

(StandardModel.gaugeTransformI)

A global section of gaugeBundleI.

See on GitHub Tag: 6V2H5

TODO Item

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

Make HiggsBundle an associated bundle.

See on GitHub Tag: 6V2IS

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.

See on GitHub Tag: 6V2I5

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.

See on GitHub Tag: 6V2LJ

Informal Lemma

(StandardModel.HiggsVec.guage_orbit)

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

See on GitHub Tag: 6V2L2

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 θ}).

See on GitHub Tag: 6V2MD

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.

See on GitHub Tag: 6V2MO

TODO Item

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

Define the global gauge action on HiggsField.

See on GitHub Tag: 6V2MV

TODO Item

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

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

See on GitHub Tag: 6V2M3

TODO Item

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

Prove invariance of potential under global gauge action.

See on GitHub Tag: 6V2NA

Informal definition

(StandardModel.HiggsField.gaugeAction)

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

See on GitHub Tag: 6V2NP

Informal Lemma

(StandardModel.HiggsField.guage_orbit)

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

See on GitHub Tag: 6V2NX

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 = φ^† φ.

See on GitHub Tag: 6V2OC

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.

See on GitHub Tag: 6V2K5

QFT 🌊

Hide 10 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.

See on GitHub Tag: 6VZMW

TODO Item

(file : PhysLean.QFT.AnomalyCancellation.Basic)

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

See on GitHub Tag: 6VZM3

TODO Item

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

Split the following two lemmas up into smaller parts.

See on GitHub Tag: 6V2JJ

TODO Item

(file : PhysLean.QFT.PerturbationTheory.WickAlgebra.Basic)

The lemma bosonicProjF_mem_ideal has a proof which is really long. We should either 1) split it up into smaller lemmas or 2) Put more comments into the proof.

See on GitHub Tag: 7ERJ3

Semiformal result

(isFull_of_isFull)

If Perm φsΛ₁ φsΛ₂ then if φsΛ₁ is a full Wick contraction then φsΛ₂ is a full Wick contraction..

Implementation note: Please contact JTS before attempting this.

See on GitHub Tag: ABLGD

Semiformal result

(perm_uncontractedList)

If Perm φsΛ₁ φsΛ₂ then the uncontracted lists of φsΛ₁ and φsΛ₂ are permutations of each other.

Implementation note: Please contact JTS before attempting this.

See on GitHub Tag: ABJD5

TODO Item

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

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

See on GitHub Tag: 6VZO6

TODO Item

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

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

See on GitHub Tag: 6VZTB

TODO Item

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

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

See on GitHub Tag: 6VZRN

TODO Item

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

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

See on GitHub Tag: 6VZPL

Quantum Mechanics ⚛️

Hide 2 TODO items:

TODO Item

(file : PhysLean.QuantumMechanics.FiniteTarget.Basic)

Define a smooth structure on FiniteTarget.

See on GitHub Tag: 6VZGG

TODO Item

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

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

See on GitHub Tag: 6VZH3

Relativity ⏳

Hide 38 TODO items:

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.

See on GitHub Tag: 6V2PV

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.

See on GitHub Tag: 6V2P6

TODO Item

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

Define the standard basis of the Lorentz algebra.

See on GitHub Tag: 6VZKA

TODO Item

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

Define the Lie group structure on the Lorentz group.

See on GitHub Tag: 6VZHM

TODO Item

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

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

See on GitHub Tag: 6VZKM

TODO Item

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

Show that generalised boosts are in the restricted Lorentz group.

See on GitHub Tag: 6VZKU

TODO Item

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

Prove topological properties of the Orthochronous Lorentz Group.

See on GitHub Tag: 6VZLO

TODO Item

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

Add definition of the restricted Lorentz group.

See on GitHub Tag: 6VZNK

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.

See on GitHub Tag: 6VZNP

TODO Item

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

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

See on GitHub Tag: 6VZNU

Informal definition

(LorentzGroup.Restricted)

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

See on GitHub Tag: 6VZN7

TODO Item

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

Generalize the inclusion of rotations into LorentzGroup to arbitrary dimension.

See on GitHub Tag: 6VZIS

Informal Lemma

(Lorentz.SL2C.toRestrictedLorentzGroup)

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

See on GitHub Tag: 6VZP6

TODO Item

(file : PhysLean.Relativity.SL2C.Basic)

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

See on GitHub Tag: 6VZQF

TODO Item

(file : PhysLean.Relativity.SpaceTime.Basic)

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

See on GitHub Tag: 6V2DR

Informal Lemma

(SpaceTime.space_equivariant)

The function space is equivariant with respect to rotations.

See on GitHub Tag: 7MTYX

TODO Item

(file : PhysLean.Relativity.SpaceTime.CliffordAlgebra)

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

See on GitHub Tag: 6VZF2

TODO Item

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

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

See on GitHub Tag: 6V2UQ

Informal Lemma

(SpecialRelativity.InstantaneousTwinParadox.ageGap_nonneg)

In the twin paradox with instantous acceleration, Twin A is always older then Twin B.

See on GitHub Tag: 7ROVE

TODO Item

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

Do the twin paradox with a non-instantaneous acceleration. This should be done in a different module.

See on GitHub Tag: 7ROQ4

TODO Item

(file : PhysLean.Relativity.Tensors.Basic)

We want to add inv_perserve_color to Simp database, however this fires the linter simpVarHead. This should be investigated.

See on GitHub Tag: 7ESNL

TODO Item

(file : PhysLean.Relativity.Tensors.Basic)

Prove that if σ satifies PermCond c c1 σ then PermCond.inv σ h satifies PermCond c1 c (PermCond.inv σ h).

See on GitHub Tag: 6VZ3C

TODO Item

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

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

See on GitHub Tag: 6VZTR

Informal definition

(IndexNotation.OverColor.forgetLift)

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

See on GitHub Tag: 6VZWS

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]].

See on GitHub Tag: 6VZR4

Informal Lemma

(Fermion.rightHandedWeylAltEquiv_equivariant)

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

See on GitHub Tag: 6VZSG

TODO Item

(file : PhysLean.Relativity.Tensors.Contraction.Pure)

Prove lemmas relating to the commutation rules of dropPair and prodP.

See on GitHub Tag: 63B7X

TODO Item

(file : PhysLean.Relativity.Tensors.Evaluation)

Add lemmas related to the interaction of evalT and permT, prodT and contrT.

See on GitHub Tag: 6VZ6G

TODO Item

(file : PhysLean.Relativity.Tensors.Product)

Change products of tensors to use Fin.append rather then Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm.

See on GitHub Tag: 6VZ3N

TODO Item

(file : PhysLean.Relativity.Tensors.Product)

Determine in prodEquiv_symm_pure why in rw (transparency := .instances) [h1] (transparency := .instances) is needed. As a first step adding this as a comment here.

See on GitHub Tag: 6VZ3U

TODO Item

(file : PhysLean.Relativity.Tensors.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).

See on GitHub Tag: 6V2CQ

Semiformal result

(toComplex)

The semilinear map from real Lorentz tensors to complex Lorentz tensors.

Semiformal implmentation note: Probably the easist way to define this is through basis.

See on GitHub Tag: 7RJQJ

Informal Lemma

(realLorentzTensor.toComplex_injective)

The map toComplex is injective.

See on GitHub Tag: 7RKCJ

Informal Lemma

(realLorentzTensor.toComplex_equivariant)

The map toComplex is equivariant.

See on GitHub Tag: 7RKDY

Informal Lemma

(realLorentzTensor.permT_toComplex)

The map toComplex commutes with permT.

See on GitHub Tag: 7RKA6

Informal Lemma

(realLorentzTensor.prodT_toComplex)

The map toComplex commutes with prodT.

See on GitHub Tag: 7RKFF

Informal Lemma

(realLorentzTensor.contrT_toComplex)

The map toComplex commutes with contrT.

See on GitHub Tag: 7RKFR

Informal Lemma

(realLorentzTensor.evalT_toComplex)

The map toComplex commutes with evalT.

See on GitHub Tag: 7RKGK

String Theory 🧵

Hide 0 TODO items:

Statistical Mechanics 🎲

Hide 0 TODO items:

Thermodynamics 🔥

Hide 0 TODO items:

Other ❓

Hide 1 TODO items:

TODO Item

(file : PhysLean.StringTheory.FTheory.SU5U1.Charges)

The results in this file are currently stated, but not proved. They should should be proved following e.g. https://arxiv.org/pdf/1504.05593. This is a large project.

See on GitHub Tag: AETF6