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

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

Sorryful result

(file : ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectories_unique)

See on GitHub Tag: ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectories_unique

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

Informal definition

(RigidBody.coordinate_system)

One can describe the motion of rigid body with a fixed (inertial) coordinate system (X,Y,Z) and a moving system (x₁,x₂,x₃) rigidly attached to the body.

See on GitHub Tag: LL31.3

Informal Lemma

(RigidBody.rigid_body_dof)

A rigid body in three-dimensional space has six degrees of freedom: three translational (for the position of its centre of mass) and three rotational (for its orientation).

See on GitHub Tag: LL32-6DF

Informal Lemma

(RigidBody.velocity_decomposition)

The velocity v of any point in a rigid body is v = V + Ω × r, where V is the velocity of the origin of the moving system and Ω is the angular velocity.

See on GitHub Tag: LL31.L3

Informal Lemma

(RigidBody.angular_velocity_is_well_defined)

The angular velocity of rotation of a rigid body from a system of coordinates fixed in the body is independent of the system chosen.

See on GitHub Tag: LL32-AM

Informal Lemma

(RigidBody.decomposition_of_motion)

The motion of a rigid body can be decomposed into a translation of some reference point plus a rotation about that point. There exists a time-dependent vector V(t) and angular velocity ω(t) such that v(r) = V + ω × r, where r is measured from the reference point.

See on GitHub Tag: LL32-DM

Informal Lemma

(RigidBody.center_of_mass_point_moves_as_particle)

The centre of mass of a rigid body moves as if all mass were concentrated at that point and acted upon by the resultant external force: M a_CM = ∑ F_ext.

See on GitHub Tag: LL32-CM

Informal Lemma

(RigidBody.angular_momentum_about_point)

The total angular momentum about a point O is L = ∫ r × v dm. With v = V + ω × r about the centre of mass, L = R × (M V) + I_CM ω, where R is the centre of mass position.

See on GitHub Tag: LL32-L

Informal Lemma

(RigidBody.translational_equation_inertial)

In the inertial frame, the translational equation of motion of a rigid body is given by dP/dt = F, where P is the total linear momentum and F is the total external force acting on the body.

See on GitHub Tag: LL32-TR

Informal Lemma

(RigidBody.rotational_equation_inertial)

In the inertial frame, the rotational equation of motion of a rigid body about the center of mass is given by dM/dt = K, where M is the total angular momentum and K is the total external torque.

See on GitHub Tag: LL32-ROT

Informal Lemma

(RigidBody.kinetic_energy_decomposition)

The kinetic energy decomposes into translational and rotational parts: T = (1/2) M |V|² + (1/2) ω ⋅ I_CM ω. Here V is the velocity of the centre of mass and I_CM is the inertia tensor about that point.

See on GitHub Tag: LL32-TK

Informal Lemma

(RigidBody.parallel_axis_theorem)

If I_O is the inertia tensor about a point O, then the inertia tensor about a parallel point O’ displaced by a is I_{O’} = I_O + M(|a|² 1 − a ⊗ a). This is the parallel-axis theorem.

See on GitHub Tag: LL32-PA

Informal definition

(RigidBody.principal_axes_of_inertia)

Because the inertia tensor is real symmetric, there exists an orthonormal basis of principal axes in which it is diagonal. The corresponding directions are the principal axes of inertia.

See on GitHub Tag: LL32-PAE

Informal Lemma

(RigidBody.principal_axes_of_inertia_bound)

None of the principal moments of inertia can exceed the sum of other two.

See on GitHub Tag: LL32-PAEB

Informal definition

(RigidBody.asymmetrical_top)

An asymmetrical top is when none of the principal moments of inertia are equal.

See on GitHub Tag: LL32-AST

Informal definition

(RigidBody.symmetrical_top)

A symmetrical top is when only two of the principal moments of inertia are equal.

See on GitHub Tag: LL32-ST

