Skip to the content.

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

Sorryful result

(file : ClassicalMechanics.HarmonicOscillator.force)

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

See on GitHub Tag: ClassicalMechanics.HarmonicOscillator.force

Sorryful result

(file : ClassicalMechanics.HarmonicOscillator.force_is_linear)

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

See on GitHub Tag: ClassicalMechanics.HarmonicOscillator.force_is_linear

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.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 5 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.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 4 TODO items:

Sorryful result

(file : divergence_smul)

See on GitHub Tag: divergence_smul

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

Sorryful result

(file : fundamental_theorem_of_variational_calculus')

The assumption IsTestFunction f in fundamental_theorem_of_variational_calculus can be weakened to Continuous f.

The proof is by contradiction, assume that there is x₀ such that f x₀ then you can easily construct g test function with support on the neighborhood of x₀ such that ⟪f x, g x⟫ ≥ 0.

See on GitHub Tag: fundamental_theorem_of_variational_calculus'

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

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

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

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.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 4 TODO items:

TODO Item

(file : PhysLean.QuantumMechanics.FiniteTarget.Basic)

Make FiniteTarget basis independent, i.e. use a linear map for the hamiltonian instead of a matrix.

See on GitHub Tag: FXH5S

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

TODO Item

(file : PhysLean.QuantumMechanics.OneDimension.Operators.Momentum)

Make API connecting the momentumOperator to momentumOperatorLinearPMap for one-dimensional QM.

See on GitHub Tag: GPZWI

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

Sorryful result

(file : CanonicalEnsemble.partitionFunction_nsmul)

The partition function of n copies of a canonical ensemble.

See on GitHub Tag: CanonicalEnsemble.partitionFunction_nsmul

Sorryful result

(file : CanonicalEnsemble.probability_le_one)

Probability of a microstate in a canonical ensemble is less then or equal to 1.

See on GitHub Tag: CanonicalEnsemble.probability_le_one

Sorryful result

(file : CanonicalEnsemble.probability_nonneg)

Probability of a microstate in a canonical ensemble is non-negative.

See on GitHub Tag: CanonicalEnsemble.probability_nonneg

Sorryful result

(file : CanonicalEnsemble.probability_nsmul)

The probability of a microstate in n copies of a canonical ensemble is equal to the product of the probability of the corresponding individual microstates.

See on GitHub Tag: CanonicalEnsemble.probability_nsmul

Sorryful result

(file : CanonicalEnsemble.meanEnergy_nsmul)

The mean energy of n copies of a canonical ensemble is equal to n times the mean energy of the canonical ensemble.

Note, can’t make this SMul since the target type depends on the value of n.

See on GitHub Tag: CanonicalEnsemble.meanEnergy_nsmul

Sorryful result

(file : CanonicalEnsemble.entropy_nsmul)

The entropy of n copies of a canonical ensemble is equal to n times the entropy of the canonical ensemble.

See on GitHub Tag: CanonicalEnsemble.entropy_nsmul

Sorryful result

(file : CanonicalEnsemble.helmholtzFreeEnergy_nsmul)

The free energy of n copies of a canonical ensemble is equal to n times the entropy of the canonical ensemble.

See on GitHub Tag: CanonicalEnsemble.helmholtzFreeEnergy_nsmul

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

TODO Item

(file : PhysLean.StatisticalMechanics.Temperature)

Define the function from Temperature to which gives the temperature in Kelvin, based on axiomized constants.

See on GitHub Tag: EQTKM

Thermodynamics 🔥

Hide 0 TODO items:

Other ❓

Hide 3 TODO items:

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