From aef181cf72ba1bfdee0dcf259bd4917c70100549 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Fri, 13 Mar 2026 19:40:59 -0700 Subject: [PATCH 1/4] feat(LaplaceRungeLenzVector): prove `angularMomentum_commutation_lrl` Co-authored-by: Aristotle (Harmonic) --- .../Hydrogen/LaplaceRungeLenzVector.lean | 41 +++++++++++++++++-- 1 file changed, 37 insertions(+), 4 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean index c7ea6d838..eb6f925aa 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean @@ -136,14 +136,48 @@ private def constRadiusRegInvCompPosition (ε : ℝˣ) (i : Fin H.d) := -/ /-- `⁅𝐋ᵢⱼ, 𝐀(ε)ₖ⁆ = iℏ(δᵢₖ𝐀(ε)ⱼ - δⱼₖ𝐀(ε)ᵢ)` -/ -@[sorryful] lemma angularMomentum_commutation_lrl (ε : ℝˣ) (i j k : Fin H.d) : ⁅𝐋[i,j], H.lrlOperator ε k⁆ = (Complex.I * ℏ * δ[i,k]) • H.lrlOperator ε j - (Complex.I * ℏ * δ[j,k]) • H.lrlOperator ε i := by - sorry + simp only [lrlOperator_eq' H ε] + simp only [lie_sub, lie_add, lie_sum, lie_smul, lie_leibniz] + simp only [angularMomentum_commutation_angularMomentum, + angularMomentum_commutation_momentum, + angularMomentum_commutation_radiusRegPow, + angularMomentum_commutation_position] + dsimp only [kroneckerDelta] + simp only [comp_sub, comp_smul, sub_comp, smul_comp, comp_zero, zero_comp, add_zero, + smul_sub, smul_add, smul_smul, comp_add, neg_comp, comp_neg, smul_neg] + simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib] + simp only [Nat.cast_ite, Nat.cast_one, CharP.cast_eq_zero, mul_ite, mul_one, mul_zero, + ite_smul, zero_smul, smul_ite, smul_zero, + Finset.sum_ite_eq, Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte] + rw [angularMomentumOperator_antisymm k i, angularMomentumOperator_antisymm k j] + simp only [neg_comp, comp_neg, smul_neg, neg_neg] + have ite_comp_right : ∀ (p : Prop) [Decidable p] + (A B : 𝓢(Space H.d, ℂ) →L[ℂ] 𝓢(Space H.d, ℂ)), + (if p then A else 0).comp B = if p then A.comp B else 0 := + fun p _ A B ↦ by split_ifs <;> simp + simp only [ite_comp_right, show ∀ (p : Prop) [Decidable p] + (A : 𝓢(Space H.d, ℂ) →L[ℂ] 𝓢(Space H.d, ℂ)), + -(if p then A else 0) = if p then -A else 0 from + fun p _ A ↦ by split_ifs <;> simp, + sub_comp, add_comp, smul_comp, zero_comp, neg_comp, + Finset.sum_add_distrib, Finset.sum_sub_distrib, + Finset.sum_ite_eq, Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte] + rw [angularMomentumOperator_antisymm i k, angularMomentumOperator_antisymm j k] + simp only [neg_comp, comp_neg, smul_neg, neg_neg, angularMomentumOperator_eq_zero, zero_comp] + split_ifs with hik hjk <;> + simp_all only [smul_zero, sub_zero, zero_sub, zero_smul, mul_zero, zero_mul, + Finset.sum_const_zero, add_zero, sub_self, neg_zero, neg_neg, + ← Finset.smul_sum, angularMomentumOperator_eq_zero, zero_comp] + all_goals try simp only [smul_comm (H.m * H.k) (Complex.I * ↑↑ℏ)] + all_goals (try (conv_lhs => rw [show + 2⁻¹ * Complex.I * ↑↑ℏ * (↑H.d - 1) * (Complex.I * ↑↑ℏ) = + Complex.I * ↑↑ℏ * (2⁻¹ * Complex.I * ↑↑ℏ * (↑H.d - 1)) from by ring])) + all_goals abel /-- `⁅𝐋ᵢⱼ, 𝐀(ε)²⁆ = 0` -/ -@[sorryful] lemma angularMomentum_commutation_lrlSqr (ε : ℝˣ) (i j : Fin H.d) : ⁅𝐋[i,j], H.lrlOperatorSqr ε⁆ = 0 := by unfold lrlOperatorSqr @@ -153,7 +187,6 @@ lemma angularMomentum_commutation_lrlSqr (ε : ℝˣ) (i j : Fin H.d) : simp [Finset.sum_add_distrib, Finset.sum_sub_distrib] /-- `⁅𝐋², 𝐀(ε)²⁆ = 0` -/ -@[sorryful] lemma angularMomentumSqr_commutation_lrlSqr (ε : ℝˣ) : ⁅angularMomentumOperatorSqr (d := H.d), H.lrlOperatorSqr ε⁆ = 0 := by unfold angularMomentumOperatorSqr From 9eff056573dadacbdcd3b500345636eb08c0228b Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sat, 14 Mar 2026 19:17:00 -0700 Subject: [PATCH 2/4] refactor(LaplaceRungeLenzVector): address review comments - Combine consecutive simp only calls - Extract inline show to named have neg_ite_zero - Replace all_goals with <;> chaining from split_ifs Co-authored-by: Aristotle (Harmonic) --- .../Hydrogen/LaplaceRungeLenzVector.lean | 36 +++++++++---------- 1 file changed, 17 insertions(+), 19 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean index eb6f925aa..b95443620 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean @@ -139,17 +139,14 @@ private def constRadiusRegInvCompPosition (ε : ℝˣ) (i : Fin H.d) := lemma angularMomentum_commutation_lrl (ε : ℝˣ) (i j k : Fin H.d) : ⁅𝐋[i,j], H.lrlOperator ε k⁆ = (Complex.I * ℏ * δ[i,k]) • H.lrlOperator ε j - (Complex.I * ℏ * δ[j,k]) • H.lrlOperator ε i := by - simp only [lrlOperator_eq' H ε] - simp only [lie_sub, lie_add, lie_sum, lie_smul, lie_leibniz] - simp only [angularMomentum_commutation_angularMomentum, - angularMomentum_commutation_momentum, - angularMomentum_commutation_radiusRegPow, - angularMomentum_commutation_position] + simp only [lrlOperator_eq' H ε, lie_sub, lie_add, lie_sum, lie_smul, lie_leibniz, + angularMomentum_commutation_angularMomentum, angularMomentum_commutation_momentum, + angularMomentum_commutation_radiusRegPow, angularMomentum_commutation_position] dsimp only [kroneckerDelta] simp only [comp_sub, comp_smul, sub_comp, smul_comp, comp_zero, zero_comp, add_zero, - smul_sub, smul_add, smul_smul, comp_add, neg_comp, comp_neg, smul_neg] - simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib] - simp only [Nat.cast_ite, Nat.cast_one, CharP.cast_eq_zero, mul_ite, mul_one, mul_zero, + smul_sub, smul_add, smul_smul, comp_add, neg_comp, comp_neg, smul_neg, + Finset.sum_add_distrib, Finset.sum_sub_distrib, + Nat.cast_ite, Nat.cast_one, CharP.cast_eq_zero, mul_ite, mul_one, mul_zero, ite_smul, zero_smul, smul_ite, smul_zero, Finset.sum_ite_eq, Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte] rw [angularMomentumOperator_antisymm k i, angularMomentumOperator_antisymm k j] @@ -158,10 +155,11 @@ lemma angularMomentum_commutation_lrl (ε : ℝˣ) (i j k : Fin H.d) : (A B : 𝓢(Space H.d, ℂ) →L[ℂ] 𝓢(Space H.d, ℂ)), (if p then A else 0).comp B = if p then A.comp B else 0 := fun p _ A B ↦ by split_ifs <;> simp - simp only [ite_comp_right, show ∀ (p : Prop) [Decidable p] - (A : 𝓢(Space H.d, ℂ) →L[ℂ] 𝓢(Space H.d, ℂ)), - -(if p then A else 0) = if p then -A else 0 from - fun p _ A ↦ by split_ifs <;> simp, + have neg_ite_zero : ∀ (p : Prop) [Decidable p] + (A : 𝓢(Space H.d, ℂ) →L[ℂ] 𝓢(Space H.d, ℂ)), + -(if p then A else 0) = if p then -A else 0 := + fun p _ A ↦ by split_ifs <;> simp + simp only [ite_comp_right, neg_ite_zero, sub_comp, add_comp, smul_comp, zero_comp, neg_comp, Finset.sum_add_distrib, Finset.sum_sub_distrib, Finset.sum_ite_eq, Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte] @@ -170,12 +168,12 @@ lemma angularMomentum_commutation_lrl (ε : ℝˣ) (i j k : Fin H.d) : split_ifs with hik hjk <;> simp_all only [smul_zero, sub_zero, zero_sub, zero_smul, mul_zero, zero_mul, Finset.sum_const_zero, add_zero, sub_self, neg_zero, neg_neg, - ← Finset.smul_sum, angularMomentumOperator_eq_zero, zero_comp] - all_goals try simp only [smul_comm (H.m * H.k) (Complex.I * ↑↑ℏ)] - all_goals (try (conv_lhs => rw [show - 2⁻¹ * Complex.I * ↑↑ℏ * (↑H.d - 1) * (Complex.I * ↑↑ℏ) = - Complex.I * ↑↑ℏ * (2⁻¹ * Complex.I * ↑↑ℏ * (↑H.d - 1)) from by ring])) - all_goals abel + ← Finset.smul_sum, angularMomentumOperator_eq_zero, zero_comp] <;> + (try simp only [smul_comm (H.m * H.k) (Complex.I * ↑↑ℏ)]) <;> + (try conv_lhs => rw [show + 2⁻¹ * Complex.I * ↑↑ℏ * (↑H.d - 1) * (Complex.I * ↑↑ℏ) = + Complex.I * ↑↑ℏ * (2⁻¹ * Complex.I * ↑↑ℏ * (↑H.d - 1)) from by ring]) <;> + abel /-- `⁅𝐋ᵢⱼ, 𝐀(ε)²⁆ = 0` -/ lemma angularMomentum_commutation_lrlSqr (ε : ℝˣ) (i j : Fin H.d) : From 971f6d38212c0fd6f408305250c744d599ac8814 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sat, 14 Mar 2026 19:27:52 -0700 Subject: [PATCH 3/4] fix(LaplaceRungeLenzVector): restore split simp calls (combining breaks rw) Co-authored-by: Aristotle (Harmonic) --- .../Hydrogen/LaplaceRungeLenzVector.lean | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean index b95443620..410293c6c 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean @@ -139,14 +139,17 @@ private def constRadiusRegInvCompPosition (ε : ℝˣ) (i : Fin H.d) := lemma angularMomentum_commutation_lrl (ε : ℝˣ) (i j k : Fin H.d) : ⁅𝐋[i,j], H.lrlOperator ε k⁆ = (Complex.I * ℏ * δ[i,k]) • H.lrlOperator ε j - (Complex.I * ℏ * δ[j,k]) • H.lrlOperator ε i := by - simp only [lrlOperator_eq' H ε, lie_sub, lie_add, lie_sum, lie_smul, lie_leibniz, - angularMomentum_commutation_angularMomentum, angularMomentum_commutation_momentum, - angularMomentum_commutation_radiusRegPow, angularMomentum_commutation_position] + simp only [lrlOperator_eq' H ε] + simp only [lie_sub, lie_add, lie_sum, lie_smul, lie_leibniz] + simp only [angularMomentum_commutation_angularMomentum, + angularMomentum_commutation_momentum, + angularMomentum_commutation_radiusRegPow, + angularMomentum_commutation_position] dsimp only [kroneckerDelta] simp only [comp_sub, comp_smul, sub_comp, smul_comp, comp_zero, zero_comp, add_zero, - smul_sub, smul_add, smul_smul, comp_add, neg_comp, comp_neg, smul_neg, - Finset.sum_add_distrib, Finset.sum_sub_distrib, - Nat.cast_ite, Nat.cast_one, CharP.cast_eq_zero, mul_ite, mul_one, mul_zero, + smul_sub, smul_add, smul_smul, comp_add, neg_comp, comp_neg, smul_neg] + simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib] + simp only [Nat.cast_ite, Nat.cast_one, CharP.cast_eq_zero, mul_ite, mul_one, mul_zero, ite_smul, zero_smul, smul_ite, smul_zero, Finset.sum_ite_eq, Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte] rw [angularMomentumOperator_antisymm k i, angularMomentumOperator_antisymm k j] From 88d554e6d66496b9ada17086c60bc841bce1d605 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 16 Mar 2026 18:06:46 -0700 Subject: [PATCH 4/4] refactor(LaplaceRungeLenzVector): remove unused simp args, drop unused have Co-authored-by: Aristotle (Harmonic) --- .../Hydrogen/LaplaceRungeLenzVector.lean | 22 ++++++++----------- 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean index 410293c6c..c987ed54a 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean @@ -146,30 +146,26 @@ lemma angularMomentum_commutation_lrl (ε : ℝˣ) (i j k : Fin H.d) : angularMomentum_commutation_radiusRegPow, angularMomentum_commutation_position] dsimp only [kroneckerDelta] - simp only [comp_sub, comp_smul, sub_comp, smul_comp, comp_zero, zero_comp, add_zero, - smul_sub, smul_add, smul_smul, comp_add, neg_comp, comp_neg, smul_neg] + simp only [comp_sub, comp_smul, zero_comp, add_zero, + smul_sub, smul_add, smul_smul] simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib] simp only [Nat.cast_ite, Nat.cast_one, CharP.cast_eq_zero, mul_ite, mul_one, mul_zero, ite_smul, zero_smul, smul_ite, smul_zero, - Finset.sum_ite_eq, Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte] + Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte] rw [angularMomentumOperator_antisymm k i, angularMomentumOperator_antisymm k j] - simp only [neg_comp, comp_neg, smul_neg, neg_neg] + simp only [neg_comp, smul_neg] have ite_comp_right : ∀ (p : Prop) [Decidable p] (A B : 𝓢(Space H.d, ℂ) →L[ℂ] 𝓢(Space H.d, ℂ)), (if p then A else 0).comp B = if p then A.comp B else 0 := fun p _ A B ↦ by split_ifs <;> simp - have neg_ite_zero : ∀ (p : Prop) [Decidable p] - (A : 𝓢(Space H.d, ℂ) →L[ℂ] 𝓢(Space H.d, ℂ)), - -(if p then A else 0) = if p then -A else 0 := - fun p _ A ↦ by split_ifs <;> simp - simp only [ite_comp_right, neg_ite_zero, - sub_comp, add_comp, smul_comp, zero_comp, neg_comp, + simp only [ite_comp_right, + sub_comp, add_comp, smul_comp, Finset.sum_add_distrib, Finset.sum_sub_distrib, - Finset.sum_ite_eq, Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte] + Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte] rw [angularMomentumOperator_antisymm i k, angularMomentumOperator_antisymm j k] - simp only [neg_comp, comp_neg, smul_neg, neg_neg, angularMomentumOperator_eq_zero, zero_comp] + simp only [neg_comp, smul_neg, neg_neg] split_ifs with hik hjk <;> - simp_all only [smul_zero, sub_zero, zero_sub, zero_smul, mul_zero, zero_mul, + simp_all only [smul_zero, sub_zero, zero_sub, zero_smul, zero_mul, Finset.sum_const_zero, add_zero, sub_self, neg_zero, neg_neg, ← Finset.smul_sum, angularMomentumOperator_eq_zero, zero_comp] <;> (try simp only [smul_comm (H.m * H.k) (Complex.I * ↑↑ℏ)]) <;>