merge master

.codespellignore

@@ -0,0 +1,11 @@
+digitalize
+Digitalising
+statics
+disjointness
+lightYears
+tne
+hge
+Breal
+ket
+rIn
+FRO

.github/ISSUE_TEMPLATE/API.yml

@@ -0,0 +1,33 @@
+name: API
+description: Auto-filled issue for API building
+title: "API: "
+labels:
+  - API
+  - help wanted
+  - Requirements needed
+body:
+  - type: textarea
+    id: content
+    attributes:
+      label: Details
+      value: |
+        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](https://www.ibm.com/docs/en/SSYQBZ_9.6.1/com.ibm.doors.requirements.doc/topics/get_it_right_the_first_time.pdf).
+
+        ## Corresponding file system
+
+        If it exists, the part of the PhysLean which corresponds to this API.
+
+    validations:
+      required: false

.github/ISSUE_TEMPLATE/Bump.yml

@@ -20,7 +20,8 @@ body:
     options:
       - label: Update mathlib rev in lakefile.toml.
       - label: Update doc-gen4 rev in lakefile.toml.
-      - label: Run `rm -rf .lake; lake update`.
+      - label: Remove the `.lake` file, e.g. on unix run `rm -rf .lake`.
+      - label: Run `lake update`.
       - label: Check `lean-toolchain` updates correctly.
       - label: Update the Lean version badge in the `README.md` file.
   validations:
@@ -55,15 +56,17 @@ body:
     description: Please check off these items as you complete them
     options:
       - label: Create a tag for the new version.
+      - label: Put a bump notice on this [thread](https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/Bumps.20of.20PhysLean.2E/with/572707099).
   validations:
     required: false
 - type: textarea
   id: examples_of_previous_bumps
   attributes:
-    label: Previous bump
+    label: Example past bumps
     description: Please do not modify this text.
     value: |
-      [v4.20.0](https://github.com/HEPLean/PhysLean/pull/591),
-      [v4.20.0-rc5](https://github.com/HEPLean/PhysLean/pull/566)
+      [v4.20.0](https://github.com/lean-phys-community/PhysLean/pull/591),
+      [v4.20.0-rc5](https://github.com/lean-phys-community/PhysLean/pull/566)
+      [v4.27.0](https://github.com/lean-phys-community/PhysLean/pull/929)
   validations:
     required: true

.github/workflows/build.yml

@@ -89,3 +89,13 @@ jobs:
         run: |
           chmod u+x scripts/lint-style.sh
           ./scripts/lint-style.sh
+
+  codespell:
+    name: Check for spelling errors
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+      - uses: codespell-project/actions-codespell@v2
+        with:
+          exclude_file: scripts/MetaPrograms/spellingWords.txt,scripts/physleanNoShake.json
+          ignore_words_file: .codespellignore

PhysLean.lean

@@ -1,13 +1,18 @@
 import PhysLean.ClassicalMechanics.Basic
+import PhysLean.ClassicalMechanics.DampedHarmonicOscillator.Basic
 import PhysLean.ClassicalMechanics.EulerLagrange
 import PhysLean.ClassicalMechanics.HamiltonsEquations
 import PhysLean.ClassicalMechanics.HarmonicOscillator.Basic
+import PhysLean.ClassicalMechanics.HarmonicOscillator.ConfigurationSpace
 import PhysLean.ClassicalMechanics.HarmonicOscillator.Solution
+import PhysLean.ClassicalMechanics.Lagrangian.TotalDerivativeEquivalence
 import PhysLean.ClassicalMechanics.Mass.MassUnit
+import PhysLean.ClassicalMechanics.Pendulum.CoplanarDoublePendulum
+import PhysLean.ClassicalMechanics.Pendulum.MiscellaneousPendulumPivotMotions
+import PhysLean.ClassicalMechanics.Pendulum.SlidingPendulum
 import PhysLean.ClassicalMechanics.RigidBody.Basic
 import PhysLean.ClassicalMechanics.RigidBody.SolidSphere
 import PhysLean.ClassicalMechanics.Scattering.RigidSphere
-import PhysLean.ClassicalMechanics.VectorFields
 import PhysLean.ClassicalMechanics.Vibrations.LinearTriatomic
 import PhysLean.ClassicalMechanics.WaveEquation.Basic
 import PhysLean.ClassicalMechanics.WaveEquation.HarmonicWave
@@ -17,37 +22,32 @@ import PhysLean.Cosmology.Basic
 import PhysLean.Cosmology.FLRW.Basic
 import PhysLean.Electromagnetism.Basic
 import PhysLean.Electromagnetism.Charge.ChargeUnit
-import PhysLean.Electromagnetism.Distributions.Potential
+import PhysLean.Electromagnetism.Current.CircularCoil
+import PhysLean.Electromagnetism.Current.InfiniteWire
+import PhysLean.Electromagnetism.Dynamics.Basic
 import PhysLean.Electromagnetism.Dynamics.CurrentDensity
 import PhysLean.Electromagnetism.Dynamics.Hamiltonian
 import PhysLean.Electromagnetism.Dynamics.IsExtrema
 import PhysLean.Electromagnetism.Dynamics.KineticTerm
 import PhysLean.Electromagnetism.Dynamics.Lagrangian
-import PhysLean.Electromagnetism.Electrostatics.Basic
 import PhysLean.Electromagnetism.Kinematics.Boosts
 import PhysLean.Electromagnetism.Kinematics.EMPotential
 import PhysLean.Electromagnetism.Kinematics.ElectricField
 import PhysLean.Electromagnetism.Kinematics.FieldStrength
 import PhysLean.Electromagnetism.Kinematics.MagneticField
 import PhysLean.Electromagnetism.Kinematics.ScalarPotential
 import PhysLean.Electromagnetism.Kinematics.VectorPotential
-import PhysLean.Electromagnetism.MaxwellEquations
-import PhysLean.Electromagnetism.PointParticle.FiniteCollection
 import PhysLean.Electromagnetism.PointParticle.OneDimension
 import PhysLean.Electromagnetism.PointParticle.ThreeDimension
 import PhysLean.Electromagnetism.Vacuum.Constant
-import PhysLean.Electromagnetism.Vacuum.Homogeneous
-import PhysLean.Electromagnetism.Vacuum.OneDimension
-import PhysLean.Electromagnetism.Vacuum.Wave
+import PhysLean.Electromagnetism.Vacuum.HarmonicWave
+import PhysLean.Electromagnetism.Vacuum.IsPlaneWave
 import PhysLean.Mathematics.Calculus.AdjFDeriv
 import PhysLean.Mathematics.Calculus.Divergence
 import PhysLean.Mathematics.DataStructures.FourTree.Basic
 import PhysLean.Mathematics.DataStructures.FourTree.UniqueMap
 import PhysLean.Mathematics.DataStructures.Matrix.LieTrace
 import PhysLean.Mathematics.Distribution.Basic
-import PhysLean.Mathematics.Distribution.Function.InvPowMeasure
-import PhysLean.Mathematics.Distribution.Function.IsDistBounded
-import PhysLean.Mathematics.Distribution.Function.OfFunction
 import PhysLean.Mathematics.Distribution.PowMul
 import PhysLean.Mathematics.FDerivCurry
 import PhysLean.Mathematics.Fin
@@ -57,6 +57,8 @@ import PhysLean.Mathematics.Geometry.Metric.Riemannian.Defs
 import PhysLean.Mathematics.InnerProductSpace.Adjoint
 import PhysLean.Mathematics.InnerProductSpace.Basic
 import PhysLean.Mathematics.InnerProductSpace.Calculus
+import PhysLean.Mathematics.InnerProductSpace.Submodule
+import PhysLean.Mathematics.KroneckerDelta
 import PhysLean.Mathematics.LinearMaps
 import PhysLean.Mathematics.List
 import PhysLean.Mathematics.List.InsertIdx
@@ -109,7 +111,8 @@ import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.
 import PhysLean.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.QuadSolToSol
 import PhysLean.Particles.BeyondTheStandardModel.Spin10.Basic
 import PhysLean.Particles.BeyondTheStandardModel.TwoHDM.Basic
-import PhysLean.Particles.BeyondTheStandardModel.TwoHDM.GaugeOrbits
+import PhysLean.Particles.BeyondTheStandardModel.TwoHDM.GramMatrix
+import PhysLean.Particles.BeyondTheStandardModel.TwoHDM.Potential
 import PhysLean.Particles.FlavorPhysics.CKMMatrix.Basic
 import PhysLean.Particles.FlavorPhysics.CKMMatrix.Invariants
 import PhysLean.Particles.FlavorPhysics.CKMMatrix.PhaseFreedom
@@ -225,12 +228,22 @@ import PhysLean.QFT.QED.AnomalyCancellation.Odd.Parameterization
 import PhysLean.QFT.QED.AnomalyCancellation.Permutations
 import PhysLean.QFT.QED.AnomalyCancellation.Sorts
 import PhysLean.QFT.QED.AnomalyCancellation.VectorLike
+import PhysLean.QuantumMechanics.DDimensions.Hydrogen.Basic
+import PhysLean.QuantumMechanics.DDimensions.Hydrogen.LaplaceRungeLenzVector
+import PhysLean.QuantumMechanics.DDimensions.Operators.AngularMomentum
+import PhysLean.QuantumMechanics.DDimensions.Operators.Commutation
+import PhysLean.QuantumMechanics.DDimensions.Operators.Momentum
+import PhysLean.QuantumMechanics.DDimensions.Operators.Position
+import PhysLean.QuantumMechanics.DDimensions.Operators.Unbounded
+import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.Basic
+import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.SchwartzSubmodule
 import PhysLean.QuantumMechanics.FiniteTarget.Basic
 import PhysLean.QuantumMechanics.FiniteTarget.HilbertSpace
 import PhysLean.QuantumMechanics.OneDimension.GeneralPotential.Basic
 import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Basic
 import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Completeness
 import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Eigenfunction
+import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Examples
 import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.TISE
 import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Basic
 import PhysLean.QuantumMechanics.OneDimension.HilbertSpace.Gaussians
@@ -270,6 +283,7 @@ import PhysLean.Relativity.SL2C.Basic
 import PhysLean.Relativity.SL2C.SelfAdjoint
 import PhysLean.Relativity.Special.ProperTime
 import PhysLean.Relativity.Special.TwinParadox.Basic
+import PhysLean.Relativity.SpeedOfLight
 import PhysLean.Relativity.Tensors.Basic
 import PhysLean.Relativity.Tensors.Color.Basic
 import PhysLean.Relativity.Tensors.Color.Discrete
@@ -325,20 +339,33 @@ import PhysLean.Relativity.Tensors.TensorSpecies.Basic
 import PhysLean.Relativity.Tensors.Tensorial
 import PhysLean.Relativity.Tensors.UnitTensor
 import PhysLean.SpaceAndTime.Space.Basic
-import PhysLean.SpaceAndTime.Space.Distributions.Basic
-import PhysLean.SpaceAndTime.Space.Distributions.ConstantTime
+import PhysLean.SpaceAndTime.Space.ConstantSliceDist
+import PhysLean.SpaceAndTime.Space.CrossProduct
+import PhysLean.SpaceAndTime.Space.Derivatives.Basic
+import PhysLean.SpaceAndTime.Space.Derivatives.Curl
+import PhysLean.SpaceAndTime.Space.Derivatives.Div
+import PhysLean.SpaceAndTime.Space.Derivatives.Grad
+import PhysLean.SpaceAndTime.Space.Derivatives.Laplacian
+import PhysLean.SpaceAndTime.Space.DistConst
+import PhysLean.SpaceAndTime.Space.DistOfFunction
+import PhysLean.SpaceAndTime.Space.IsDistBounded
 import PhysLean.SpaceAndTime.Space.LengthUnit
-import PhysLean.SpaceAndTime.Space.SpaceStruct
+import PhysLean.SpaceAndTime.Space.Norm
+import PhysLean.SpaceAndTime.Space.RadialAngularMeasure
+import PhysLean.SpaceAndTime.Space.Slice
 import PhysLean.SpaceAndTime.Space.Translations
-import PhysLean.SpaceAndTime.Space.VectorIdentities
 import PhysLean.SpaceAndTime.SpaceTime.Basic
 import PhysLean.SpaceAndTime.SpaceTime.Boosts
-import PhysLean.SpaceAndTime.SpaceTime.Distributions
+import PhysLean.SpaceAndTime.SpaceTime.Derivatives
+import PhysLean.SpaceAndTime.SpaceTime.LorentzAction
 import PhysLean.SpaceAndTime.SpaceTime.TimeSlice
 import PhysLean.SpaceAndTime.Time.Basic
+import PhysLean.SpaceAndTime.Time.Derivatives
 import PhysLean.SpaceAndTime.Time.TimeMan
 import PhysLean.SpaceAndTime.Time.TimeTransMan
 import PhysLean.SpaceAndTime.Time.TimeUnit
+import PhysLean.SpaceAndTime.TimeAndSpace.Basic
+import PhysLean.SpaceAndTime.TimeAndSpace.ConstantTimeDist
 import PhysLean.StatisticalMechanics.BoltzmannConstant
 import PhysLean.StatisticalMechanics.CanonicalEnsemble.Basic
 import PhysLean.StatisticalMechanics.CanonicalEnsemble.Finite
@@ -358,6 +385,7 @@ import PhysLean.StringTheory.FTheory.SU5.Quanta.FiveQuanta
 import PhysLean.StringTheory.FTheory.SU5.Quanta.IsViable
 import PhysLean.StringTheory.FTheory.SU5.Quanta.TenQuanta
 import PhysLean.Thermodynamics.Basic
+import PhysLean.Thermodynamics.IdealGas.Basic
 import PhysLean.Thermodynamics.Temperature.Basic
 import PhysLean.Thermodynamics.Temperature.TemperatureUnits
 import PhysLean.Units.Basic