TODO list

This TODO list is automatically created from the Lean files. It contains a number of different types of TODO items:

Classical Mechanics ⚙️

Hide 19 TODO items:

Sorryful result

(file : ClassicalMechanics.HarmonicOscillator.EquationOfMotion)

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

See on GitHub Tag: ClassicalMechanics.HarmonicOscillator.EquationOfMotion

Sorryful result

(file : ClassicalMechanics.HarmonicOscillator.equationOfMotion_iff_newtons_second_law)

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

See on GitHub Tag: ClassicalMechanics.HarmonicOscillator.equationOfMotion_iff_newtons_second_law

Sorryful result

(file : ClassicalMechanics.HarmonicOscillator.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: ClassicalMechanics.HarmonicOscillator.ExtremaOfAction

Sorryful result

(file : ClassicalMechanics.HarmonicOscillator.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: ClassicalMechanics.HarmonicOscillator.equationOfMotion_iff_extremaOfAction

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

Sorryful result

(file : ClassicalMechanics.HarmonicOscillator.sol_equationOfMotion)

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

See on GitHub Tag: ClassicalMechanics.HarmonicOscillator.sol_equationOfMotion

Sorryful result

(file : ClassicalMechanics.HarmonicOscillator.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: ClassicalMechanics.HarmonicOscillator.sol_unique

TODO Item

(file : PhysLean.ClassicalMechanics.RigidBody.Basic)

The definition of a rigid body is currently defined via linear maps from the space of smooth functions to ℝ. When possible, it should be change to continuous linear maps.

See on GitHub Tag: MEX5S

Informal definition

(RigidBody.kineticEnergy)

The kinetic energy of a rigid body.

See on GitHub Tag: MEYBM

Sorryful result

(file : RigidBody.solidSphere_centerOfMass)

The center of mass of a solid sphere located at the origin is 0.

See on GitHub Tag: RigidBody.solidSphere_centerOfMass

Sorryful result

(file : RigidBody.solidSphere_inertiaTensor)

The moment of inertia tensor of a solid sphere through its center of mass is 2/5 m R^2 * I.

See on GitHub Tag: RigidBody.solidSphere_inertiaTensor

TODO Item

(file : PhysLean.ClassicalMechanics.Scattering.RigidSphere)

Derive the scattering cross section of a perfectly rigid sphere.

See on GitHub Tag: L7OTP

TODO Item

(file : PhysLean.ClassicalMechanics.Vibrations.LinearTriatomic)

Derive the frequencies of vibaration of a symmetric linear triatomic molecule.

See on GitHub Tag: L7O4I

TODO Item

(file : PhysLean.ClassicalMechanics.WaveEquation.HarmonicWave)

Show that the wave equation is invariant under rotations and any direction s can be rotated to EuclideanSpace.single 2 1 if only one wave is concerened.

See on GitHub Tag: EGQUA

TODO Item

(file : PhysLean.ClassicalMechanics.WaveEquation.HarmonicWave)

Show that any disturbance (subject to certian conditions) can be expressed as a superposition of harmonic plane waves via Fourier integral.

See on GitHub Tag: EGU3E

Condensed Matter 🧊

Hide 3 TODO items:

TODO Item

(file : PhysLean.CondensedMatter.TightBindingChain.Basic)

Prove results related to the one-dimensional tight binding chain. This is related to the following issue/feature-request: https://github.com/HEPLean/PhysLean/issues/523

See on GitHub Tag: BBZAB

Sorryful result

(file : CondensedMatter.TightBindingChain.hamiltonian_hermitian)

The hamiltonian of the tight binding chain is hermitian.

See on GitHub Tag: CondensedMatter.TightBindingChain.hamiltonian_hermitian

Sorryful result

(file : CondensedMatter.TightBindingChain.energyEigenstate_orthogonal)

The energy eigenstates of the tight binding chain are orthogonal.

See on GitHub Tag: CondensedMatter.TightBindingChain.energyEigenstate_orthogonal

Cosmology 🌌

Hide 10 TODO items:

Sorryful result

(file : Cosmology.SpatialGeometry)

The inductive type with three constructors:

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

See on GitHub Tag: Cosmology.SpatialGeometry

Sorryful result

(file : Cosmology.SpatialGeometry.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: Cosmology.SpatialGeometry.S

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

Sorryful result

(file : Cosmology.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: Cosmology.FLRW

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 10 TODO items:

TODO Item

(file : PhysLean.Electromagnetism.Basic)

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.Electrostatics.Basic)

Generalize Faraday’s law to arbitary space dimensions. This may involve generalizing the curl operator to arbitrary dimensions.

See on GitHub Tag: IBQW4

Sorryful result

(file : Electromagnetism.OneDimPointParticle.gaussLaw_iff)

For the charge distribution of a point particle in 1-dimension, a static electric field satifies Gauss’s law if and only if it is the linear combination of the electric field electricField q ε (corresponding to the symmetric step function), plus a constant electric field.

The if direction of this result is easy to prove, whilst the only if direction is difficult.

Note: This result follows from the (as yet unproven) analgous result for the vacuum.

See on GitHub Tag: Electromagnetism.OneDimPointParticle.gaussLaw_iff

Sorryful result

(file : Electromagnetism.OneDimVacuum.gaussLaw_iff)

An electric field obey’s Gauss’s law for the vacuum in 1 dimension if and only if it is the constant electric field.

See on GitHub Tag: Electromagnetism.OneDimVacuum.gaussLaw_iff

TODO Item

(file : PhysLean.Electromagnetism.Electrostatics.ThreeDimension.InfinitePlane)

Define the charge distribution, electric potential and electric field of an infinite plane of charge, and prove Gauss’ law and Faraday’s law for it.

See on GitHub Tag: L7NZ6

Informal Lemma

(Electromagnetism.ThreeDimPointParticle.electricField_rotationally_invariant)

The electrostatic field of a point particle is rotationally invariant.

See on GitHub Tag: L7NXF

TODO Item

(file : PhysLean.Electromagnetism.FieldStrength.Basic)

Define the dual field strength.

See on GitHub Tag: 6V2OU

Sorryful result

(file : Electromagnetism.lorentzAction)

The Lorentz action on the electric and magnetic fields.

See on GitHub Tag: Electromagnetism.lorentzAction

Sorryful result

(file : Electromagnetism.toElectricMagneticField_equivariant)

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

See on GitHub Tag: Electromagnetism.toElectricMagneticField_equivariant

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 6 TODO items:

Sorryful result

(file : divergence_smul)

See on GitHub Tag: divergence_smul

TODO Item

(file : PhysLean.Mathematics.Distribution.Basic)

For distributions, prove that the derivative fderivD commutes with integrals and sums. This may require defining the integral of families of distributions although it is expected this will follow from the definition of a distribution.

See on GitHub Tag: 01-09-25-JTS

TODO Item

(file : PhysLean.Mathematics.Distribution.Function.IsDistBounded)

The proof IsDistBounded.pow needs golfing.

See on GitHub Tag: LSLHW

TODO Item

(file : PhysLean.Mathematics.Distribution.Function.OfFunction)

Add a general lemma specifying the derivative of functions from distributions.

See on GitHub Tag: LV5RM

TODO Item

(file : PhysLean.Mathematics.FDerivCurry)

Replace following helper lemmas with fun_prop after #24056 in Mathlib has gone through.

See on GitHub Tag: AZ2QN

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 50 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

Sorryful result

(file : 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

See on GitHub Tag: StandardModel.gaugeGroupℤ₆SubGroup

Sorryful result

(file : 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

See on GitHub Tag: StandardModel.GaugeGroupℤ₆

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

TODO Item

(file : PhysLean.Particles.SuperSymmetry.SU5.Charges.PhenoClosed)

Make the result viableChargesMultiset a safe definition, that is to say proof that the recursion terminates.

See on GitHub Tag: JGVOQ

QFT 🌊

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

Sorryful result

(file : WickContraction.Perm.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: WickContraction.Perm.isFull_of_isFull

Sorryful result

(file : WickContraction.Perm.perm_uncontractedList)

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

See on GitHub Tag: WickContraction.Perm.perm_uncontractedList

TODO Item

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

The implementation of pure U(1) anomaly cancellation conditions is done currently through the type ACCSystemCharges. This whole directory could be simplified by refactoring to remove ACCSystemCharges defining PureU1Charges as Fin n → ℚ directly, or this space quotiented by permutations and overall factors.

See on GitHub Tag: K3HYF

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 30 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.CliffordAlgebra)

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

See on GitHub Tag: 6VZF2

TODO Item

(file : PhysLean.Relativity.LorentzAlgebra.Basis)

Define the standard basis of the Lorentz algebra.

See on GitHub Tag: 6VZKA

TODO Item

(file : PhysLean.Relativity.LorentzGroup.Basic)

Define the Lie group structure on the Lorentz group.

See on GitHub Tag: 6VZHM

Sorryful result

(file : LorentzGroup.generalizedBoost_timeComponent_eq)

The time component of a generalised boost is equal to

1 +
    ‖u.1.timeComponent • v.1.spatialPart - v.1.timeComponent • u.1.spatialPart‖ / (1 + ⟪u.1, v.1⟫ₘ)

A proof of this result can be found at the below link: https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/Lorentz.20group/near/523249684

Note that the decleration of this semiformal result will be similar once the TODO item FXQ45 is completed.

See on GitHub Tag: LorentzGroup.generalizedBoost_timeComponent_eq

TODO Item

(file : PhysLean.Relativity.LorentzGroup.Orthochronous.Basic)

Prove topological properties of the Orthochronous Lorentz Group.

See on GitHub Tag: 6VZLO

TODO Item

(file : PhysLean.Relativity.LorentzGroup.Restricted.Basic)

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

See on GitHub Tag: 6VZNP

Semiformal result

(restricted_isConnected)

The restricted Lorentz group is connected.

See on GitHub Tag: FXNL5

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

Sorryful result

(file : realLorentzTensor.toComplex_equivariant)

The map toComplex is equivariant.

See on GitHub Tag: realLorentzTensor.toComplex_equivariant

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 3 TODO items:

TODO Item

(file : PhysLean.StatisticalMechanics.CanonicalEnsemble.TwoState)

Generalize the results for the two-state canonical ensemble so that the two states have arbitary energies, rather than one state having energy 0.

See on GitHub Tag: EVJNH

Informal Lemma

(CanonicalEnsemble.twoState_entropy_eq)

A simplification of the entropy of the two-state canonical ensemble.

See on GitHub Tag: EVJJI

Informal Lemma

(CanonicalEnsemble.twoState_helmholtzFreeEnergy_eq)

A simplification of the helmholtzFreeEnergy of the two-state canonical ensemble.

See on GitHub Tag: EVMPR

Thermodynamics 🔥

Hide 0 TODO items:

Other ❓

Hide 13 TODO items:

TODO Item

(file : PhysLean.SpaceAndTime.Space.Basic)

In the above documentation describe the notion of a type, and introduce the type Space d.

See on GitHub Tag: HB6RR

TODO Item

(file : PhysLean.SpaceAndTime.Space.Basic)

Convert Space from an abbrev to a def.

See on GitHub Tag: HB6VC

TODO Item

(file : PhysLean.SpaceAndTime.Space.Basic)

In the above documentation describe what an instance is, and why it is useful to have instances for Space d.

See on GitHub Tag: HB6YZ

TODO Item

(file : PhysLean.SpaceAndTime.Space.Basic)

After TODO ‘HB6VC’, give Space d the necessary instances using inferInstanceAs.

See on GitHub Tag: HB6WN

TODO Item

(file : PhysLean.SpaceAndTime.Space.Basic)

In the above documentation describe the notion of a basis in Lean.

See on GitHub Tag: HB6Z4

TODO Item

(file : PhysLean.SpaceAndTime.Space.Basic)

In the above documentation describe the different notions of a derivative in Lean.

See on GitHub Tag: HB63O

TODO Item

(file : PhysLean.SpaceAndTime.Space.LengthUnit)

For each unit of charge give the reference the literature where it’s definition is defined.

See on GitHub Tag: ITXJV

TODO Item

(file : PhysLean.SpaceAndTime.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.StringTheory.FTheory.SU5.Charges.OfRationalSection)

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

TODO Item

(file : PhysLean.Units.Basic)

Make SI : UnitChoices computable, probably by replacing the axioms defining the units. See here: https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/physical.20units/near/534914807

See on GitHub Tag: LCSAY

TODO Item

(file : PhysLean.Units.Examples)

Add an example involving derivatives.

See on GitHub Tag: LCR7N

TODO Item

(file : PhysLean.Units.WithDim.Basic)

Induce instances on WithDim d M from instances on M.

See on GitHub Tag: LPWE4