Informal definition

(RigidBody.spherical_top)

A spherical top is when all three of the principal moments of inertia are equal.

See on GitHub Tag: LL32-SPT

Informal definition

(RigidBody.RotatingFrame)

A rotating body-fixed frame is a coordinate system attached to the body that rotates with the body relative to an inertial (fixed) frame. The frame is characterised by its angular velocity vector Ω(t).

See on GitHub Tag: LL32-RF

Informal definition

(RigidBody.rotating_frame_derivative)

The time derivative in the rotating frame, d’/dt, is the derivative of the components of a vector with respect to time when expressed in the rotating (body-fixed) frame.

See on GitHub Tag: LL32-dprime

Informal Lemma

(RigidBody.transport_law_inertial_rotating)

For any vector field A(t), its inertial-frame time derivative equals the rotating-frame derivative plus the contribution from the frame rotation: (dA/dt)_inertial = (dA/dt)_rotating + Ω × A. Here Ω is the angular velocity of the rotating frame.

See on GitHub Tag: LL36-Ltransport

Informal Lemma

(RigidBody.transport_law_for_momentum)

For linear momentum, the relation between inertial and rotating derivatives is (dP/dt)_inertial = d’P/dt + Ω × P. So, d’P/dt + Ω × P = F which is the linear-momentum equation in the rotating frame.

See on GitHub Tag: LL32-transportP

Informal Lemma

(RigidBody.transport_law_for_angular_momentum)

For angular momentum, the relation between inertial and rotating derivatives is (dM/dt)_inertial = d’M/dt + Ω × M, and with the rotational form of Newton’s law M_tot = (dM/dt)_inertial this yields d’M/dt + Ω × M = K, the angular-momentum equation in the rotating frame.

See on GitHub Tag: LL32-transportM

Informal Lemma

(RigidBody.euler_equations)

When motion is described in body-fixed principal axes (I₁, I₂, I₃ diagonal), the equations of rotational motion (Euler’s equations) are: I₁ dω₁/dt + (I₃ − I₂) ω₂ ω₃ = M₁, with cyclic permutations. M is the external torque about the centre of mass.

See on GitHub Tag: LL32-EQ

Informal Lemma

(RigidBody.steady_rotation_conditions)

A rigid body can perform steady (uniform) rotation about any principal axis if the torque about that axis vanishes. Stability depends on the ordering of principal moments.

See on GitHub Tag: LL32-SR

Informal Lemma

(RigidBody.intermediate_axis_instability)

Rotations about the largest and smallest principal axes are stable under small perturbations; rotation about the intermediate axis is unstable (tennis-racket effect).

See on GitHub Tag: LL32-IAI

Informal Lemma

(RigidBody.reduction_to_two_body)

If a rigid body is confined to planar motion, its dynamics reduce to a two-dimensional problem: the inertia reduces to a scalar moment and rotation is described by a single angular velocity.

See on GitHub Tag: LL32-RTB

Informal Lemma

(RigidBody.rigid_body_work_and_power)

The power delivered to a rigid body by forces is P = ∑ Fᵢ ⋅ vᵢ = F_tot ⋅ V + M ⋅ ω, where F_tot is total force, V the reference point velocity, and M the torque. Translational and rotational contributions separate.

See on GitHub Tag: LL32-WP

Informal Lemma

(RigidBody.small_oscillations_about_equilibrium)

Small oscillations about a stable equilibrium orientation are governed by linearised equations obtained by expanding energy to second order in angular displacements. Normal modes and frequencies depend on inertia and restoring torques.

See on GitHub Tag: LL32-SO

Sorryful result

(file : RigidBody.solidSphere_inertiaTensor)

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

Sorryful result

(file : CondensedMatter.TightBindingChain.hamiltonian_hermitian)

See on GitHub Tag: CondensedMatter.TightBindingChain.hamiltonian_hermitian

Sorryful result

