TODO List
This TODO list is automatically created from the Lean files.
Create a new file for the geometric model which properly models the position as a configuration space and velocity as its tangent space, see the HarmonicOscillator file.
Define and prove properties of the quality factor Q.
Define and prove properties of the relaxation time τ.
Prove that the selected trajectory is the unique solution of the equation of motion with the given initial conditions.
Prove conservation of linear momentum for the free particle.
Create a new folder for the damped harmonic oscillator, initially as a place-holder.
Create a new file for the geometric model which properly models the position as a configuration space and velocity as its tangent space, then show explicitly how this coordinate model is a simplification of the geometric model. A nice reference for such an analysis is: https://web.williams.edu/Mathematics/it3/texts/var_noether.pdf
Configuration Space should be refactored to take `EuclideanSpace ℝ (Fin 1)` as its value.
The API around the configuration space should be improved to allow further development of a proper geometric model of the Harmonic Oscillator.
Implement other initial conditions for the classical harmonic oscillator. For example: - Two positions at different times. - Two velocities at different times. And convert them into the type `InitialConditions` above.
For the classical harmonic oscillator find the time for which it returns to it's initial position and velocity.
For the classical harmonic oscillator find the times for which it passes through zero.
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.
The kinetic energy of a rigid body.
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.
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).
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.
The angular velocity of rotation of a rigid body from a system of coordinates fixed in the body is independent of the system chosen.
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.
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.
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.
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.
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.
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.
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.
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.
None of the principal moments of inertia can exceed the sum of other two.
An asymmetrical top is when none of the principal moments of inertia are equal.
A symmetrical top is when only two of the principal moments of inertia are equal.
A spherical top is when all three of the principal moments of inertia are equal.
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).
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.
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.
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.
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.
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.
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.
Rotations about the largest and smallest principal axes are stable under small perturbations; rotation about the intermediate axis is unstable (tennis-racket effect).
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.
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.
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.
Derive the scattering cross section of a perfectly rigid sphere.
Derive the frequencies of vibaration of a symmetric linear triatomic molecule.
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 concerned.
Show that any disturbance (subject to certain conditions) can be expressed as a superposition of harmonic plane waves via Fourier integral.
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-Physlib/topic/Maxwell's.20Equations
Prove that the magnetic field around a circular current loop is as given in the reference https://ntrs.nasa.gov/api/citations/20140002333/downloads/20140002333.pdf.
Add a constructor for DistElectromagneticPotential from a scalar potential which is a function using an if...then...else... based on IsDistBounded.
Add a constructor for DistElectromagneticPotential from vector potentials.
Add a constructor for DistElectromagneticPotential from electric and magnetic fields.
Remove the definition `deriv` in distributional electromagnetism and replace it with `distTensorDeriv` everywhere.
Write lemmas for the various properties (e.g. the electric field) of the electromagnetic potential from the various constructors.
Define constructors for the distributional electromagnetic potential, similar to e.g. `ofScalarPotential` and `ofVectorPotential` for `ElectromagneticPotential`.
Lift the action on `ElectromagneticPotential d` to a `DistribMulAction`.
Add results related to the differentiability of the derivative of the Electromagnetic potential.
Currently the API for the field strength tensor has the definition of `fieldStrengthMatrix`. This is now unneeded, and should be replaced with `toField {A.toFieldStrength x| [μ] [ν]}ᵀ` and suitble API around that. To undertake this TODO, it is likely easier to start building the API around `toField {A.toFieldStrength x| [μ] [ν]}ᵀ` and then remove `fieldStrengthMatrix` once the API is in place.
Generalize the proof of `toFieldStrength_eq_sum_basis_eval` so that any tensor can easily be written as the sum of its components times the basis. The likely location for this is in the `Tensorial` module. The TODO item with tag: 8285454220008908699 is likely a prerequisite to this.
Add a section in this file on the evaluation of the field strength tensor's indices. I.e. equalitites related to `toField {A.toFieldStrength x| [μ] [ν]}ᵀ`.
For the electromagnetic field strength, we have lots of lemmas related to the components of the field strength tensor in terms of the basis. For example, `toTensor_toFieldStrength_basis_repr`, these should be removed. They are used downstream, so there use there should be refactored.
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.
Replace the definitions of bi-linear maps in `./Mathematics/LinaerMaps` with definitions from Mathlib.
Ensure that all the lines in QuantumInfo are below 100 characters long.
Turn the `sorryful` linter on for the QuantumInfo module.
Remove all instances of `erw` within Physlib. This usually indicates the need for better API.
Refactor: Refactor the code in the QuantumInfo module to mirror the API structure of the rest of Physlib. For example, different key data structures should have their own files or directories. Results should be organized in a general way such that they can be applied more generally.
Find a way to free the environment `env` in `transverseTactics`. This leads to memory problems when using `transverseTactics` directly in loops.
The gauge group of the Georgi-Glashow model, i.e., `SU(5)`.
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
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
The group embedding from `StandardModel.GaugeGroupℤ₆` to `GaugeGroupI` induced by `inclSM` by quotienting by the kernel `inclSM_ker`.
The gauge group of the Pati-Salam model (unquotiented by ℤ₂), i.e., `SU(4) × SU(2) × SU(2)`.
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
The kernel of the map `inclSM` is equal to the subgroup `StandardModel.gaugeGroupℤ₃SubGroup`. See footnote 10 of https://arxiv.org/pdf/2201.07245
The group embedding from `StandardModel.GaugeGroupℤ₃` to `GaugeGroupI` induced by `inclSM` by quotienting by the kernel `inclSM_ker`.
The equivalence between `GaugeGroupI` and `Spin(6) × Spin(4)`.
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
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
The group `StandardModel.gaugeGroupℤ₆SubGroup` under the homomorphism `embedSM` factors through the subgroup `gaugeGroupℤ₂SubGroup`.
The group homomorphism from `StandardModel.GaugeGroupℤ₆` to `GaugeGroupℤ₂` induced by `embedSM`.
Remove the definitions of elements `(SM 3).Charges` B₀, B₁ etc, here are use only `B : Fin 7 → (SM 3).Charges`.
The gauge group of the Spin(10) model, i.e., the group `Spin(10)`.
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
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
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`.
The inclusion of the Standard Model gauge group into Spin(10), i.e., the composition of `inclGeorgiGlashow` and `GeorgiGlashow.inclSM`.
The inclusion `inclSM` is equal to the inclusion `inclSMThruGeorgiGlashow`.
Redefine the gauge group as a quotient of SU(3) x SU(2) x U(1) by a subgroup of ℤ₆.
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
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
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
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
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
The gauge group `GaugeGroupI` is a Lie group.
For every `q` in `GaugeGroupQuot` the group `GaugeGroup q` is a Lie group.
The trivial principal bundle over SpaceTime with structure group `GaugeGroupI`.
A global section of `gaugeBundleI`.
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 θ})`.
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.
Make `HiggsBundle` an associated bundle.
Define the global gauge action on HiggsField.
Prove `⟪φ1, φ2⟫_H` invariant under the global gauge action. (norm_map_of_mem_unitary)
Prove invariance of potential under global gauge action.
The action of `gaugeTransformI` on `HiggsField` acting pointwise through `HiggsVec.rep`.
There exists a `g` in `gaugeTransformI` such that `gaugeAction g φ = φ'` iff `φ(x)^† φ(x) = φ'(x)^† φ'(x)`.
For every smooth map `f` from `SpaceTime` to `ℝ` such that `f` is positive semidefinite, there exists a Higgs field `φ` such that `f = φ^† φ`.
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`.
Make the result `viableChargesMultiset` a safe definition, that is to say proof that the recursion terminates.
Anomaly cancellation conditions can be derived formally from the gauge group and fermionic representations using e.g. topological invariants. Include such a definition.
Anomaly cancellation conditions can be defined using algebraic varieties. Link such an approach to the approach here.
Split the following two lemmas up into smaller parts.
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.
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.
The definition of `coordinateMap` here may be improved by replacing `Finsupp.equivFunOnFinite` with `Finsupp.linearEquivFunOnFinite`. Investigate this.
Incorporate normRegularizedPow into Space.Norm
Define a smooth structure on `FiniteTarget`.
To match this with the results currently in the `QuantumInfo` part of the library, we should: 1. Define `FiniteHilbertSpace` as a structure with a single entry `val`, this should take as an input a finite and decidable type `d`. Below this type is taken as default to be `Fin n`. 2. On this type we should then define the structure of an inner-product space, and a Hilbert space. 3. We could then define the notation `𝓗[d]` to denote the Hilbert space corresponding to the type `d`. 4. The results from `QuantumInfo/Finite/Braket.lean` can then be moved over to Physlib, and related to the definition of the Hilbert space here. Optional. Maybe it is worth moving these files to a directory called `States`, with the idea that it includes this definition of the Hilbert space, the definition of bras and kets, and the definition of mixed states. Maybe also parts of `./ResourceTheory/FreeState`.
`{contrBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ contrBispinorDown p | α' β' }ᵀ`. Proof: expand `contrBispinorDown` and use fact that metrics contract to the identity.
`{coBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ coBispinorDown p | α' β' }ᵀ`. proof: expand `coBispinorDown` and use fact that metrics contract to the identity.
Prove injectivity of ofCliffordAlgebra and construct the full isomorphism.
Define the Lie group structure on the Lorentz group.
Prove topological properties of the Orthochronous Lorentz Group.
Prove that every member of the restricted Lorentz group is combination of a boost and a rotation.
The restricted Lorentz group is connected.
Find the conditions for which the age gap for the twin paradox is zero.
In the twin paradox with instantaneous acceleration, Twin A is always older then Twin B.
Do the twin paradox with a non-instantaneous acceleration. This should be done in a different module.
In this file (Physlib/Relativity/Tensors/Basic.lean), write an overview of the implementation of tensors in Physlib. It should cover the main points: - the definition of a tensor species, - the meaning of color, - the tensorial instances, - other key definitions.
Refactor: Throughout the `Tensor` file system are lemmas related to `ComponentIdx`. The definition of `ComponentIdx` and the lemmas about it should be placed in it's own directory. Around `ComponentIdx`, we should build convenient API. Here `ComponentIdx` is the type of values that indices in e.g. Lorentz tensors can take.
Define the equivalence between `ComponentIdx ![c]` and `basisIdx c`. Replace Lorentz.Vector.indexEquiv and Lorentz.CoVector.indexEquiv with this more general definition.
Prove that if `σ` satisfies `PermCond c c1 σ` then `PermCond.inv σ h` satisfies `PermCond c1 c (PermCond.inv σ h)`.
The natural isomorphism between `lift (C := C) ⋙ forget` and `Functor.id (Discrete C ⥤ Rep k G)`.
The linear equivalence between `rightHandedWeyl` and `altRightHandedWeyl` given by multiplying an element of `rightHandedWeyl` by the matrix `εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]]`.
The linear equivalence `rightHandedWeylAltEquiv` is equivariant with respect to the action of `SL(2,C)` on `rightHandedWeyl` and `altRightHandedWeyl`.
docs: The files on contractions of tensors are currently lacking documentation. These should be added, mirroring good examples within Physlib.
Prove lemmas relating to the commutation rules of `dropPair` and `prodP`.
Determine a way to simplify the definition of `succSuccAbove` using predefined functions from Mathlib, but ensuring tactics such as `decide` still work.
Add lemmas related to the interaction of evalT and permT, prodT and contrT.
Split this module on Lorentz co-vectors into two: `Basic.lean` and `Tensorial.lean`. The former should contain the basic definitions and vector space structure of Lorentz co-vectors (e.g. the basis etc.). This should only depend on imports from Mathlib. The latter should contain the tensorial instance and everything which should depend on the `Tensorial` imports. A similar TODO item exists for Lorentz vectors.
Refactor: Split this module on Lorentz vectors into two: `Basic.lean` and `Tensorial.lean`. The former should contain the basic definitions and vector space structure of Lorentz vectors (e.g. the basis etc.). This should only depend on imports from Mathlib. The latter should contain the tensorial instance and everything which should depend on the `Tensorial` imports. A similar TODO item exists for Lorentz co-vectors.
Replace the definition of `TensorSpecies` with the construction from functions `TensorSpecies.ofFunctions`.
A simplification of the `entropy` of the two-state canonical ensemble.
A simplification of the `helmholtzFreeEnergy` of the two-state canonical ensemble.
Fix the manifold structure on `Space d`. In particular, we should not need to define `manifoldStructure`. Instead, we should be able to give `Space d` an instance of `IsManifold` directly.
Make the version of the derivative described through `deriv_eq_mfderiv_manifoldStructure` the definition of `deriv` and prove the equivalence with the current definition, under suitable conditions.
Generalize the statement that a div-free field is a curl to time-dependent fields.
Generalize the statement that a curl-free field is a gradient to time-dependent fields.
Add a general lemma specifying the derivative of functions from distributions.
For each unit of charge give the reference the literature where it's definition is defined.
In the above documentation describe what an instance is, and why it is useful to have instances for `Space d`.
In the above documentation describe the notion of a basis in Lean.
SpaceTime should be refactored into a structure, or similar, to prevent casting.
The function `space` is equivariant with respect to rotations.
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.
Make SI : UnitChoices computable, probably by replacing the axioms defining the units. See here: https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/physical.20units/near/534914807
Induce instances on `WithDim d M` from instances on `M`.
Improve the module doc-string of the `Qubit` file, to explain the current implementation.
Version bump
This issue is a tracker issue for bumping Physlib to new versions of Lean. The checklist below should be used to ensure that the bump is done correctly.
Basics
- Update mathlib rev in lakefile.toml.
- Update doc-gen4 rev in lakefile.toml.
- Remove the
.lakefile, e.g. on unix runrm -rf .lake. - Run
lake update. - Check
lean-toolchainupdates correctly. - Update the Lean version badge in the
README.mdfile.
Build
- Run
lake buildand fix any errors.
Scripts
- Ensure
lake exe lint_allruns without errors. - Ensure
lake exe TODO_to_yml mkFileruns without errors. - Ensure
lake exe stats mkHTMLruns without errors. - Ensure
lake exe informal mkFile mkDot mkHTMLruns without errors. - Ensure
lake exe make_tagruns without errors. - Remove the created files
rm ./docs/Informal.md; rm ./docs/InformalDot.dot; rm ./docs/InformalGraph.html; rm ./docs/Stats.html; rm ./docs/_data/TODO.yml.
Afterwards
- Create a tag for the new version.
- Put a bump notice on this thread.
Example past bumps
The current implementation of Lorentz vectors in Lean, defines some preliminary modules and representations, these include Co, Contr etc.
These can be removed and simply replaced with Vector and CoVector, with a careful seperation of definitions into the required modules. Similar for the complex case.
In ./Odd/BasisLinear and ./Even/BasisLinear, there is a poor choice of variable names splitting the two planes.
An example in the odd case is:
compared to:
There should be clearer descriptive naming around these planes. They should also be split into different file systems. The naming is tricky, but I think we should avoid something non-descriptive like plane1 etc.
It would be nice to set up a technical debt counter for Physlib, similar to that for Mathlib.
There is some discussion on this around:
Details
Key data structure
This API is not directed around a single key data structure, instead it is centred around the concept of a surface in space. For each type of surface is defined around an embedding into Space d.
Need
This API is needed for a number of reasons, common examples involve any system where distributions in space are important for example in Electromagnetism.
Requirements
For each of the following surface we require that the API has the following requirements:
- The API shall contain a map corresponding to the embedding of the surface into
Space d. - The API shall contain a measure on
Space dcorresponding to integration over the surface. - The API shall contain a proof that the above measure has tempered growth.
- The API shall contain a distribution corresponding to the surface.
- The API shall where applicable contain a proof that the surface is of measure zero.
The surfaces these apply to are:
- The spherical shell
- The line
- The solid sphere
- The spherical cylinder
- The solid cylinder
- The thin ring
- The half-plane
Example PRs
Example PRs in this direction include #942.
Corresponding file system
There is as of yet no file system for this API, but we see it sitting in ./SpaceAndTime/Space/Surfaces/
Parent APIs
#854
Details
Key data structure
The components of tensor, for example a 2-tensor $T^\mu_\nu$, the components would contain all specifications of the index.
- is defined as
ComponentIdx
Need
This is used to manipulate tensors and extract their components. It is also used with basis of tensors.
What needs doing
- The data structure
ComponentIdxand results related there to are currently spread throughout theTensorsdirectory. They should be moved into their own file system.
Requirements
- The API shall contain the combination of components based on taking the product of tensors.
- The API shall contain the restriction of components based on contraction of indices.
Corresponding file system
Currently these sit in the file system:
https://github.com/lean-phys-community/PhysLean/tree/master/PhysLean/Relativity/Tensors
Details
Key data structure
The isometry group of Euclidean space, this is the Euclidean group.
- is defined.
Need
This is needed for symmetries of Euclidean space, it contains rotations, reflections and translations.
Requirements
- The API shall contain the inclusion of the special Euclidean group.
- The API shall contain the inclusion of translations.
- The API shall contain the inclusion of rotations about each spatial point.
- The API shall contain a specification of a group element from a translation and rotation.
- The API shall contain the inclusion of the Euclidean group into the Affine group.
Corresponding file system
There is no corresponding part of PhysLean for this API yet.
References
There is some coverage of this in:
See the discussion here about the definition of the Euclidean Space:
Details
Key data structure
This is Euclidean SpaceTime. The key data structure should be a type TimeAndSpace d which is an abbreviation of Time x Space d.
- is defined.
Need
This API is needed throughout PhysLean, for example in Euclidean field theory, but also areas such as electromagnetism and classical mechanics.
Requirements
- The API shall contain isometry projections from
TimeAndSpace dtoTimeand `Space. - The API shall contain an action of the Euclidean group on
TimeAndSpace d. - The API shall contain an action of the Euclidean group on Schwartz maps with targets
TimeAndSpace d.
Corresponding file system
The corresponding file system is: https://github.com/lean-phys-community/PhysLean/tree/master/PhysLean/SpaceAndTime/TimeAndSpace
References
Specifics of the material in this section appears here:
Parent APIs
#854 #855 #940
Details
Key data structure
The API is built around the FieldConfiguration type representing tempered distributions as field configurations, combined with Euclidean spacetime and test function spaces:
FieldConfiguration := SpaceTime →d[ℝ] ℝ- tempered distributions on Euclidean spacetime 1SpaceTime := EuclideanSpace ℝ (Fin STDimension)- 4D Euclidean spacetime (must remain Euclidean for OS reconstruction)TestFunction := SchwartzMap SpaceTime ℝ- Schwartz test functionsGJGeneratingFunctional- generating functional Z[J] = ∫ exp(i⟨ω, J⟩) dμ(ω)
The axioms have been discharged here in the spacetime Hermite model.
Need
This API is needed to provide a mathematically rigorous foundation for constructive quantum field theory in PhysLean using the Osterwalder-Schrader approach. After completion, it will:
- Enable formalization of Glimm-Jaffe constructive QFT framework
- Support Schwinger functions and correlation functions via functional derivatives
- Provide basis for implementing Osterwalder-Schrader axioms
- Allow rigorous treatment of Euclidean field measures and generating functionals
- Bridge distribution theory with QFT
Requirements
Core Framework
- Preserve Euclidean
SpaceTimedefinition (essential for OS reconstruction) - Keep
STDimension := 4and related constants - Maintain
getTimeComponentandspatialPartfunctions for Euclidean space - Retain Lebesgue measure
μ := volume
Distribution Integration
- Replace
FieldConfigurationwithSpaceTime →d[ℝ] ℝnotation - Update
distributionPairingto use distribution evaluation - Integrate
Distribution.fderivDfor derivatives 2 - Ensure measurable space instance works with new type
Test Function Infrastructure
- Keep
schwartzMuloperation for complex test functions - Preserve
schwartz_comp_clmhelper function - Maintain
complex_testfunction_decomposeand associated lemmas - Keep
distributionPairingℂ_realfor complex test function pairing
Generating Functionals
- Preserve
GJGeneratingFunctionaldefinition Z[J] = ∫ exp(i⟨ω, J⟩) dμ(ω) - Keep
GJGeneratingFunctionalℂfor complex analyticity - Maintain
GJMeanfor mean field calculations
Documentation and Integration
- Add module docstring following PhysLean standards
- Document integration decisions (Euclidean vs Lorentzian)
- Add references to Osterwalder-Schrader literature
- Ensure compatibility with existing PhysLean distribution infrastructure
Corresponding file system
The API should be integrated into PhysLean's QFT module hierarchy:
PhysLean/QFT/
├── ConstructiveQFT/
│ ├── EuclideanFramework.lean # Core framework (minimal changes from user's file)
│ ├── GlimmJaffe.lean # GJ framework specifics
│ └── OsterwalderSchrader.lean # OS axioms implementation
Related existing PhysLean infrastructure:
PhysLean/Mathematics/Distribution/Basic.lean- Distribution types and derivativesPhysLean/SpaceAndTime/Space/Basic.lean- Spatial coordinates (for spatial slices)- Note:
PhysLean/SpaceAndTime/SpaceTime/Basic.leanuses Lorentzian spacetime and should NOT be used for this Euclidean framework 3
Wiki pages you might want to explore:
Citations
Details
Key data structure
The key data structure is the type corresponding to the Galilean group.
- is defined
Need
The Galilean group is used in newtonian and non-relativistic physics, it contains many of the usual transformations one may want to do on Space and Time.
Requirements
- The API shall contain an instance of a group on the type corresponding to the Galilean group.
- The API shall contain an instance of a Lie group on the type corresponding to the Galilean group.
- The API shall contain an inclusion from the group of rotations.
- The API shall contain an inclusions from the space-translation group.
- The API shall contain an inclusion from the time-translation group.
- The API shall be general for any dimension.
Corresponding file system
A file system is not currently defined for the Galilean group.
Details
Key data structure
The type corresponding to the manifold underlying time. Note that this is not the same as Time which is commonly used in physics.
- is defined
Need
This manifold is of use in topological field theory, where one does not have a metric on the world-volume. It also can be used to give a precise notion to the meaning of the time unit.
Requirements
- The API shall contain an instance of a manifold on the type
Corresponding file system
https://github.com/HEPLean/PhysLean/tree/master/PhysLean/SpaceAndTime/Time
Details
The details of this issue are not yet completed. The issue is here to track the progress of the API specified by the title. Parts of this API may already be included within the project. There are a number of things we need to specify, help in specifying these points is appreciated.
Key data structure
What is the key data structure the API is built around.
Need
Why is this API needed, after it is completed, what will it make easier or allow us to do.
Requirements
A tickbox list of the requirements of the API. This should include things which have already been done as well as things still to be worked on. Details on writing good system requirements can be found here.
Corresponding file system
https://github.com/HEPLean/PhysLean/tree/master/PhysLean/Relativity/Tensors
Parent APIs
#941
Details
The details of this issue are not yet completed. The issue is here to track the progress of the API specified by the title. Parts of this API may already be included within the project. There are a number of things we need to specify, help in specifying these points is appreciated.
Key data structure
What is the key data structure the API is built around.
Need
Why is this API needed, after it is completed, what will it make easier or allow us to do.
Requirements
A tickbox list of the requirements of the API. This should include things which have already been done as well as things still to be worked on. Details on writing good system requirements can be found here.
Corresponding file system
If it exists, the part of the PhysLean which corresponds to this API.
Parent APIs
#906
Details
The details of this issue are not yet completed. The issue is here to track the progress of the API specified by the title. Parts of this API may already be included within the project. There are a number of things we need to specify, help in specifying these points is appreciated.
Key data structure
What is the key data structure the API is built around.
Need
Why is this API needed, after it is completed, what will it make easier or allow us to do.
Requirements
A tickbox list of the requirements of the API. This should include things which have already been done as well as things still to be worked on. Details on writing good system requirements can be found here.
Corresponding file system
If it exists, the part of the PhysLean which corresponds to this API.
Parent APIs
#886
Key data structure
The key data structure shall be the input data of the damped harmonic oscillator. Namely, the mass, spring constant and damping coefficient.
- is defined
Need
The damped harmonic oscillator is a key example of a classical mechanical system, and a simple generalisation of the harmonic oscillator.
Requirements
- The API shall contain the definition of the kinetic energy.
- The API shall contain the definition of the potential energy.
- The API shall contain the definition of the lagrangian.
- The API shall contain a simplification of the variational gradient of the lagrangian to the Euler-Lagrange equations.
- The API shall contain a definition of the equation of motion of the system.
- The API shall contain a definition of the initial conditions of the damped harmonic oscillator.
- The API shall contain the definition of a trajectory of the damped harmonic oscillator.
Corresponding file system
https://github.com/HEPLean/PhysLean/tree/master/PhysLean/ClassicalMechanics/DampedHarmonicOscillator
Parent APIs
#846
Details
Key data structure
The key data structure shall be the definition of a Rigid Body specified by its mass distribution.
- is defined
Need
This API is needed to study many examples in classical mechanics, for example rigid spheres.
Requirements
- The API shall allow the calculation of the total mass of the rigid body.
- The API shall allow the calculation of the center of mass of the rigid body.
- The API shall allow the calculation of the moment of inertia of the rigid body.
- The API shall contain the definition of the angular velocity of rotation of the rigid body.
- The API shall contain the definition of the velocity of the center of mass of the rigid body.
- The API shall contain the definition of the kinetic energy of the rigid body.
- The API shall contain the definition of Euler angles for a rigid body.
Corresponding file system
https://github.com/HEPLean/PhysLean/tree/master/PhysLean/ClassicalMechanics/RigidBody
References
- Landau and Lifshitz, Mechanics, Section 32.
Parent APIs
#854 #855
The details of this issue are not yet completed. The issue is here to track the progress of the API specified by the title. Parts of this API may already be included within the project. There are a number of things we need to specify, help in specifying these points is appreciated.
Key data structure
What is the key data structure the API is built around.
Need
Why is this API needed, after it is completed, what will it make easier or allow us to do.
Requirements
A tickbox list of the requirements of the API. This should include things which have already been done as well as things still to be worked on.
Corresponding file system
If it exists, the part of the PhysLean which corresponds to this API.
Parent APIs
#861
Key data structure
The key data structure is a fluid specified by the distribution of its fluid velocity, density and pressure.
- is defined
Need
This is one of the core definitions fluid dynamics and can be used to define many other properties in this area.
Requirements
- Flow out of a volume
- Mass flux density
- Equation of continuity
- Euler's equation
- Definition of an ideal fluid
- Definition of the entropy flux density
- Bernoulli's equation
- Energy flux
Corresponding file system
This does not yet have an API in PhysLean
References
A good reference for this is
- Landau and Lifshitz, Fluid Mechanics, Chapter 1.
Parent APIs
#854 #855
The details of this issue are not yet completed. The issue is here to track the progress of the API specified by the title. Parts of this API may already be included within the project. There are a number of things we need to specify, help in specifying these points is appreciated.
Key data structure
What is the key data structure the API is built around.
Need
Why is this API needed, after it is completed, what will it make easier or allow us to do.
Requirements
A tickbox list of the requirements of the API. This should include things which have already been done as well as things still to be worked on.
Corresponding file system
If it exists, the part of the PhysLean which corresponds to this API.
Parent APIs
#885 #908
Key data structure
The key data structure here is the Lorentz group, which is the key symmetry group of Minkowski SpaceTime.
- is defined
Need
This API is needed throughout the project, we use it to define Lorentz tensors which are the foundations to the definition of SpaceTime and many other quantities in the project, such as fermions, the Electromangetic potential etc.
Requirements
- Instance as a group
- Instance as a Lie group
- Inclusion of boosts
- Inclusion of rotations
- Different membership conditions
- Definition of proper Lorentz transforms
- Definition of orthochronous Lorentz transforms
- Definition of the restricted Lorentz group
Corresponding file system
https://github.com/HEPLean/PhysLean/tree/master/PhysLean/Relativity/LorentzGroup
Key data structure
The key data structure is the configuration space of the pendulum. There are multiple ways that it could be defined, e.g. by an x and y coordinates which are constrained, or by its angle. One should be chosen.
- is defined
Need
The pendulum is a simple example of a problem in classical mechanics, this API will show the more general power of APIs around classical mechanics.
Requirements
- The API shall contain the structure of a manifold on the configuration space.
- The API shall contain a map from the configuration space to
Space, giving the position of the pendulum in real space. - The API shall contain the definition of a trajectory based on the configuration space
- The API shall subsequently contain the definition of the lagrangian
Corresponding file system
https://github.com/HEPLean/PhysLean/tree/master/PhysLean/ClassicalMechanics/Pendulum
Parent APIs
#863
Key data structure
The key data structure here is the general notation of a Feynman diagram. It is suspected that getting a good, and general definition for this data structure will be hard, but vital for the building of a good API.
- is defined
Need
Feynman diagrams are one of the main calculation tools used in particle physics. With Feynman diagrams we will be able to formalise a lot more results within particle physics than is currently possible, and slowly make our way to research level results in this direction.
Requirements
- The definition shall be general enough to accept any Feynman diagram from any theory.
- The API shall contain a definition to provably generate all Feynman diagrams up to a given order for a given amplitude.
- The API shall contain a computable definition of the symmetry factor of a Feynman diagram.
- The API shall contain a definition permitting the conversion of a Feynman diagram into its underlying algebraic expression.
Corresponding file system
There is a start to this in PhysLean, however this can likely be rewritten.
Parent APIs
#881 #885
The details of this issue are not yet completed. The issue is here to track the progress of the API specified by the title. Parts of this API may already be included within the project. There are a number of things we need to specify, help in specifying these points is appreciated.
Key data structure
What is the key data structure the API is built around.
Need
Why is this API needed, after it is completed, what will it make easier or allow us to do.
Requirements
A tickbox list of the requirements of the API. This should include things which have already been done as well as things still to be worked on.
Corresponding file system
If it exists, the part of the PhysLean which corresponds to this API.
Key data structure
The key data structure here is the collection of integer charges one can assign to the Standard Model particles. Sets of charges which are multiples of each other should be equivalent.
- is defined
Need
Z-prime models are an important yet simple extension of the standard model. They have been utilized in many phenomenological problems. Having this data structure will allow us to reason more easily about these models.
Requirements
- The API shall contain an action of the group which permutes families of particles
- The API shall contain a function returning the charges associated with different terms in the potential
- The API shall contain a function given the anomaly cancellation conditions on the charges
- The API shall contain an equivalence class on the charges by addition of hypercharge
- The API shall contain common named sets of charges
Corresponding file system
Lots of aspect of this API already exist in PhysLean, however, it is not structured around a key data structure, so needs to be rewritten. This content can be found as part of:
https://github.com/HEPLean/PhysLean/tree/master/PhysLean/Particles/StandardModel
Parent APIs
#858
The details of this issue are not yet completed. The issue is here to track the progress of the API specified by the title. Parts of this API may already be included within the project. There are a number of things we need to specify, help in specifying these points is appreciated.
Key data structure
The key data structure here is the electromagnetic potential, there are a number of ways one could define this. For example as a function or as a distribution. We need both definitions.
- is defined
Need
This API will let us solve problems in electromagnetism for example, plane waves, electrostatic problems and electrodynamics problems.
Requirements
- The API shall contain the definition of the EM potential from a connection on a U(1)-gauge bundle.
- The API shall contain the definition of the Electric field from the EM potential.
- The API shall contain the definition of the Magnetic field from the EM potential.
- The API shall contain the definition of the Kinetic term from the EM potential.
- The API shall contain the definition of the Lagrangian from the EM potential.
Corresponding file system
https://github.com/HEPLean/PhysLean/tree/master/PhysLean/Electromagnetism
Parent APIs
#885 #858
The details of this issue are not yet completed. The issue is here to track the progress of the API specified by the title. Parts of this API may already be included within the project. There are a number of things we need to specify, help in specifying these points is appreciated.
Key data structure
What is the key data structure the API is built around.
Need
Why is this API needed, after it is completed, what will it make easier or allow us to do.
Requirements
A tickbox list of the requirements of the API. This should include things which have already been done as well as things still to be worked on.
Corresponding file system
If it exists, the part of the PhysLean which corresponds to this API.
Parent APIs
#858
The details of this issue are not yet completed. The issue is here to track the progress of the API specified by the title. Parts of this API may already be included within the project. There are a number of things we need to specify, help in specifying these points is appreciated.
Key data structure
What is the key data structure the API is built around.
Need
Why is this API needed, after it is completed, what will it make easier or allow us to do.
Requirements
A tickbox list of the requirements of the API. This should include things which have already been done as well as things still to be worked on.
Corresponding file system
If it exists, the part of the PhysLean which corresponds to this API.
Parent APIs
#909
The details of this issue are not yet completed. The issue is here to track the progress of the API specified by the title. Parts of this API may already be included within the project. There are a number of things we need to specify, help in specifying these points is appreciated.
Key data structure
What is the key data structure the API is built around.
Need
Why is this API needed, after it is completed, what will it make easier or allow us to do.
Requirements
A tickbox list of the requirements of the API. This should include things which have already been done as well as things still to be worked on.
Corresponding file system
If it exists, the part of the PhysLean which corresponds to this API.
The details of this issue are not yet completed. The issue is here to track the progress of the API specified by the title. Parts of this API may already be included within the project. There are a number of things we need to specify, help in specifying these points is appreciated.
Key data structure
What is the key data structure the API is built around.
Need
Why is this API needed, after it is completed, what will it make easier or allow us to do.
Requirements
A tickbox list of the requirements of the API. This should include things which have already been done as well as things still to be worked on.
Corresponding file system
If it exists, the part of the PhysLean which corresponds to this API.
The details of this issue are not yet completed. The issue is here to track the progress of the API specified by the title. Parts of this API may already be included within the project. There are a number of things we need to specify, help in specifying these points is appreciated.
Key data structure
What is the key data structure the API is built around.
Need
Why is this API needed, after it is completed, what will it make easier or allow us to do.
Requirements
A tickbox list of the requirements of the API. This should include things which have already been done as well as things still to be worked on.
Corresponding file system
If it exists, the part of the PhysLean which corresponds to this API.
The details of this issue are not yet completed. The issue is here to track the progress of the API specified by the title. Parts of this API may already be included within the project. There are a number of things we need to specify, help in specifying these points is appreciated.
Key data structure
What is the key data structure the API is built around.
Need
Why is this API needed, after it is completed, what will it make easier or allow us to do.
Requirements
A tickbox list of the requirements of the API. This should include things which have already been done as well as things still to be worked on.
Corresponding file system
If it exists, the part of the PhysLean which corresponds to this API.
Parent APIs
#862 #861
The details of this issue are not yet completed. The issue is here to track the progress of the API specified by the title. Parts of this API may already be included within the project. There are a number of things we need to specify, help in specifying these points is appreciated.
Key data structure
What is the key data structure the API is built around.
Need
Why is this API needed, after it is completed, what will it make easier or allow us to do.
Requirements
A tickbox list of the requirements of the API. This should include things which have already been done as well as things still to be worked on.
Corresponding file system
If it exists, the part of the PhysLean which corresponds to this API.
Standard model gauge group
Key data structure
The Standard Model gauge group is actually one of a number gauge groups corresponding to a quotient of SU(3)xSU(2)xU(1) by a finite group. The key data structure should take as an input a specification of which quotient, and correspond to said group.
- Is defined
Need
The standard model gauge group is the most important groups in particle physics, and having a good API around it will open the door for lots of further results in this area.
Requirements
The following are requirements of the API:
- the instance of a group
- the instance of a Lie group
- the center of the group
- the principal bundle
- associated bundles
- common representations, and properties thereof
- the electroweak subgroup
- connection to an API around the Lie algebra
Corresponding File System
https://github.com/HEPLean/PhysLean/tree/master/PhysLean/Particles/StandardModel
Contributing to this API
This API is open to contributions from anyone. If you believe that the requirements outlined above need modification, feel free to comment here. If you make a PR which is related to this API, please link it to this issue.
Parent APIs
#859 #856
The details of this issue are not yet completed. The issue is here to track the progress of the API specified by the title. Parts of this API may already be included within the project. There are a number of things we need to specify, help in specifying these points is appreciated.
Key data structure
What is the key data structure the API is built around.
Need
Why is this API needed, after it is completed, what will it make easier or allow us to do.
Requirements
A tickbox list of the requirements of the API. This should include things which have already been done as well as things still to be worked on.
Corresponding file system
If it exists, the part of the PhysLean which corresponds to this API. .
Parent APIs
#856
Key data structure
The key data structure is SpaceTime. This represents the SpaceTime with a given but arbitrary choice of units, with a given by arbitrary choice of zero. It is the usual notion of SpaceTime used by physicists. It corresponds to Minkowski spacetime, and is used in relativity.
- is defined
Need
This API is heavily used in relativistic physics.
Requirements
- The API shall contain a map from
SpaceTimetoSpaceandTime. - The API shall contain the derivatives of functions from
SpaceTimeto a normed space. - The API shall contain the derivatives of functions from
SpaceTimeto manifolds. - The API shall contain derivatives of distributions from
SpaceTimeto normed spaces. - The API shall contain derivatives of distributions from
SpaceTimeto manifolds. - The API shall contain the splitting of integrals over
SpaceTimeto integrals overSpaceandTime. - The API shall contain an action of the Lorentz group on
SpaceTime.
Corresponding file system
https://github.com/HEPLean/PhysLean/tree/master/PhysLean/SpaceAndTime/SpaceTime
Parent APIs
#854 #855 #886
Key data structure
The key data structure is Time consisting of a real value. This represents the Time with a given but arbitrary choice of units, with a given by arbitrary choice of zero. It is the usual notion of Time used by physicists.
- is defined
Need
This API is heavily used in non-relativistic physics, specifically classical mechanics.
Requirements
- The API shall contain an instance of a vector space on Time.
- The API shall contain an ordering on Time
- The API shall contain a norm on Time.
- The API shall contain the derivatives of functions from
Timeto a normed space. - The API shall contain the derivatives of functions from
Timeto manifolds. - The API shall contain an action of the translation group on
Time. - The API shall contain derivatives of distributions from
Timeto normed spaces. - The API shall contain derivatives of distributions from
Timeto manifolds.
Corresponding file system
https://github.com/HEPLean/PhysLean/tree/master/PhysLean/SpaceAndTime/Time
Parent APIs
#909 #911
Space
Key data structure
The key data structure for the Space Api is a structure with a single value corresponding to a map from Fin n to Real. This corresponds to flat space. It acts as part of the standard world volume for many problems in physics.
- Is defined
Need
This API is one of the most heavily used in PhysLean and acts as the backbone to many other problems.
Requirements
The following are requirements of the API:
- the instance of a vector space
- basis vectors
- derivatives of functions from space to normed spaces
- derivatives of functions from space to manifolds
- the action of the group of rotations
- translations
- relation between Spaces of different dimensions
- derivatives of distributions from Space to normed spaces
- derivatives of distributions from Space to manifolds
- The API shall contain a
VSubinstance toEuclideanSpace. - The API shall contain an
NormAddTorsorinstance fromEuclideanSpace, see the conversation here.
Corresponding File System
https://github.com/HEPLean/PhysLean/tree/master/PhysLean/SpaceAndTime/Space
Contributing to this API
This API is open to contributions from anyone. If you believe that the requirements outlined above need modification, feel free to comment here. If you make a PR which is related to this API, please link it to this issue.
References
See
Parent APIs
#911
Key data structure
The key data structure shall correspond to the vector space associated with Higgs fields. It shall contain two fields, one for each of the Higgs vectors.
- is defined.
Need
The two-Higgs doublet model is a key example of a theory beyond the standard model. In is the simplest of a large collection of models called N-doublet models.
Requirements
- The API shall contain an instance of a vector space on the key-data structure.
- The API shall contain the action of the global gauge group on the two Higgs doublets.
- The API shall contain the definition of the potential of the two Higgs doublets.
- The API shall contain a theorem proving that the potential is invariant under the global gauge group.
- The API shall contain an action of the group $\mathbb{Z}_2$ swapping the two Higgs vectors.
Corresponding file system
https://github.com/HEPLean/PhysLean/tree/master/PhysLean/Particles/BeyondTheStandardModel/TwoHDM
Parent APIs
#857
The details of this issue are not yet completed. The issue is here to track the progress of the API specified by the title. Parts of this API may already be included within the project. There are a number of things we need to specify, help in specifying these points is appreciated.
Key data structure
What is the key data structure the API is built around.
Need
Why is this API needed, after it is completed, what will it make easier or allow us to do.
Requirements
A tickbox list of the requirements of the API. This should include things which have already been done as well as things still to be worked on.
Corresponding file system
If it exists, the part of the PhysLean which corresponds to this API.
Parent APIs
#885
Key data structure
The key data structure here corresponds to Hilbert space of 'square integrable functions from Space d to the complex numbers`. Really one will need the equivalence class of such functions.
- is defined
Need
This API will be used in, for example, the study of the classical harmonic oscillator, the reflectionless potential and other problems based on potentials in space.
Requirements
- The API shall contain the definition of the position operator
- The API shall contain the definition of the momentum operator
- The key data structure shall carry the instance of a Hilbert space
- The API shall contain the definition of a bra
Corresponding file system
Aspects of this API already exist, however, they are not structured neatly around the key data structure.
https://github.com/HEPLean/PhysLean/tree/master/PhysLean/QuantumMechanics/OneDimension
Parent APIs
#854
The details of this issue are not yet completed. The issue is here to track the progress of the API specified by the title. Parts of this API may already be included within the project. There are a number of things we need to specify, help in specifying these points is appreciated.
Key data structure
What is the key data structure the API is built around.
Need
Why is this API needed, after it is completed, what will it make easier or allow us to do.
Requirements
A tickbox list of the requirements of the API. This should include things which have already been done as well as things still to be worked on.
Corresponding file system
If it exists, the part of the PhysLean which corresponds to this API.
Parent APIs
#848
Finite dimensional Hilbert Space
Key data structure
The key data structure is the finite dimensional Hilbert space, which takes as an input the dimension of the Hilbert space. This is for a general system and not for any specific Hamiltonian.
- is defined
Need
Finite dimensional quantum mechanical systems are prevalent in lots of aspects of physics, including qubits in quantum information, and the Hilbert space of finite lattices. For example the tight binding chain.
Requirements
The following are requirements of the API:
- ability to easily define notation for basis vectors
- statements about the dimensions
- used in the definition of the qubit
- used in the definition of the tight binding chain
- easy conversion between bras and kets
- tensor products
- pure states
Corresponding File System
This file system exists, the link needs adding here.
Contributing to this API
This API is open to contributions from anyone. If you believe that the requirements outlined above need modification, feel free to comment here. If you make a PR which is related to this API, please link it to this issue.
Configuration space of Harmonic Oscillator
Key data structure
The key data structure of this API is the configuration space of the classical harmonic oscillator. This is a should be defined as a structure with a single value of type Real.
- Is defined
Need
Currently the classical harmonic oscillator in PhysLean is not defined using a custom defined configuration space. The problem with this is that the physics is hidden, and defining properties on the configuration space is difficult.
This API should act as a template for making other APIs.
Requirements
The following are requirements of the API:
- the structure of a smooth manifold on the configuration space
- maps from the configuration space to the actual position of the particle in Space
- Trajectories should be defined using the configuration space
- Well defined notion for trajectories, may need interaction with 5e Space API
Corresponding File System
https://github.com/HEPLean/PhysLean/tree/master/PhysLean/ClassicalMechanics/HarmonicOscillator
Parent APIs
#854 #863
As suggested by @PrParadoxy in #832, the Lorentz algebra should be derived from the Lorentz group.
- Include a TODO item in the Lorentz algebra file about this.
- Introduce the Lorentz algebra from the Lorentz group.
Version bump
- Why PhysLean decides to define finite Hilbert Space and infinite Hilbert Space separately?
- We try to define Ket as a linear map (eg. noncomputable def Ket: ℂ →ₗ[ℂ] H := (innerSL ℂ 1).toLinearMap.smulRight ψ), so that we can use the uniform notation tensor product of map (eg. f "⊗ₘ" g => TensorProduct.map f g) for calculation like this: ((⟨ψ| ⊗ₘ ⟨φ|) ∘ₛₗ (|ψ⟩ ⊗ₘ |φ⟩)). And also, Ket definition can both used for infinite Hilbert Space and finite Hilbert Space. How do you think of this definition? What are pros and cons of doing this?
This issue is for the improvement of the documentation related to the Harmonic Oscillator. We should check the following:
- Are there any typos or grammatical errors?
- Does the structure make sense to someone with a limited understanding of Lean? (if not what can be improved)
The documentation currently is attached:
If you have suggestions of improvements feel free to add a comment below, and I can edit the docs accordingly whilst making the suggester a co-author of the commit.
This issue is to track which module-doc strings are good and which need improving.
If a doc-string for a module is already 'good', please tick it off here, otherwise feel free to improve it.
Doc-string module improvements
Classical mechanics
- PhysLean.ClassicalMechanics.Basic
- PhysLean.ClassicalMechanics.EulerLagrange
- PhysLean.ClassicalMechanics.HamiltonsEquations
- #738
- PhysLean.ClassicalMechanics.HarmonicOscillator.Solution
- PhysLean.ClassicalMechanics.Mass.MassUnit
- PhysLean.ClassicalMechanics.VectorFields
- PhysLean.ClassicalMechanics.WaveEquation.Basic
- PhysLean.ClassicalMechanics.WaveEquation.HarmonicWave
Condensed matter
Cosmology
Electromagnetism
- PhysLean.Electromagnetism.Basic
- PhysLean.Electromagnetism.Charge.ChargeUnit
- #723
- PhysLean.Electromagnetism.Electrostatics.OneDimension.PointParticle
- PhysLean.Electromagnetism.Electrostatics.OneDimension.Vacuum
- PhysLean.Electromagnetism.Electrostatics.TreeDimension.PointParticle
- PhysLean.Electromagnetism.FieldStrength.Basic
- PhysLean.Electromagnetism.FieldStrength.Derivative
- PhysLean.Electromagnetism.Homogeneous
- PhysLean.Electromagnetism.LorentzAction
- PhysLean.Electromagnetism.MaxwellEquations
- PhysLean.Electromagnetism.Wave
Mathematics
- PhysLean.Mathematics.Calculus.AdjFDeriv
- PhysLean.Mathematics.Calculus.Divergence
- PhysLean.Mathematics.DataStructures.FourTree.Basic
- PhysLean.Mathematics.DataStructures.FourTree.UniqueMap
- PhysLean.Mathematics.DataStructures.Matrix.LieTrace
- PhysLean.Mathematics.Distribution.Basic
- PhysLean.Mathematics.Distribution.OfBounded
- PhysLean.Mathematics.Distribution.PowMul
- PhysLean.Mathematics.FDerivCurry
- PhysLean.Mathematics.Fin
- PhysLean.Mathematics.Fin.Involutions
- PhysLean.Mathematics.Geometry.Metric.PseudoRiemannian.Defs
- PhysLean.Mathematics.Geometry.Metric.Riemannian.Defs
- PhysLean.Mathematics.InnerProductSpace.Adjoint
- PhysLean.Mathematics.InnerProductSpace.Basic
- PhysLean.Mathematics.InnerProductSpace.Calculus
- PhysLean.Mathematics.LinearMaps
- PhysLean.Mathematics.List
- PhysLean.Mathematics.List.InsertIdx
- PhysLean.Mathematics.List.InsertionSort
- PhysLean.Mathematics.PiTensorProduct
- PhysLean.Mathematics.RatComplexNum
- PhysLean.Mathematics.SO3.Basic
- PhysLean.Mathematics.SchurTriangulation
- PhysLean.Mathematics.SpecialFunctions.PhysHermite
- PhysLean.Mathematics.Trigonometry.Tanh
- PhysLean.Mathematics.VariationalCalculus.Basic
- PhysLean.Mathematics.VariationalCalculus.HasVarAdjDeriv
- PhysLean.Mathematics.VariationalCalculus.HasVarAdjoint
- PhysLean.Mathematics.VariationalCalculus.HasVarGradient
- PhysLean.Mathematics.VariationalCalculus.IsLocalizedfunctionTransform
- PhysLean.Mathematics.VariationalCalculus.IsTestFunction
Meta
- PhysLean.Meta.AllFilePaths
- PhysLean.Meta.Basic
- PhysLean.Meta.Informal.Basic
- PhysLean.Meta.Informal.Post
- PhysLean.Meta.Informal.SemiFormal
- PhysLean.Meta.Linters.Sorry
- PhysLean.Meta.Notes.Basic
- PhysLean.Meta.Notes.HTMLNote
- PhysLean.Meta.Notes.NoteFile
- PhysLean.Meta.Notes.ToHTML
- PhysLean.Meta.Remark.Basic
- PhysLean.Meta.Remark.Properties
- PhysLean.Meta.TODO.Basic
- PhysLean.Meta.TransverseTactics
Optics
Particles
- PhysLean.Particles.BeyondTheStandardModel.GeorgiGlashow.Basic
- PhysLean.Particles.BeyondTheStandardModel.PatiSalam.Basic
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Basic
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.FamilyMaps
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.NoGrav.Basic
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.Basic
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.DimSevenPlane
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.FamilyMaps
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Permutations
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.BMinusL
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.Basic
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.BoundPlaneDim
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.FamilyMaps
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.HyperCharge
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.PlaneNonSols
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.QuadSol
- PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.QuadSolToSol
- PhysLean.Particles.BeyondTheStandardModel.Spin10.Basic
- PhysLean.Particles.BeyondTheStandardModel.TwoHDM.Basic
- PhysLean.Particles.BeyondTheStandardModel.TwoHDM.GaugeOrbits
- PhysLean.Particles.FlavorPhysics.CKMMatrix.Basic
- PhysLean.Particles.FlavorPhysics.CKMMatrix.Invariants
- PhysLean.Particles.FlavorPhysics.CKMMatrix.PhaseFreedom
- PhysLean.Particles.FlavorPhysics.CKMMatrix.Relations
- PhysLean.Particles.FlavorPhysics.CKMMatrix.Rows
- PhysLean.Particles.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
- PhysLean.Particles.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters
- PhysLean.Particles.StandardModel.AnomalyCancellation.Basic
- PhysLean.Particles.StandardModel.AnomalyCancellation.FamilyMaps
- PhysLean.Particles.StandardModel.AnomalyCancellation.NoGrav.Basic
- PhysLean.Particles.StandardModel.AnomalyCancellation.NoGrav.One.Lemmas
- PhysLean.Particles.StandardModel.AnomalyCancellation.NoGrav.One.LinearParameterization
- PhysLean.Particles.StandardModel.AnomalyCancellation.Permutations
- PhysLean.Particles.StandardModel.Basic
- PhysLean.Particles.StandardModel.HiggsBoson.Basic
- PhysLean.Particles.StandardModel.HiggsBoson.GaugeAction
- PhysLean.Particles.StandardModel.HiggsBoson.PointwiseInnerProd
- PhysLean.Particles.StandardModel.HiggsBoson.Potential
- PhysLean.Particles.StandardModel.Representations
- PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.B3
- PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Basic
- PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.HyperCharge
- PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.LineY3B3
- PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.Basic
- PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.PlaneWithY3B3
- PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.ToSols
- PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Permutations
- PhysLean.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Y3
- PhysLean.Particles.SuperSymmetry.SU5.Charges.AllowsTerm
- PhysLean.Particles.SuperSymmetry.SU5.Charges.Basic
- PhysLean.Particles.SuperSymmetry.SU5.Charges.Completions
- PhysLean.Particles.SuperSymmetry.SU5.Charges.Map
- PhysLean.Particles.SuperSymmetry.SU5.Charges.MinimalSuperSet
- PhysLean.Particles.SuperSymmetry.SU5.Charges.MinimallyAllowsTerm.Basic
- PhysLean.Particles.SuperSymmetry.SU5.Charges.MinimallyAllowsTerm.FinsetTerms
- PhysLean.Particles.SuperSymmetry.SU5.Charges.MinimallyAllowsTerm.OfFinset
- PhysLean.Particles.SuperSymmetry.SU5.Charges.OfFieldLabel
- PhysLean.Particles.SuperSymmetry.SU5.Charges.OfPotentialTerm
- PhysLean.Particles.SuperSymmetry.SU5.Charges.PhenoClosed
- PhysLean.Particles.SuperSymmetry.SU5.Charges.PhenoConstrained
- PhysLean.Particles.SuperSymmetry.SU5.Charges.U1U1
- PhysLean.Particles.SuperSymmetry.SU5.Charges.Yukawa
- PhysLean.Particles.SuperSymmetry.SU5.Charges.ZMod
- PhysLean.Particles.SuperSymmetry.SU5.FieldLabels
- PhysLean.Particles.SuperSymmetry.SU5.Potential
QFT
- PhysLean.QFT.AnomalyCancellation.Basic
- PhysLean.QFT.AnomalyCancellation.GroupActions
- PhysLean.QFT.PerturbationTheory.CreateAnnihilate
- PhysLean.QFT.PerturbationTheory.FeynmanDiagrams.Basic
- PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.Basic
- PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.Grading
- PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.NormTimeOrder
- PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.NormalOrder
- PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.SuperCommute
- PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.TimeOrder
- PhysLean.QFT.PerturbationTheory.FieldSpecification.Basic
- PhysLean.QFT.PerturbationTheory.FieldSpecification.CrAnFieldOp
- PhysLean.QFT.PerturbationTheory.FieldSpecification.CrAnSection
- PhysLean.QFT.PerturbationTheory.FieldSpecification.Filters
- PhysLean.QFT.PerturbationTheory.FieldSpecification.NormalOrder
- PhysLean.QFT.PerturbationTheory.FieldSpecification.TimeOrder
- PhysLean.QFT.PerturbationTheory.FieldStatistics.Basic
- PhysLean.QFT.PerturbationTheory.FieldStatistics.ExchangeSign
- PhysLean.QFT.PerturbationTheory.FieldStatistics.OfFinset
- PhysLean.QFT.PerturbationTheory.Koszul.KoszulSign
- PhysLean.QFT.PerturbationTheory.Koszul.KoszulSignInsert
- PhysLean.QFT.PerturbationTheory.WickAlgebra.Basic
- PhysLean.QFT.PerturbationTheory.WickAlgebra.Grading
- PhysLean.QFT.PerturbationTheory.WickAlgebra.NormalOrder.Basic
- PhysLean.QFT.PerturbationTheory.WickAlgebra.NormalOrder.Lemmas
- PhysLean.QFT.PerturbationTheory.WickAlgebra.NormalOrder.WickContractions
- PhysLean.QFT.PerturbationTheory.WickAlgebra.StaticWickTerm
- PhysLean.QFT.PerturbationTheory.WickAlgebra.StaticWickTheorem
- PhysLean.QFT.PerturbationTheory.WickAlgebra.SuperCommute
- PhysLean.QFT.PerturbationTheory.WickAlgebra.TimeContraction
- PhysLean.QFT.PerturbationTheory.WickAlgebra.TimeOrder
- PhysLean.QFT.PerturbationTheory.WickAlgebra.Universality
- PhysLean.QFT.PerturbationTheory.WickAlgebra.WickTerm
- PhysLean.QFT.PerturbationTheory.WickAlgebra.WicksTheorem
- PhysLean.QFT.PerturbationTheory.WickAlgebra.WicksTheoremNormal
- PhysLean.QFT.PerturbationTheory.WickContraction.Basic
- PhysLean.QFT.PerturbationTheory.WickContraction.Card
- PhysLean.QFT.PerturbationTheory.WickContraction.Erase
- PhysLean.QFT.PerturbationTheory.WickContraction.ExtractEquiv
- PhysLean.QFT.PerturbationTheory.WickContraction.InsertAndContract
- PhysLean.QFT.PerturbationTheory.WickContraction.InsertAndContractNat
- PhysLean.QFT.PerturbationTheory.WickContraction.Involutions
- PhysLean.QFT.PerturbationTheory.WickContraction.IsFull
- PhysLean.QFT.PerturbationTheory.WickContraction.Join
- PhysLean.QFT.PerturbationTheory.WickContraction.Perm
- PhysLean.QFT.PerturbationTheory.WickContraction.Sign.Basic
- PhysLean.QFT.PerturbationTheory.WickContraction.Sign.InsertNone
- PhysLean.QFT.PerturbationTheory.WickContraction.Sign.InsertSome
- PhysLean.QFT.PerturbationTheory.WickContraction.Sign.Join
- PhysLean.QFT.PerturbationTheory.WickContraction.Singleton
- PhysLean.QFT.PerturbationTheory.WickContraction.StaticContract
- PhysLean.QFT.PerturbationTheory.WickContraction.SubContraction
- PhysLean.QFT.PerturbationTheory.WickContraction.TimeCond
- PhysLean.QFT.PerturbationTheory.WickContraction.TimeContract
- PhysLean.QFT.PerturbationTheory.WickContraction.Uncontracted
- PhysLean.QFT.PerturbationTheory.WickContraction.UncontractedList
- PhysLean.QFT.QED.AnomalyCancellation.Basic
- PhysLean.QFT.QED.AnomalyCancellation.BasisLinear
- PhysLean.QFT.QED.AnomalyCancellation.ConstAbs
- PhysLean.QFT.QED.AnomalyCancellation.Even.BasisLinear
- PhysLean.QFT.QED.AnomalyCancellation.Even.LineInCubic
- PhysLean.QFT.QED.AnomalyCancellation.Even.Parameterization
- PhysLean.QFT.QED.AnomalyCancellation.LineInPlaneCond
- PhysLean.QFT.QED.AnomalyCancellation.LowDim.One
- PhysLean.QFT.QED.AnomalyCancellation.LowDim.Three
- PhysLean.QFT.QED.AnomalyCancellation.LowDim.Two
- PhysLean.QFT.QED.AnomalyCancellation.Odd.BasisLinear
- PhysLean.QFT.QED.AnomalyCancellation.Odd.LineInCubic
- PhysLean.QFT.QED.AnomalyCancellation.Odd.Parameterization
- PhysLean.QFT.QED.AnomalyCancellation.Permutations
- PhysLean.QFT.QED.AnomalyCancellation.Sorts
- PhysLean.QFT.QED.AnomalyCancellation.VectorLike
Quantum mechanics
- PhysLean.QuantumMechanics.FiniteTarget.Basic
- PhysLean.QuantumMechanics.FiniteTarget.HilbertSpace
- PhysLean.QuantumMechanics.OneDimension.GeneralPotential.Basic
- PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Basic
- PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Completeness
- PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Eigenfunction
- PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.TISE
- PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Basic
- PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Gaussians
- PhysLean.QuantumMechanics.OneDimension.HilbertSpace.PlaneWaves
- PhysLean.QuantumMechanics.OneDimension.HilbertSpace.PositionStates
- PhysLean.QuantumMechanics.OneDimension.HilbertSpace.SchwartzSubmodule
- PhysLean.QuantumMechanics.OneDimension.Operators.Commutation
- PhysLean.QuantumMechanics.OneDimension.Operators.Momentum
- PhysLean.QuantumMechanics.OneDimension.Operators.Parity
- PhysLean.QuantumMechanics.OneDimension.Operators.Position
- PhysLean.QuantumMechanics.OneDimension.Operators.Unbounded
- PhysLean.QuantumMechanics.OneDimension.ReflectionlessPotential.Basic
- PhysLean.QuantumMechanics.PlanckConstant
Relativity
- PhysLean.Relativity.Bispinors.Basic
- PhysLean.Relativity.CliffordAlgebra
- PhysLean.Relativity.LorentzAlgebra.Basic
- PhysLean.Relativity.LorentzAlgebra.Basis
- PhysLean.Relativity.LorentzAlgebra.ExponentialMap
- PhysLean.Relativity.LorentzGroup.Basic
- PhysLean.Relativity.LorentzGroup.Boosts.Apply
- PhysLean.Relativity.LorentzGroup.Boosts.Basic
- PhysLean.Relativity.LorentzGroup.Boosts.Generalized
- PhysLean.Relativity.LorentzGroup.Orthochronous.Basic
- PhysLean.Relativity.LorentzGroup.Proper
- PhysLean.Relativity.LorentzGroup.Restricted.Basic
- PhysLean.Relativity.LorentzGroup.Restricted.FromBoostRotation
- PhysLean.Relativity.LorentzGroup.Rotations
- PhysLean.Relativity.LorentzGroup.ToVector
- PhysLean.Relativity.MinkowskiMatrix
- PhysLean.Relativity.PauliMatrices.AsTensor
- PhysLean.Relativity.PauliMatrices.Basic
- PhysLean.Relativity.PauliMatrices.CliffordAlgebra
- PhysLean.Relativity.PauliMatrices.Relations
- PhysLean.Relativity.PauliMatrices.SelfAdjoint
- PhysLean.Relativity.PauliMatrices.ToTensor
- PhysLean.Relativity.SL2C.Basic
- PhysLean.Relativity.SL2C.SelfAdjoint
- PhysLean.Relativity.Special.ProperTime
- PhysLean.Relativity.Special.TwinParadox.Basic
- PhysLean.Relativity.Tensors.Basic
- PhysLean.Relativity.Tensors.Color.Basic
- PhysLean.Relativity.Tensors.Color.Discrete
- PhysLean.Relativity.Tensors.Color.Lift
- PhysLean.Relativity.Tensors.ComplexTensor.Basic
- PhysLean.Relativity.Tensors.ComplexTensor.Lemmas
- PhysLean.Relativity.Tensors.ComplexTensor.Matrix.Pre
- PhysLean.Relativity.Tensors.ComplexTensor.Metrics.Basic
- PhysLean.Relativity.Tensors.ComplexTensor.Metrics.Lemmas
- PhysLean.Relativity.Tensors.ComplexTensor.Metrics.Pre
- PhysLean.Relativity.Tensors.ComplexTensor.OfRat
- PhysLean.Relativity.Tensors.ComplexTensor.Units.Basic
- PhysLean.Relativity.Tensors.ComplexTensor.Units.Pre
- PhysLean.Relativity.Tensors.ComplexTensor.Units.Symm
- PhysLean.Relativity.Tensors.ComplexTensor.Vector.Pre.Basic
- PhysLean.Relativity.Tensors.ComplexTensor.Vector.Pre.Contraction
- PhysLean.Relativity.Tensors.ComplexTensor.Vector.Pre.Modules
- PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Basic
- PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Contraction
- PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Metric
- PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Modules
- PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Two
- PhysLean.Relativity.Tensors.ComplexTensor.Weyl.Unit
- PhysLean.Relativity.Tensors.Constructors
- PhysLean.Relativity.Tensors.Contraction.Basic
- PhysLean.Relativity.Tensors.Contraction.Basis
- PhysLean.Relativity.Tensors.Contraction.Products
- PhysLean.Relativity.Tensors.Contraction.Pure
- PhysLean.Relativity.Tensors.Dual
- PhysLean.Relativity.Tensors.Elab
- PhysLean.Relativity.Tensors.Evaluation
- PhysLean.Relativity.Tensors.MetricTensor
- PhysLean.Relativity.Tensors.OfInt
- PhysLean.Relativity.Tensors.Product
- PhysLean.Relativity.Tensors.RealTensor.Basic
- PhysLean.Relativity.Tensors.RealTensor.Derivative
- PhysLean.Relativity.Tensors.RealTensor.Matrix.Pre
- PhysLean.Relativity.Tensors.RealTensor.Metrics.Basic
- PhysLean.Relativity.Tensors.RealTensor.Metrics.Pre
- PhysLean.Relativity.Tensors.RealTensor.ToComplex
- PhysLean.Relativity.Tensors.RealTensor.Units.Pre
- PhysLean.Relativity.Tensors.RealTensor.Vector.Basic
- PhysLean.Relativity.Tensors.RealTensor.Vector.Causality.Basic
- PhysLean.Relativity.Tensors.RealTensor.Vector.Causality.LightLike
- PhysLean.Relativity.Tensors.RealTensor.Vector.Causality.TimeLike
- PhysLean.Relativity.Tensors.RealTensor.Vector.MinkowskiProduct
- PhysLean.Relativity.Tensors.RealTensor.Vector.Pre.Basic
- PhysLean.Relativity.Tensors.RealTensor.Vector.Pre.Contraction
- PhysLean.Relativity.Tensors.RealTensor.Vector.Pre.Modules
- PhysLean.Relativity.Tensors.RealTensor.Velocity.Basic
- PhysLean.Relativity.Tensors.TensorSpecies.Basic
- PhysLean.Relativity.Tensors.Tensorial
- PhysLean.Relativity.Tensors.UnitTensor
SpaceAndTime
- PhysLean.SpaceAndTime.Space.Basic
- PhysLean.SpaceAndTime.Space.Distributions
- PhysLean.SpaceAndTime.Space.LengthUnit
- PhysLean.SpaceAndTime.Space.SpaceStruct
- PhysLean.SpaceAndTime.Space.VectorIdentities
- PhysLean.SpaceAndTime.SpaceTime.Basic
- PhysLean.SpaceAndTime.SpaceTime.TimeSlice
- PhysLean.SpaceAndTime.Time.Basic
- PhysLean.SpaceAndTime.Time.TimeMan
- PhysLean.SpaceAndTime.Time.TimeTransMan
- PhysLean.SpaceAndTime.Time.TimeUnit
StatisticalMechanics
- PhysLean.StatisticalMechanics.BoltzmannConstant
- PhysLean.StatisticalMechanics.CanonicalEnsemble.Basic
- PhysLean.StatisticalMechanics.CanonicalEnsemble.Finite
- PhysLean.StatisticalMechanics.CanonicalEnsemble.TwoState
StringTheory
- PhysLean.StringTheory.Basic
- PhysLean.StringTheory.FTheory.SU5.Basic
- PhysLean.StringTheory.FTheory.SU5.Charges.AnomalyFree
- PhysLean.StringTheory.FTheory.SU5.Charges.OfRationalSection
- PhysLean.StringTheory.FTheory.SU5.Charges.Viable
- PhysLean.StringTheory.FTheory.SU5.Fluxes.Basic
- PhysLean.StringTheory.FTheory.SU5.Fluxes.NoExotics.ChiralIndices
- PhysLean.StringTheory.FTheory.SU5.Fluxes.NoExotics.Completeness
- PhysLean.StringTheory.FTheory.SU5.Fluxes.NoExotics.Elems
- PhysLean.StringTheory.FTheory.SU5.Fluxes.NoExotics.ToList
- PhysLean.StringTheory.FTheory.SU5.Quanta.Basic
- PhysLean.StringTheory.FTheory.SU5.Quanta.FiveQuanta
- PhysLean.StringTheory.FTheory.SU5.Quanta.IsViable
- PhysLean.StringTheory.FTheory.SU5.Quanta.TenQuanta
Thermodynamics
- PhysLean.Thermodynamics.Basic
- PhysLean.Thermodynamics.Temperature.Basic
- PhysLean.Thermodynamics.Temperature.TemperatureUnits
Units
- PhysLean.Units.Basic
- PhysLean.Units.Examples
- PhysLean.Units.FDeriv
- PhysLean.Units.Integral
- PhysLean.Units.WithDim.Area
- PhysLean.Units.WithDim.Basic
- PhysLean.Units.WithDim.Energy
- PhysLean.Units.WithDim.Mass
- PhysLean.Units.WithDim.Momentum
- PhysLean.Units.WithDim.Pressure
- PhysLean.Units.WithDim.Speed
- PhysLean.Units.WithDim.Velocity
This is to track progress in the direction of on-boarding documentation. It is being discussed on the Lean Zulip here. Some possible directions:
- Improve the getting started page: https://physlean.com/GettingStarted with information regarding GitHub forking etc.
- Update the contributing file in the main PhysLean repository, to include the key information needed to contribute to the project.
- Create a frequently asked questions page concerning basic questions within the project.
Feel suggest other points here, or assign yourself to any points. Long-form discussions or questions should be made on the Zulip.
See the discussion here.
We should introduce the notion of a measurement along with an axiom. Ideally this should take account of units but also allow us to work with things abstractly.
There was an attempt at defining a second at #488. See also the discussion here.
Working on building out the Kinematics module in PhysLean/ClassicalMechanics/Kinematics, starting with:
Definitions.lean → Time, Position, Velocity, Acceleration
Equations.lean → Constant acceleration equations
Theorems.lean → Proofs of derivative-based relationships
This issue originates from this conversation.
- Define the epsilon tensor in general dimension. See here.
- Redefine the
spaceCurlin terms of this epsilon tensor. - Define a continuous linear equivalence between
SpaceTimeandTime x Space. - Define a map
timeSlicetakingSpaceTime → MtoTime → Space → Mwith corresponding API. - Define
((realLorentzTensor d).tensorBasis _ (fun x => Fin.cast (by simp) μ))formally as a unit vector in SpaceTime pointing the μ direction. - Change
SpaceTime.derivto an abbreviation offderivusing the above spacetime derivative. - Come up with a good way to go from
SpaceTimetoSpacederivatives etc. (e.g. greek derivatives vs latin) - Use the above to rewrite Maxwell's equations in a better way.
For more details on individual points see the details of the above conversation.
The following modules need their module doc-string improved (this is the first docstring in the file) to include the following information:
- A description of the physical content of the module (file) (or if it is the
Basicmodule an overall physical description of the physics within that directory). - The current status, i.e. what are the important definitions and lemmas in that file or directory.
- What is left to be done, with referenced TODO items.
An example is given in
If you update one of these please change the status of it here, or write a comment on this issue. More modules may be added to this list.
In the formalization of beyond the standard model gauge groups, there are the following TODO items:
Georgi-Glashow Model
- informal_def (6V2WM): GeorgiGlashow.GaugeGroupI
- informal_def (6V2WS): GeorgiGlashow.inclSM
- informal_lemma (6V2W2): GeorgiGlashow.inclSM_ker
- informal_def (6V2XA): GeorgiGlashow.embedSMℤ₆
Pati-Salam
- informal_def (6V2Q2): PatiSalam.GaugeGroupI
- informal_def (6V2RH): PatiSalam.inclSM
- informal_lemma (6V2RQ): PatiSalam.inclSM_ker
- informal_def (6V2RY): PatiSalam.embedSMℤ₃
- informal_def (6V2R7): PatiSalam.gaugeGroupISpinEquiv
- informal_def (6V2SG): PatiSalam.gaugeGroupℤ₂SubGroup
- informal_def (6V2SM): PatiSalam.GaugeGroupℤ₂
- informal_lemma (6V2SV): PatiSalam.sm_ℤ₆_factor_through_gaugeGroupℤ₂SubGroup
- informal_def (6V2S4): PatiSalam.embedSMℤ₆Toℤ₂
Spin(10) model (aka SO(10) model)
- informal_def (6V2S4): PatiSalam.embedSMℤ₆Toℤ₂
- informal_def (6V2YG): Spin10Model.inclPatiSalam
- informal_def (6V2YO): Spin10Model.inclSM
- informal_def (6V2YU): Spin10Model.inclGeorgiGlashow
- informal_def (6V2YZ): Spin10Model.inclSMThruGeorgiGlashow
- informal_lemma (6V2Y6): Spin10Model.inclSM_eq_inclSMThruGeorgiGlashow
The categorification of aspects of index notation is leading to type-theoretic problems. I think it is best to separate the actual implementation of index notation in PhysLean from the formal categorical aspects. I think this will help make proofs etc. in this area smoother.
Subtasks
- Remove categorical structure of map in perm
There are lots of erw [...] in PhysLean. These are slow, and thus it is beneficial for them to be removed.
To remove an erw [...] usually means changing the corresponding lemma to simp-normal form.
The whole of PhysLean needs the MultiGoal linter run on it and all the warnings dealt with.
In particular
[leanOptions]
linter.style.multiGoal = true
should be added to lakefile.toml and the project built with lake build.
This will generate warnings, some of which may be from Mathlib, but the ones from PhysLean should be dealt. For example:
exact h
exact h2
should be replaced with:
· exact h1
· exact h2
This issue is tied to the project:
https://github.com/orgs/HEPLean/projects/3
The aim of which is to track progress in quantum mechanics within PhysLean.
This is an issue to track the formalization of properties of the Pauli matrices.
The goal is to prove the properties of the Pauli matrices using index notation with HepLean. The properties of the Pauli matrices to be proved are (2.23)-(2.30) of this note.
- 2.23
- 2.24
- 2.25
- 2.26
- 2.27
- 2.28
- 2.29
- 2.30
It may be best to complete a number of steps before this:
- Improve the API around the basis of tensors and tensor trees, to allow calculations to be done by looking at each component (Done in #343)
- Improve the @[simp]'s lemma around tensor trees and tensors, to make the calculations of the above as simple as possible. (Done in #343)
- Define an integer version of (coordinates of) tensors, and show that it injects into all tensors. On these
decidecan be used. (Done in #343) - Using the above three, simplify the proof and speed of:
pauliCo_contr_pauliContr. (Done in #343) - Define the epsilon Lorentz tensor with four four-vector indices.
- Write the above lemmas out using index notation in Lean.
After these have all been formalized:
- Make a curated noted containing for Pauli matrices and their properties.
This issue is related to: #286.
Contributions to this issue are very much welcome in any direction.
There are two parts to this issue:
- The way
informal_lemmaandinformal_definitioncurrently work in HepLean is that they are turned through elaboration into elements of the typeInformalLemmaorInformalDefinition. This does not seem like the most optimal approach, and an approach similar toTODOelements will likely work better. - The output of
informal_lemmaandinformal_definitionon the HepLean website needs improving. Either with an updated form of graph or just a list of them.
It's preferable to align the workflows of HepLean with that of Mathlib. Here's the task breakdown:
- Automatically tag and release after a version bump.
- Move the dependency of doc-gen4 from the top-level lakefile to a separate
docleandirectory as suggested by doc-gen4, and create a workflow that is triggered when a PR merges similar to the documentation generation of Mathlib barring the separate repo. This preventslake, called from the top-level, from pulling and building doc-gen4 and its dependencies. - Incorporate Mathlib linters.
If more tasks are required, feel free to add them to the list above, and link related PRs to the "Development" section on the right of the GitHub web UI.
Hey, I loved learning about this project (although I am by no means able to understand more than 10% :D)
Just a suggestion: why not write a short blog post at https://github.com/leanprover-community/blog/ announcing this project? I don't know how many people are looking into the blog, but I mean it wouldn't hurt, would it?
If you are interested I can prepare a post for you with the basics (I understand) and you can than add additional infos.
Best wishes for the project, I hope it will attract a lot of contributors!