feat: Laplace-Runge-Lenz vector (#947)

* refactor: positionOperator

* feat: (regularized) radius operator

* feat: (regularized) LRL vector

* feat: radius op commutators

* feat: commute

* minor changes

* feat: LRL vector, commutators and square

* golf + removing "simp only"s

* minor clean-up

* improved comments

* [H,A] sorry free

* rpow name change

* linter fixes

* linter fixes v2

* naming improvements

* todo: normRegularizedPow

Author: gloges

PhysLean.lean

@@ -226,6 +226,8 @@ 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

PhysLean/Mathematics/KroneckerDelta.lean

@@ -9,18 +9,25 @@ import PhysLean.Meta.TODO.Basic
 
 # Kronecker delta
 
-This file defines compact notation for the Kronecker delta, `δ[i,j] ≔ if (i = j) then 1 else 0`.
+This file defines the Kronecker delta, `δ[i,j] ≔ if (i = j) then 1 else 0`.
 
 -/
 TODO "YVABB" "Build functionality for working with sums involving Kronecker deltas."
 
-
 namespace KroneckerDelta
 
 /-- The Kronecker delta function, `ite (i = j) 1 0`. -/
-def kronecker_delta [Ring R] (i j : Fin d) : R := if (i = j) then 1 else 0
+def kroneckerDelta [Ring R] (i j : Fin d) : R := if (i = j) then 1 else 0
+
+@[inherit_doc kroneckerDelta]
+macro "δ[" i:term "," j:term "]" : term => `(kroneckerDelta $i $j)
+
+lemma kroneckerDelta_symm [Ring R] (i j : Fin d) :
+    kroneckerDelta (R := R) i j = kroneckerDelta j i :=
+  ite_cond_congr (Eq.propIntro Eq.symm Eq.symm)
 
-@[inherit_doc kronecker_delta]
-macro "δ[" i:term "," j:term "]" : term => `(kronecker_delta $i $j)
+lemma kroneckerDelta_self [Ring R] : ∀ i : Fin d, kroneckerDelta (R := R) i i = 1 := by
+  intro i
+  exact if_pos rfl
 
 end KroneckerDelta

PhysLean/QuantumMechanics/DDimensions/Hydrogen/Basic.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2026 Gregory J. Loges. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gregory J. Loges
+-/
+import PhysLean.QuantumMechanics.DDimensions.Operators.Momentum
+import PhysLean.QuantumMechanics.DDimensions.Operators.Position
+/-!
+
+# Hydrogen atom
+
+This module introduces the `d`-dimensional hydrogen atom with `1/r` potential.
+
+In addition to the dimension `d`, the quantum mechanical system is characterized by
+a mass `m > 0` and constant `k` appearing in the potential `V = -k/r`.
+The standard hydrogen atom has `d=3`, `m = mₑmₚ/(mₑ + mₚ) ≈ mₑ` and `k = e²/4πε₀`.
+
+The potential `V = -k/r` is singular at the origin. To address this we define a regularized
+Hamiltonian in which the potential is replaced by `-k(r(ε)⁻¹ + ½ε²r(ε)⁻³)`, where
+`r(ε)² = ‖x‖² + ε²`. The `ε²/r³` term limits to the zero distribution for `ε → 0`
+but is convenient to include for two reasons:
+- It improves the convergence: `r(ε)⁻¹ + ½ε²r(ε)⁻³ = r⁻¹(1 + O(ε⁴/r⁴))` with no `O(ε²/r²)` term.
+- It is what appears in the commutators of the (regularized) LRL vector components.
+
+-/
+
+namespace QuantumMechanics
+open SchwartzMap
+
+/-- A hydrogen atom is characterized by the number of spatial dimensions `d`,
+  the mass `m` and the coefficient `k` for the `1/r` potential. -/
+structure HydrogenAtom where
+  /-- Number of spatial dimensions -/
+  d : ℕ
+
+  /-- Mass (positive) -/
+  m : ℝ
+  hm : 0 < m
+
+  /-- Coefficient in potential (positive for attractive) -/
+  k : ℝ
+
+namespace HydrogenAtom
+noncomputable section
+
+variable (H : HydrogenAtom)
+
+@[simp]
+lemma m_ne_zero : H.m ≠ 0 := by linarith [H.hm]
+
+/-- The hydrogen atom Hamiltonian regularized by `ε > 0` is defined to be
+  `𝐇(ε) ≔ (2m)⁻¹𝐩² - k(𝐫(ε)⁻¹ + ½ε²𝐫(ε)⁻³)`. -/
+def hamiltonianReg (ε : ℝ) : 𝓢(Space H.d, ℂ) →L[ℂ] 𝓢(Space H.d, ℂ) :=
+  (2 * H.m)⁻¹ • 𝐩² - H.k • (𝐫[ε,-1] + (2⁻¹ * ε ^ 2) • 𝐫[ε,-3])
+
+end
+end HydrogenAtom
+end QuantumMechanics