(file : CondensedMatter.TightBindingChain.energyEigenstate_orthogonal)

See on GitHub Tag: CondensedMatter.TightBindingChain.energyEigenstate_orthogonal

Cosmology 🌌

Hide 8 TODO items:

Sorryful result

(file : Cosmology.SpatialGeometry.tendsto_sinh_rx_over_x)

See on GitHub Tag: Cosmology.SpatialGeometry.tendsto_sinh_rx_over_x

Sorryful result

(file : Cosmology.SpatialGeometry.limit_S_saddle)

See on GitHub Tag: Cosmology.SpatialGeometry.limit_S_saddle

Sorryful result

(file : Cosmology.SpatialGeometry.tendsto_sin_rx_over_x)

See on GitHub Tag: Cosmology.SpatialGeometry.tendsto_sin_rx_over_x

Sorryful result

(file : Cosmology.SpatialGeometry.limit_S_sphere)

See on GitHub Tag: Cosmology.SpatialGeometry.limit_S_sphere

Sorryful result

(file : Cosmology.FLRW)

See on GitHub Tag: Cosmology.FLRW

Informal Lemma

(Cosmology.FLRW.FriedmannEquation.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.FriedmannEquation.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.FriedmannEquation.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 4 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 arbitrary space dimensions. This may involve generalizing the curl operator to arbitrary dimensions.

See on GitHub Tag: IBQW4

Informal Lemma

(Electromagnetism.ThreeDimPointParticle.electricField_rotationally_invariant)

The electrostatic field of a point particle is rotationally invariant.

See on GitHub Tag: L7NXF

Sorryful result

(file : Electromagnetism.OneDimVacuum.gaussLaw_iff)

See on GitHub Tag: Electromagnetism.OneDimVacuum.gaussLaw_iff

Mathematics ➗

Hide 3 TODO items:

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

See on GitHub Tag: StandardModel.gaugeGroupℤ₆SubGroup

Sorryful result

(file : StandardModel.GaugeGroupℤ₆)

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

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

Make HiggsBundle an associated bundle.

See on GitHub Tag: 6V2IS

TODO Item

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

Define the global gauge action on HiggsField.

See on GitHub Tag: 6V2MV

TODO Item

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

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

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.ChargeSpectrum.PhenoClosed)

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

See on GitHub Tag: JGVOQ

QFT 🌊

Hide 16 TODO items:

TODO Item

(file : PhysLean.QFT.AnomalyCancellation.Basic)

Replace ACCSystemChargesMk with ⟨n⟩ notation everywhere.

See on GitHub Tag: NCRC5

Sorryful result

(file : ACCSystemLinear.linSolsIncl_injective)

See on GitHub Tag: ACCSystemLinear.linSolsIncl_injective

Sorryful result

(file : ACCSystemQuad.quadSolsInclLinSols_injective)

See on GitHub Tag: ACCSystemQuad.quadSolsInclLinSols_injective

Sorryful result

(file : ACCSystemQuad.quadSolsIncl_injective)

See on GitHub Tag: ACCSystemQuad.quadSolsIncl_injective

Sorryful result

(file : ACCSystem.solsInclQuadSols_injective)

See on GitHub Tag: ACCSystem.solsInclQuadSols_injective

Sorryful result

(file : ACCSystem.solsInclLinSols_injective)

See on GitHub Tag: ACCSystem.solsInclLinSols_injective

Sorryful result

(file : ACCSystem.solsIncl_injective)

See on GitHub Tag: ACCSystem.solsIncl_injective

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)

See on GitHub Tag: WickContraction.Perm.isFull_of_isFull

Sorryful result

(file : WickContraction.Perm.perm_uncontractedList)

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

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 instantaneous 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 σ satisfies PermCond c c1 σ then PermCond.inv σ h satisfies 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 efficient.

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

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 arbitrary 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.DistOfFunction)

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

See on GitHub Tag: LV5RM

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