Imports
/- 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 -/ module public import Physlib.QuantumMechanics.Hydrogen.Basic public import Physlib.QuantumMechanics.Operators.Commutation public import Physlib.Meta.Linters.Sorry

Laplace-Runge-Lenz vector

In this file we define

    The (regularized) LRL vector operator for the quantum mechanical hydrogen atom, 𝐀(ε)ᵢ ≔ ½(𝐩ⱼ𝐋ᵢⱼ + 𝐋ᵢⱼ𝐩ⱼ) - mk·𝐫(ε)⁻¹𝐱ᵢ.

The main results are

    The commutators ⁅𝐋ᵢⱼ, 𝐀(ε)ₖ⁆ = iℏ(δᵢₖ𝐀(ε)ⱼ - δⱼₖ𝐀(ε)ᵢ) in angularMomentum_commutation_lrl

    The commutators ⁅𝐀(ε)ᵢ, 𝐀(ε)ⱼ⁆ = (-2iℏm·𝐇(ε) + iℏmkε²·𝐫(ε)⁻³))𝐋ᵢⱼ in lrl_commutation_lrl

    The commutators ⁅𝐇(ε), 𝐀(ε)ᵢ⁆ = iℏε²(⋯) in hamiltonianReg_commutation_lrl

    The relation 𝐀(ε)² = 2m 𝐇(ε)(𝐋² + ¼ℏ²(d-1)²) + m²k² + ε²(⋯) in lrlOperatorSqr_eq

@[expose] public sectionattribute [local instance 100] LieRing.ofAssociativeRing

The (regularized) Laplace-Runge-Lenz vector operator for the d-dimensional hydrogen atom, 𝐀(ε)ᵢ ≔ ½(𝐩ⱼ𝐋ᵢⱼ + 𝐋ᵢⱼ𝐩ⱼ) - mk·𝐫(ε)⁻¹𝐱ᵢ.

def lrlOperator (ε : ˣ) (i : Fin H.d) : 𝓢(Space H.d, ) →L[] 𝓢(Space H.d, ) := (2 : )⁻¹ (𝐩 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐩) - (H.m * H.k) 𝐫₀ ε (-1) ∘L 𝐱 i

𝐀(ε)ᵢ = 𝐱ᵢ𝐩² - (𝐱ⱼ𝐩ⱼ)𝐩ᵢ + ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ

H:HydrogenAtomε:ˣi:Fin H.d2⁻¹ (𝐩 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐩) = 𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩) - (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐩 i + (2⁻¹ * I * * (H.d - 1)) 𝐩 i -- mk·r⁻¹x terms match exactly calc _ = (2 : )⁻¹ j, ((𝐩 j ∘L 𝐱 i) ∘L 𝐩 j + 𝐱 i ∘L 𝐩 j ∘L 𝐩 j - ((𝐩 j ∘L 𝐱 j) ∘L 𝐩 i + 𝐱 j ∘L 𝐩 j ∘L 𝐩 i)) := H:HydrogenAtomε:ˣi:Fin H.d2⁻¹ (𝐩 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐩) = 2⁻¹ j, ((𝐩 j ∘SL 𝐱 i) ∘SL 𝐩 j + 𝐱 i ∘SL 𝐩 j ∘SL 𝐩 j - ((𝐩 j ∘SL 𝐱 j) ∘SL 𝐩 i + 𝐱 j ∘SL 𝐩 j ∘SL 𝐩 i)) simp_rw H:HydrogenAtomε:ˣi:Fin H.d2⁻¹ (𝐩 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐩) = 2⁻¹ j, ((𝐩 j ∘SL 𝐱 i) ∘SL 𝐩 j + 𝐱 i ∘SL 𝐩 j ∘SL 𝐩 j - ((𝐩 j ∘SL 𝐱 j) ∘SL 𝐩 i + 𝐱 j ∘SL 𝐩 j ∘SL 𝐩 i))H:HydrogenAtomε:ˣi:Fin H.d2⁻¹ ( i_1, 𝐩 i_1 * 𝐋 i i_1 + i_1, 𝐋 i i_1 * 𝐩 i_1) = 2⁻¹ j, ((𝐩 j ∘SL 𝐱 i) ∘SL 𝐩 j + 𝐱 i ∘SL 𝐩 j ∘SL 𝐩 j - ((𝐩 j ∘SL 𝐱 j) ∘SL 𝐩 i + 𝐱 j ∘SL 𝐩 j ∘SL 𝐩 i)) H:HydrogenAtomε:ˣi:Fin H.d2⁻¹ ( x, 𝐩 x ∘SL 𝐋 i x + x, 𝐋 i x ∘SL 𝐩 x) = 2⁻¹ j, ((𝐩 j ∘SL 𝐱 i) ∘SL 𝐩 j + 𝐱 i ∘SL 𝐩 j ∘SL 𝐩 j - ((𝐩 j ∘SL 𝐱 j) ∘SL 𝐩 i + 𝐱 j ∘SL 𝐩 j ∘SL 𝐩 i)) H:HydrogenAtomε:ˣi:Fin H.d2⁻¹ x, (𝐩 x ∘SL 𝐋 i x + 𝐋 i x ∘SL 𝐩 x) = 2⁻¹ j, ((𝐩 j ∘SL 𝐱 i) ∘SL 𝐩 j + 𝐱 i ∘SL 𝐩 j ∘SL 𝐩 j - ((𝐩 j ∘SL 𝐱 j) ∘SL 𝐩 i + 𝐱 j ∘SL 𝐩 j ∘SL 𝐩 i)) H:HydrogenAtomε:ˣi:Fin H.d2⁻¹ x, (𝐩 x ∘SL (𝐱 i ∘SL 𝐩 x - 𝐱 x ∘SL 𝐩 i) + (𝐱 i ∘SL 𝐩 x - 𝐱 x ∘SL 𝐩 i) ∘SL 𝐩 x) = 2⁻¹ j, ((𝐩 j ∘SL 𝐱 i) ∘SL 𝐩 j + 𝐱 i ∘SL 𝐩 j ∘SL 𝐩 j - ((𝐩 j ∘SL 𝐱 j) ∘SL 𝐩 i + 𝐱 j ∘SL 𝐩 j ∘SL 𝐩 i)) H:HydrogenAtomε:ˣi:Fin H.d2⁻¹ x, (𝐩 x ∘SL 𝐱 i ∘SL 𝐩 x - 𝐩 x ∘SL 𝐱 x ∘SL 𝐩 i + (𝐱 i ∘SL 𝐩 x - 𝐱 x ∘SL 𝐩 i) ∘SL 𝐩 x) = 2⁻¹ j, ((𝐩 j ∘SL 𝐱 i) ∘SL 𝐩 j + 𝐱 i ∘SL 𝐩 j ∘SL 𝐩 j - ((𝐩 j ∘SL 𝐱 j) ∘SL 𝐩 i + 𝐱 j ∘SL 𝐩 j ∘SL 𝐩 i)) H:HydrogenAtomε:ˣi:Fin H.d2⁻¹ x, (𝐩 x ∘SL 𝐱 i ∘SL 𝐩 x - 𝐩 x ∘SL 𝐱 x ∘SL 𝐩 i + ((𝐱 i ∘SL 𝐩 x) ∘SL 𝐩 x - (𝐱 x ∘SL 𝐩 i) ∘SL 𝐩 x)) = 2⁻¹ j, ((𝐩 j ∘SL 𝐱 i) ∘SL 𝐩 j + 𝐱 i ∘SL 𝐩 j ∘SL 𝐩 j - ((𝐩 j ∘SL 𝐱 j) ∘SL 𝐩 i + 𝐱 j ∘SL 𝐩 j ∘SL 𝐩 i)) H:HydrogenAtomε:ˣi:Fin H.d2⁻¹ x, (𝐩 x ∘SL 𝐱 i ∘SL 𝐩 x - 𝐩 x ∘SL 𝐱 x ∘SL 𝐩 i + (𝐱 i ∘SL 𝐩 x ∘SL 𝐩 x - 𝐱 x ∘SL 𝐩 i ∘SL 𝐩 x)) = 2⁻¹ x, (𝐩 x ∘SL 𝐱 i ∘SL 𝐩 x + 𝐱 i ∘SL 𝐩 x ∘SL 𝐩 x - (𝐩 x ∘SL 𝐱 x ∘SL 𝐩 i + 𝐱 x ∘SL 𝐩 x ∘SL 𝐩 i)) H:HydrogenAtomε:ˣi:Fin H.d2⁻¹ x, (𝐩 x ∘SL 𝐱 i ∘SL 𝐩 x - 𝐩 x ∘SL 𝐱 x ∘SL 𝐩 i + (𝐱 i ∘SL 𝐩 x ∘SL 𝐩 x - 𝐱 x ∘SL 𝐩 i ∘SL 𝐩 x)) = 2⁻¹ x, (𝐩 x ∘SL 𝐱 i ∘SL 𝐩 x + 𝐱 i ∘SL 𝐩 x ∘SL 𝐩 x - (𝐩 x ∘SL 𝐱 x ∘SL 𝐩 i + 𝐱 x ∘SL 𝐩 i ∘SL 𝐩 x)) H:HydrogenAtomε:ˣi:Fin H.d2⁻¹ x, (𝐩 x ∘SL 𝐱 i ∘SL 𝐩 x - 𝐩 x ∘SL 𝐱 x ∘SL 𝐩 i + (𝐱 i ∘SL 𝐩 x ∘SL 𝐩 x - 𝐱 x ∘SL 𝐩 i ∘SL 𝐩 x)) = 2⁻¹ x, (𝐩 x ∘SL 𝐱 i ∘SL 𝐩 x + 𝐱 i ∘SL 𝐩 x ∘SL 𝐩 x - 𝐩 x ∘SL 𝐱 x ∘SL 𝐩 i - 𝐱 x ∘SL 𝐩 i ∘SL 𝐩 x) H:HydrogenAtomε:ˣi:Fin H.d2⁻¹ x, (𝐩 x ∘SL 𝐱 i ∘SL 𝐩 x - 𝐩 x ∘SL 𝐱 x ∘SL 𝐩 i + 𝐱 i ∘SL 𝐩 x ∘SL 𝐩 x - 𝐱 x ∘SL 𝐩 i ∘SL 𝐩 x) = 2⁻¹ x, (𝐩 x ∘SL 𝐱 i ∘SL 𝐩 x + 𝐱 i ∘SL 𝐩 x ∘SL 𝐩 x - 𝐩 x ∘SL 𝐱 x ∘SL 𝐩 i - 𝐱 x ∘SL 𝐩 i ∘SL 𝐩 x) All goals completed! 🐙] _ = (2 : )⁻¹ j, ((2 : ) 𝐱 i ∘L 𝐩 j ∘L 𝐩 j - (I * ) δ[i,j] 𝐩 j - ((2 : ) (𝐱 j ∘L 𝐩 j) ∘L 𝐩 i - (I * ) 𝐩 i)) := H:HydrogenAtomε:ˣi:Fin H.d2⁻¹ j, ((𝐩 j ∘SL 𝐱 i) ∘SL 𝐩 j + 𝐱 i ∘SL 𝐩 j ∘SL 𝐩 j - ((𝐩 j ∘SL 𝐱 j) ∘SL 𝐩 i + 𝐱 j ∘SL 𝐩 j ∘SL 𝐩 i)) = 2⁻¹ j, (2 𝐱 i ∘SL 𝐩 j ∘SL 𝐩 j - (I * ) δ[i,j] 𝐩 j - (2 (𝐱 j ∘SL 𝐩 j) ∘SL 𝐩 i - (I * ) 𝐩 i)) All goals completed! 🐙 _ = (2 : )⁻¹ j, ((2 : ) 𝐱 i ∘L 𝐩 j ∘L 𝐩 j - (2 : ) (𝐱 j ∘L 𝐩 j) ∘L 𝐩 i + (I * ) 𝐩 i - (I * ) δ[i,j] 𝐩 j) := H:HydrogenAtomε:ˣi:Fin H.d2⁻¹ j, (2 𝐱 i ∘SL 𝐩 j ∘SL 𝐩 j - (I * ) δ[i,j] 𝐩 j - (2 (𝐱 j ∘SL 𝐩 j) ∘SL 𝐩 i - (I * ) 𝐩 i)) = 2⁻¹ j, (2 𝐱 i ∘SL 𝐩 j ∘SL 𝐩 j - 2 (𝐱 j ∘SL 𝐩 j) ∘SL 𝐩 i + (I * ) 𝐩 i - (I * ) δ[i,j] 𝐩 j) simp_rw H:HydrogenAtomε:ˣi:Fin H.d2⁻¹ j, (2 𝐱 i ∘SL 𝐩 j ∘SL 𝐩 j - (I * ) δ[i,j] 𝐩 j - (2 (𝐱 j ∘SL 𝐩 j) ∘SL 𝐩 i - (I * ) 𝐩 i)) = 2⁻¹ j, (2 𝐱 i ∘SL 𝐩 j ∘SL 𝐩 j - 2 (𝐱 j ∘SL 𝐩 j) ∘SL 𝐩 i + (I * ) 𝐩 i - (I * ) δ[i,j] 𝐩 j)H:HydrogenAtomε:ˣi:Fin H.d2⁻¹ x, (2 𝐱 i ∘SL 𝐩 x ∘SL 𝐩 x - 2 (𝐱 x ∘SL 𝐩 x) ∘SL 𝐩 i - ((I * ) δ[i,x] 𝐩 x - (I * ) 𝐩 i)) = 2⁻¹ j, (2 𝐱 i ∘SL 𝐩 j ∘SL 𝐩 j - 2 (𝐱 j ∘SL 𝐩 j) ∘SL 𝐩 i + (I * ) 𝐩 i - (I * ) δ[i,j] 𝐩 j) All goals completed! 🐙] _ = 𝐱 i ∘L (𝐩 ⬝ᵥ 𝐩) - (𝐱 ⬝ᵥ 𝐩) ∘L 𝐩 i + ((2⁻¹ * I * ) H.d 𝐩 i - (2⁻¹ * I * ) 𝐩 i) := H:HydrogenAtomε:ˣi:Fin H.d2⁻¹ j, (2 𝐱 i ∘SL 𝐩 j ∘SL 𝐩 j - 2 (𝐱 j ∘SL 𝐩 j) ∘SL 𝐩 i + (I * ) 𝐩 i - (I * ) δ[i,j] 𝐩 j) = 𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩) - (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐩 i + ((2⁻¹ * I * ) H.d 𝐩 i - (2⁻¹ * I * ) 𝐩 i) H:HydrogenAtomε:ˣi:Fin H.d(2⁻¹ * 2) 𝐱 i ∘SL i, 𝐩 i ∘SL 𝐩 i - (2⁻¹ * 2) (∑ i, 𝐱 i ∘SL 𝐩 i) ∘SL 𝐩 i + ((2⁻¹ * (I * )) x, 𝐩 i - (2⁻¹ * (I * )) 𝐩 i) = 𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩) - (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐩 i + ((2⁻¹ * (I * )) H.d 𝐩 i - (2⁻¹ * (I * )) 𝐩 i) H:HydrogenAtomε:ˣi:Fin H.d𝐱 i ∘SL i, 𝐩 i ∘SL 𝐩 i - (∑ i, 𝐱 i ∘SL 𝐩 i) ∘SL 𝐩 i = 𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩) - (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐩 i All goals completed! 🐙 _ = 𝐱 i ∘L (𝐩 ⬝ᵥ 𝐩) - (𝐱 ⬝ᵥ 𝐩) ∘L 𝐩 i + (2⁻¹ * I * * (H.d - 1)) 𝐩 i := H:HydrogenAtomε:ˣi:Fin H.d𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩) - (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐩 i + ((2⁻¹ * I * ) H.d 𝐩 i - (2⁻¹ * I * ) 𝐩 i) = 𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩) - (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐩 i + (2⁻¹ * I * * (H.d - 1)) 𝐩 i All goals completed! 🐙

𝐀(ε)ᵢ = 𝐋ᵢⱼ𝐩ⱼ + ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ

H:HydrogenAtomε:ˣi:Fin H.d𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩) - (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐩 i = 𝐋 i ⬝ᵥ 𝐩 H:HydrogenAtomε:ˣi:Fin H.d𝐋 i ⬝ᵥ 𝐩 = 𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩) - (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐩 i H:HydrogenAtomε:ˣi:Fin H.d𝐋 i ⬝ᵥ 𝐩 = j, 𝐱 i ∘SL 𝐩 j ∘SL 𝐩 j - j, (𝐱 j ∘SL 𝐩 j) ∘SL 𝐩 iH:HydrogenAtomε:ˣi:Fin H.d j, 𝐱 i ∘SL 𝐩 j ∘SL 𝐩 j - j, (𝐱 j ∘SL 𝐩 j) ∘SL 𝐩 i = 𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩) - (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐩 i H:HydrogenAtomε:ˣi:Fin H.d𝐋 i ⬝ᵥ 𝐩 = j, 𝐱 i ∘SL 𝐩 j ∘SL 𝐩 j - j, (𝐱 j ∘SL 𝐩 j) ∘SL 𝐩 i All goals completed! 🐙 All goals completed! 🐙

𝐀(ε)ᵢ = 𝐩ⱼ𝐋ᵢⱼ - ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ

lemma lrlOperator_eq'' (ε : ˣ) (i : Fin H.d) : H.lrlOperator ε i = 𝐩 ⬝ᵥ 𝐋 i - (2⁻¹ * I * * (H.d - 1)) 𝐩 i - (H.m * H.k) 𝐫₀ ε (-1) ∘L 𝐱 i := H:HydrogenAtomε:ˣi:Fin H.dH.lrlOperator ε i = 𝐩 ⬝ᵥ 𝐋 i - (2⁻¹ * I * * (H.d - 1)) 𝐩 i - (H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 i H:HydrogenAtomε:ˣi:Fin H.dH.lrlOperator ε i = 2 H.lrlOperator ε i - H.lrlOperator ε iH:HydrogenAtomε:ˣi:Fin H.d2 H.lrlOperator ε i - H.lrlOperator ε i = 𝐩 ⬝ᵥ 𝐋 i - (2⁻¹ * I * * (H.d - 1)) 𝐩 i - (H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 i H:HydrogenAtomε:ˣi:Fin H.dH.lrlOperator ε i = 2 H.lrlOperator ε i - H.lrlOperator ε i All goals completed! 🐙 nth_rw 2 [H:HydrogenAtomε:ˣi:Fin H.d2 H.lrlOperator ε i - (𝐋 i ⬝ᵥ 𝐩 + (2⁻¹ * I * * (H.d - 1)) 𝐩 i - (H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 i) = 𝐩 ⬝ᵥ 𝐋 i - (2⁻¹ * I * * (H.d - 1)) 𝐩 i - (H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 iH:HydrogenAtomε:ˣi:Fin H.d2 H.lrlOperator ε i - (𝐋 i ⬝ᵥ 𝐩 + (2⁻¹ * I * * (H.d - 1)) 𝐩 i - (H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 i) = 𝐩 ⬝ᵥ 𝐋 i - (2⁻¹ * I * * (H.d - 1)) 𝐩 i - (H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 i H:HydrogenAtomε:ˣi:Fin H.d(2 * 2⁻¹) (𝐩 ⬝ᵥ 𝐋 i) + (2 * 2⁻¹) (𝐋 i ⬝ᵥ 𝐩) - (2 * (H.m * H.k)) 𝐫₀ ε (-1) ∘SL 𝐱 i - (𝐋 i ⬝ᵥ 𝐩 + (2⁻¹ * I * * (H.d - 1)) 𝐩 i - (H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 i) = 𝐩 ⬝ᵥ 𝐋 i - (2⁻¹ * I * * (H.d - 1)) 𝐩 i - (H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 i H:HydrogenAtomε:ˣi:Fin H.d1 (𝐩 ⬝ᵥ 𝐋 i) + 1 (𝐋 i ⬝ᵥ 𝐩) - (H.m * H.k * 2) 𝐫₀ ε (-1) ∘SL 𝐱 i - (𝐋 i ⬝ᵥ 𝐩 + (I * * (-1 / 2) + I * * H.d * (1 / 2)) 𝐩 i - (H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 i) = 𝐩 ⬝ᵥ 𝐋 i - (I * * (-1 / 2) + I * * H.d * (1 / 2)) 𝐩 i - (H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 i H:HydrogenAtomε:ˣi:Fin H.dx✝¹:𝓢(Space H.d, )x✝:Space H.d((1 (𝐩 ⬝ᵥ 𝐋 i) + 1 (𝐋 i ⬝ᵥ 𝐩) - (H.m * H.k * 2) 𝐫₀ ε (-1) ∘SL 𝐱 i - (𝐋 i ⬝ᵥ 𝐩 + (I * * (-1 / 2) + I * * H.d * (1 / 2)) 𝐩 i - (H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 i)) x✝¹) x✝ = ((𝐩 ⬝ᵥ 𝐋 i - (I * * (-1 / 2) + I * * H.d * (1 / 2)) 𝐩 i - (H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 i) x✝¹) x✝ H:HydrogenAtomε:ˣi:Fin H.dx✝¹:𝓢(Space H.d, )x✝:Space H.d((𝐩 ⬝ᵥ 𝐋 i) x✝¹) x✝ + ((𝐋 i ⬝ᵥ 𝐩) x✝¹) x✝ - H.m * H.k * 2 * (((x✝ ^ 2 + ε ^ 2) ^ (-1 / 2)) * ((x✝.val i) * x✝¹ x✝)) - (((𝐋 i ⬝ᵥ 𝐩) x✝¹) x✝ + -((I * * (-1 / 2) + I * * H.d * 2⁻¹) * (I * * Space.deriv i (⇑x✝¹) x✝)) - H.m * H.k * (((x✝ ^ 2 + ε ^ 2) ^ (-1 / 2)) * ((x✝.val i) * x✝¹ x✝))) = ((𝐩 ⬝ᵥ 𝐋 i) x✝¹) x✝ + (I * * (-1 / 2) + I * * H.d * 2⁻¹) * (I * * Space.deriv i (⇑x✝¹) x✝) - H.m * H.k * (((x✝ ^ 2 + ε ^ 2) ^ (-1 / 2)) * ((x✝.val i) * x✝¹ x✝)) All goals completed! 🐙

⁅𝐋ᵢⱼ, 𝐀(ε)ₖ⁆ = iℏ(δᵢₖ𝐀(ε)ⱼ - δⱼₖ𝐀(ε)ᵢ)

@[sorryful] lemma declaration uses `sorry`angularMomentum_commutation_lrl (ε : ˣ) (i j k : Fin H.d) : 𝐋 i j, H.lrlOperator ε k = (I * ) (δ[i,k] H.lrlOperator ε j - δ[j,k] H.lrlOperator ε i) := H:HydrogenAtomε:ˣi:Fin H.dj:Fin H.dk:Fin H.d𝐋 i j, H.lrlOperator ε k = (I * ) (δ[i,k] H.lrlOperator ε j - δ[j,k] H.lrlOperator ε i) All goals completed! 🐙

⁅𝐋ᵢⱼ, 𝐀(ε)²⁆ = 0

@[sorryful, simp] lemma angularMomentum_commutation_lrlSqr (ε : ˣ) (i j : Fin H.d) : 𝐋 i j, H.lrlOperator ε ⬝ᵥ H.lrlOperator ε = 0 := H:HydrogenAtomε:ˣi:Fin H.dj:Fin H.d𝐋 i j, H.lrlOperator ε ⬝ᵥ H.lrlOperator ε = 0 All goals completed! 🐙

⁅𝐋², 𝐀(ε)²⁆ = 0

@[sorryful, simp] lemma angularMomentumSqr_commutation_lrlSqr (ε : ˣ) : 𝐋²[H.d], H.lrlOperator ε ⬝ᵥ H.lrlOperator ε = 0 := H:HydrogenAtomε:ˣ𝐋², H.lrlOperator ε ⬝ᵥ H.lrlOperator ε = 0 All goals completed! 🐙
/- ## LRL / LRL commutators To compute the commutator `⁅𝐀ᵢ(ε), 𝐀ⱼ(ε)⁆` we take the following approach: - Write `𝐀(ε)ᵢ = 𝐱ᵢ𝐩² - (𝐱ⱼ𝐩ⱼ)𝐩ᵢ + ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ ≕ f1ᵢ - f2ᵢ + f3ᵢ - f4ᵢ` - Organize the sixteen terms which result from expanding `⁅f1ᵢ-f2ᵢ+f3ᵢ-f4ᵢ, f1ⱼ-f2ⱼ+f3ⱼ-f4ⱼ⁆` into four diagonal terms such as `⁅f1ᵢ, f1ⱼ⁆` and six off-diagonal pairs such as `⁅f1ᵢ, f3ⱼ⁆ + ⁅f3ᵢ, f1ⱼ⁆ = ⁅f1ᵢ, f3ⱼ⁆ - ⁅f1ⱼ, f3ᵢ⁆`. - Compute the diagonal commutators and off-diagonal pairs individually. Many vanish, and those that don't are all of the form `iℏ (⋯) 𝐋ᵢⱼ` (as they must to be antisymmetric in `i,j`). - Collect terms. -/ private lemma positionDotMomentum_commutation_position {d : } (i : Fin d) : 𝐱[d] ⬝ᵥ 𝐩, 𝐱 i = (-I * ) 𝐱 i := d:i:Fin d𝐱 ⬝ᵥ 𝐩, 𝐱 i = (-I * ) 𝐱 i d:i:Fin d𝐱 ⬝ᵥ 𝐩, 𝐱 i = j, 𝐱 j ∘SL 𝐩 j, 𝐱 id:i:Fin d j, 𝐱 j ∘SL 𝐩 j, 𝐱 i = (-I * ) 𝐱 i d:i:Fin d𝐱 ⬝ᵥ 𝐩, 𝐱 i = j, 𝐱 j ∘SL 𝐩 j, 𝐱 i All goals completed! 🐙 simp_rw d:i:Fin d j, 𝐱 j ∘SL 𝐩 j, 𝐱 i = (-I * ) 𝐱 id:i:Fin d x, 𝐱 x ∘SL (-𝐱 i, 𝐩 x) = (-I * ) 𝐱 i d:i:Fin d x, 𝐱 x ∘SL (-((I * ) δ[i,x] ContinuousLinearMap.id 𝓢(Space d, ))) = (-I * ) 𝐱 i d:i:Fin d x, 𝐱 x ∘SL (-(I * ) δ[i,x] ContinuousLinearMap.id 𝓢(Space d, )) = (-I * ) 𝐱 i d:i:Fin d x, 𝐱 x ∘SL ((-I * ) δ[i,x] ContinuousLinearMap.id 𝓢(Space d, )) = (-I * ) 𝐱 i d:i:Fin d x, (-I * ) δ[i,x] 𝐱 x ∘SL ContinuousLinearMap.id 𝓢(Space d, ) = (-I * ) 𝐱 i d:i:Fin d x, (-I * ) δ[i,x] 𝐱 x = (-I * ) 𝐱 i d:i:Fin d(-I * ) x, δ[i,x] 𝐱 x = (-I * ) 𝐱 i All goals completed! 🐙]private lemma positionDotMomentum_commutation_momentum {d : } (i : Fin d) : 𝐱[d] ⬝ᵥ 𝐩, 𝐩 i = (I * ) 𝐩 i := d:i:Fin d𝐱 ⬝ᵥ 𝐩, 𝐩 i = (I * ) 𝐩 i d:i:Fin d𝐱 ⬝ᵥ 𝐩, 𝐩 i = j, 𝐱 j, 𝐩 i ∘SL 𝐩 jd:i:Fin d j, 𝐱 j, 𝐩 i ∘SL 𝐩 j = (I * ) 𝐩 i d:i:Fin d𝐱 ⬝ᵥ 𝐩, 𝐩 i = j, 𝐱 j, 𝐩 i ∘SL 𝐩 j All goals completed! 🐙 simp_rw d:i:Fin d j, 𝐱 j, 𝐩 i ∘SL 𝐩 j = (I * ) 𝐩 id:i:Fin d x, ((I * ) δ[x,i] ContinuousLinearMap.id 𝓢(Space d, )) ∘SL 𝐩 x = (I * ) 𝐩 i d:i:Fin d x, (I * ) δ[x,i] ContinuousLinearMap.id 𝓢(Space d, ) ∘SL 𝐩 x = (I * ) 𝐩 i d:i:Fin d x, (I * ) δ[x,i] 𝐩 x = (I * ) 𝐩 i d:i:Fin d(I * ) x, δ[x,i] 𝐩 x = (I * ) 𝐩 i d:i:Fin d(I * ) x, δ[i,x] 𝐩 x = (I * ) 𝐩 i All goals completed! 🐙]d: i, 𝐱 i * 𝐩 i, 𝐩 ⬝ᵥ 𝐩 = i, 𝐱 i, 𝐩 ⬝ᵥ 𝐩 ∘SL 𝐩 i All goals completed! 🐙 simp_rw d: i, 𝐱 i, 𝐩 ⬝ᵥ 𝐩 ∘SL 𝐩 i = (2 * I * ) (𝐩 ⬝ᵥ 𝐩)d: x, ((2 * I * ) 𝐩 x) ∘SL 𝐩 x = (2 * I * ) (𝐩 ⬝ᵥ 𝐩) d: x, (2 * I * ) 𝐩 x ∘SL 𝐩 x = (2 * I * ) (𝐩 ⬝ᵥ 𝐩) d:(2 * I * ) x, 𝐩 x ∘SL 𝐩 x = (2 * I * ) (𝐩 ⬝ᵥ 𝐩) d:(2 * I * ) x, 𝐩 x ∘SL 𝐩 x = (2 * I * ) i, 𝐩 i * 𝐩 i All goals completed! 🐙]private lemma positionDotMomentum_commutation_radiusRegPow (d : ) (ε : ˣ) (s : ) : 𝐱[d] ⬝ᵥ 𝐩, 𝐫₀[d] ε s = (-s * I * ) (𝐫₀ ε s - ε.1 ^ 2 𝐫₀ ε (s-2)) := d:ε:ˣs:𝐱 ⬝ᵥ 𝐩, 𝐫₀ ε s = (-s * I * ) (𝐫₀ ε s - ε ^ 2 𝐫₀ ε (s - 2)) calc _ = i, 𝐱 i ∘L 𝐩 i, 𝐫₀ ε s := d:ε:ˣs:𝐱 ⬝ᵥ 𝐩, 𝐫₀ ε s = i, 𝐱 i ∘SL 𝐩 i, 𝐫₀ ε s All goals completed! 🐙 _ = (-s * I * ) ( i, 𝐱 i ∘L 𝐱 i) ∘L 𝐫₀ ε (s-2) := d:ε:ˣs: i, 𝐱 i ∘SL 𝐩 i, 𝐫₀ ε s = (-s * I * ) (∑ i, 𝐱 i ∘SL 𝐱 i) ∘SL 𝐫₀ ε (s - 2) All goals completed! 🐙 _ = (-s * I * ) (𝐫₀ ε s - ε.1 ^ 2 𝐫₀ ε (s-2)) := d:ε:ˣs:(-s * I * ) (∑ i, 𝐱 i ∘SL 𝐱 i) ∘SL 𝐫₀ ε (s - 2) = (-s * I * ) (𝐫₀ ε s - ε ^ 2 𝐫₀ ε (s - 2)) All goals completed! 🐙All goals completed! 🐙d:i:Fin dj:Fin d (k l : Fin d), 𝐱 k ∘SL (𝐩 ⬝ᵥ 𝐩), (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐩 l = (-I * ) (𝐱 k ∘SL 𝐩 l - δ[k,l] (𝐱 ⬝ᵥ 𝐩)) ∘SL (𝐩 ⬝ᵥ 𝐩) d:i:Fin dj:Fin dk:Fin dl:Fin d𝐱 k ∘SL (𝐩 ⬝ᵥ 𝐩), (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐩 l = (-I * ) (𝐱 k ∘SL 𝐩 l - δ[k,l] (𝐱 ⬝ᵥ 𝐩)) ∘SL (𝐩 ⬝ᵥ 𝐩) calc _ = (𝐱 ⬝ᵥ 𝐩) ∘L 𝐱 k, 𝐩 l ∘L (𝐩 ⬝ᵥ 𝐩) + 𝐱 k ∘L 𝐩[d] ⬝ᵥ 𝐩, 𝐱[d] ⬝ᵥ 𝐩 ∘L 𝐩 l + 𝐱 k, 𝐱[d] ⬝ᵥ 𝐩 ∘L (𝐩 ⬝ᵥ 𝐩) ∘L 𝐩 l := d:i:Fin dj:Fin dk:Fin dl:Fin d𝐱 k ∘SL (𝐩 ⬝ᵥ 𝐩), (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐩 l = (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 k, 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) + 𝐱 k ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 ⬝ᵥ 𝐩 ∘SL 𝐩 l + 𝐱 k, 𝐱 ⬝ᵥ 𝐩 ∘SL (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐩 l All goals completed! 🐙 _ = (𝐱 ⬝ᵥ 𝐩) ∘L 𝐱 k, 𝐩 l ∘L (𝐩 ⬝ᵥ 𝐩) + (-I * ) 𝐱 k ∘L 𝐩 l ∘L (𝐩 ⬝ᵥ 𝐩) := d:i:Fin dj:Fin dk:Fin dl:Fin d(𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 k, 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) + 𝐱 k ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 ⬝ᵥ 𝐩 ∘SL 𝐩 l + 𝐱 k, 𝐱 ⬝ᵥ 𝐩 ∘SL (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐩 l = (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 k, 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) + (-I * ) 𝐱 k ∘SL 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) d:i:Fin dj:Fin dk:Fin dl:Fin d(𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 k, 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) + (-2 * I * + - -I * ) 𝐱 k ∘SL 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) = (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 k, 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) + (-I * ) 𝐱 k ∘SL 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) All goals completed! 🐙 _ = (-I * ) (𝐱 k ∘L 𝐩 l - δ[k,l] (𝐱 ⬝ᵥ 𝐩)) ∘L (𝐩 ⬝ᵥ 𝐩) := d:i:Fin dj:Fin dk:Fin dl:Fin d(𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 k, 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) + (-I * ) 𝐱 k ∘SL 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) = (-I * ) (𝐱 k ∘SL 𝐩 l - δ[k,l] (𝐱 ⬝ᵥ 𝐩)) ∘SL (𝐩 ⬝ᵥ 𝐩) simp_rw d:i:Fin dj:Fin dk:Fin dl:Fin d(𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 k, 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) + (-I * ) 𝐱 k ∘SL 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) = (-I * ) (𝐱 k ∘SL 𝐩 l - δ[k,l] (𝐱 ⬝ᵥ 𝐩)) ∘SL (𝐩 ⬝ᵥ 𝐩)d:i:Fin dj:Fin dk:Fin dl:Fin d(𝐱 ⬝ᵥ 𝐩) ∘SL ((I * ) δ[k,l] ContinuousLinearMap.id 𝓢(Space d, )) ∘SL (𝐩 ⬝ᵥ 𝐩) + (-I * ) 𝐱 k ∘SL 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) = (-I * ) (𝐱 k ∘SL 𝐩 l - δ[k,l] (𝐱 ⬝ᵥ 𝐩)) ∘SL (𝐩 ⬝ᵥ 𝐩) d:i:Fin dj:Fin dk:Fin dl:Fin d(𝐱 ⬝ᵥ 𝐩) ∘SL ((I * ) δ[k,l] ContinuousLinearMap.id 𝓢(Space d, )) ∘SL (𝐩 ⬝ᵥ 𝐩) + (-I * ) 𝐱 k ∘SL 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) = (-I * ) ((𝐱 k ∘SL 𝐩 l) ∘SL (𝐩 ⬝ᵥ 𝐩) - (δ[k,l] (𝐱 ⬝ᵥ 𝐩)) ∘SL (𝐩 ⬝ᵥ 𝐩)) d:i:Fin dj:Fin dk:Fin dl:Fin d(𝐱 ⬝ᵥ 𝐩) ∘SL ((I * ) δ[k,l] ContinuousLinearMap.id 𝓢(Space d, )) ∘SL (𝐩 ⬝ᵥ 𝐩) + (-I * ) 𝐱 k ∘SL 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) = (-I * ) (𝐱 k ∘SL 𝐩 l) ∘SL (𝐩 ⬝ᵥ 𝐩) - (-I * ) (δ[k,l] (𝐱 ⬝ᵥ 𝐩)) ∘SL (𝐩 ⬝ᵥ 𝐩) d:i:Fin dj:Fin dk:Fin dl:Fin d(𝐱 ⬝ᵥ 𝐩) ∘SL ((I * ) δ[k,l] ContinuousLinearMap.id 𝓢(Space d, ) ∘SL (𝐩 ⬝ᵥ 𝐩)) + (-I * ) 𝐱 k ∘SL 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) = (-I * ) (𝐱 k ∘SL 𝐩 l) ∘SL (𝐩 ⬝ᵥ 𝐩) - (-I * ) δ[k,l] (𝐱 ⬝ᵥ 𝐩) ∘SL (𝐩 ⬝ᵥ 𝐩) d:i:Fin dj:Fin dk:Fin dl:Fin d(I * ) δ[k,l] (𝐱 ⬝ᵥ 𝐩) ∘SL ContinuousLinearMap.id 𝓢(Space d, ) ∘SL (𝐩 ⬝ᵥ 𝐩) + (-I * ) 𝐱 k ∘SL 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) = (-I * ) (𝐱 k ∘SL 𝐩 l) ∘SL (𝐩 ⬝ᵥ 𝐩) - (-I * ) δ[k,l] (𝐱 ⬝ᵥ 𝐩) ∘SL (𝐩 ⬝ᵥ 𝐩) d:i:Fin dj:Fin dk:Fin dl:Fin d(I * ) δ[k,l] (𝐱 ⬝ᵥ 𝐩) ∘SL (𝐩 ⬝ᵥ 𝐩) + (-I * ) 𝐱 k ∘SL 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) = (-I * ) (𝐱 k ∘SL 𝐩 l) ∘SL (𝐩 ⬝ᵥ 𝐩) - (-I * ) δ[k,l] (𝐱 ⬝ᵥ 𝐩) ∘SL (𝐩 ⬝ᵥ 𝐩) d:i:Fin dj:Fin dk:Fin dl:Fin d(I * ) δ[k,l] (𝐱 ⬝ᵥ 𝐩) ∘SL (𝐩 ⬝ᵥ 𝐩) + (-I * ) 𝐱 k ∘SL 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) = (-I * ) (𝐱 k ∘SL 𝐩 l) ∘SL (𝐩 ⬝ᵥ 𝐩) + -((-I * ) δ[k,l] (𝐱 ⬝ᵥ 𝐩) ∘SL (𝐩 ⬝ᵥ 𝐩)) d:i:Fin dj:Fin dk:Fin dl:Fin d(I * ) δ[k,l] (𝐱 ⬝ᵥ 𝐩) ∘SL (𝐩 ⬝ᵥ 𝐩) + (-I * ) 𝐱 k ∘SL 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) = (-I * ) (𝐱 k ∘SL 𝐩 l) ∘SL (𝐩 ⬝ᵥ 𝐩) + -(-I * ) δ[k,l] (𝐱 ⬝ᵥ 𝐩) ∘SL (𝐩 ⬝ᵥ 𝐩) d:i:Fin dj:Fin dk:Fin dl:Fin d(I * ) δ[k,l] (𝐱 ⬝ᵥ 𝐩) ∘SL (𝐩 ⬝ᵥ 𝐩) + -(I * ) 𝐱 k ∘SL 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) = -(I * ) (𝐱 k ∘SL 𝐩 l) ∘SL (𝐩 ⬝ᵥ 𝐩) + - -(I * ) δ[k,l] (𝐱 ⬝ᵥ 𝐩) ∘SL (𝐩 ⬝ᵥ 𝐩) d:i:Fin dj:Fin dk:Fin dl:Fin d(I * ) δ[k,l] (𝐱 ⬝ᵥ 𝐩) ∘SL (𝐩 ⬝ᵥ 𝐩) + -(I * ) 𝐱 k ∘SL 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) = -(I * ) (𝐱 k ∘SL 𝐩 l) ∘SL (𝐩 ⬝ᵥ 𝐩) + (I * ) δ[k,l] (𝐱 ⬝ᵥ 𝐩) ∘SL (𝐩 ⬝ᵥ 𝐩) d:i:Fin dj:Fin dk:Fin dl:Fin d(I * ) δ[k,l] (𝐱 ⬝ᵥ 𝐩) ∘SL (𝐩 ⬝ᵥ 𝐩) + -(I * ) 𝐱 k ∘SL 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) = -(I * ) 𝐱 k ∘SL 𝐩 l ∘SL (𝐩 ⬝ᵥ 𝐩) + (I * ) δ[k,l] (𝐱 ⬝ᵥ 𝐩) ∘SL (𝐩 ⬝ᵥ 𝐩) All goals completed! 🐙]private lemma positionDotMomentumCompMomentum_comm {d : } (i j : Fin d) : (𝐱 ⬝ᵥ 𝐩) ∘L 𝐩 i, (𝐱 ⬝ᵥ 𝐩) ∘L 𝐩 j = 0 := d:i:Fin dj:Fin d(𝐱 ⬝ᵥ 𝐩) ∘SL 𝐩 i, (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐩 j = 0 All goals completed! 🐙private lemma positionCompMomentumSqr_comm_momentum_add {d : } (i j : Fin d) : 𝐱 i ∘L (𝐩 ⬝ᵥ 𝐩), 𝐩 j + 𝐩 i, 𝐱 j ∘L (𝐩 ⬝ᵥ 𝐩) = 0 := d:i:Fin dj:Fin d𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩), 𝐩 j + 𝐩 i, 𝐱 j ∘SL (𝐩 ⬝ᵥ 𝐩) = 0 nth_rw 2 [d:i:Fin dj:Fin d𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩), 𝐩 j + -𝐱 j ∘SL (𝐩 ⬝ᵥ 𝐩), 𝐩 i = 0d:i:Fin dj:Fin d𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩), 𝐩 j + -𝐱 j ∘SL (𝐩 ⬝ᵥ 𝐩), 𝐩 i = 0 All goals completed! 🐙private lemma positionDotMomentumCompMomentum_comm_momentum_add {d : } (i j : Fin d) : (𝐱 ⬝ᵥ 𝐩) ∘L 𝐩 i, 𝐩 j + 𝐩 i, (𝐱 ⬝ᵥ 𝐩) ∘L 𝐩 j = 0 := d:i:Fin dj:Fin d(𝐱 ⬝ᵥ 𝐩) ∘SL 𝐩 i, 𝐩 j + 𝐩 i, (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐩 j = 0 nth_rw 2 [d:i:Fin dj:Fin d(𝐱 ⬝ᵥ 𝐩) ∘SL 𝐩 i, 𝐩 j + -(𝐱 ⬝ᵥ 𝐩) ∘SL 𝐩 j, 𝐩 i = 0d:i:Fin dj:Fin d(𝐱 ⬝ᵥ 𝐩) ∘SL 𝐩 i, 𝐩 j + -(𝐱 ⬝ᵥ 𝐩) ∘SL 𝐩 j, 𝐩 i = 0 All goals completed! 🐙d:ε:ˣi:Fin dj:Fin dA:𝓢(Space d, ) →L[] 𝓢(Space d, ) := 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1)hA:𝐱 i ∘SL A ∘SL 𝐱 j = 𝐱 j ∘SL A ∘SL 𝐱 i𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩), 𝐫₀ ε (-1) ∘SL 𝐱 j + 𝐫₀ ε (-1) ∘SL 𝐱 i, 𝐱 j ∘SL (𝐩 ⬝ᵥ 𝐩) = (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j calc _ = 𝐫₀ ε (-1) ∘L 𝐱 i ∘L 𝐩[d] ⬝ᵥ 𝐩, 𝐱 j + 𝐱 i ∘L A ∘L 𝐱 j - (𝐫₀ ε (-1) ∘L 𝐱 j ∘L 𝐩[d] ⬝ᵥ 𝐩, 𝐱 i + 𝐱 j ∘L A ∘L 𝐱 i) := d:ε:ˣi:Fin dj:Fin dA:𝓢(Space d, ) →L[] 𝓢(Space d, ) := 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1)hA:𝐱 i ∘SL A ∘SL 𝐱 j = 𝐱 j ∘SL A ∘SL 𝐱 i𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩), 𝐫₀ ε (-1) ∘SL 𝐱 j + 𝐫₀ ε (-1) ∘SL 𝐱 i, 𝐱 j ∘SL (𝐩 ⬝ᵥ 𝐩) = 𝐫₀ ε (-1) ∘SL 𝐱 i ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 j + 𝐱 i ∘SL A ∘SL 𝐱 j - (𝐫₀ ε (-1) ∘SL 𝐱 j ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 i + 𝐱 j ∘SL A ∘SL 𝐱 i) nth_rw 2 [d:ε:ˣi:Fin dj:Fin dA:𝓢(Space d, ) →L[] 𝓢(Space d, ) := 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1)hA:𝐱 i ∘SL A ∘SL 𝐱 j = 𝐱 j ∘SL A ∘SL 𝐱 i𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩), 𝐫₀ ε (-1) ∘SL 𝐱 j + -𝐱 j ∘SL (𝐩 ⬝ᵥ 𝐩), 𝐫₀ ε (-1) ∘SL 𝐱 i = 𝐫₀ ε (-1) ∘SL 𝐱 i ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 j + 𝐱 i ∘SL A ∘SL 𝐱 j - (𝐫₀ ε (-1) ∘SL 𝐱 j ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 i + 𝐱 j ∘SL A ∘SL 𝐱 i)d:ε:ˣi:Fin dj:Fin dA:𝓢(Space d, ) →L[] 𝓢(Space d, ) := 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1)hA:𝐱 i ∘SL A ∘SL 𝐱 j = 𝐱 j ∘SL A ∘SL 𝐱 i𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩), 𝐫₀ ε (-1) ∘SL 𝐱 j + -𝐱 j ∘SL (𝐩 ⬝ᵥ 𝐩), 𝐫₀ ε (-1) ∘SL 𝐱 i = 𝐫₀ ε (-1) ∘SL 𝐱 i ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 j + 𝐱 i ∘SL A ∘SL 𝐱 j - (𝐫₀ ε (-1) ∘SL 𝐱 j ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 i + 𝐱 j ∘SL A ∘SL 𝐱 i) simp_rw d:ε:ˣi:Fin dj:Fin dA:𝓢(Space d, ) →L[] 𝓢(Space d, ) := 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1)hA:𝐱 i ∘SL A ∘SL 𝐱 j = 𝐱 j ∘SL A ∘SL 𝐱 i𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩), 𝐫₀ ε (-1) ∘SL 𝐱 j + -𝐱 j ∘SL (𝐩 ⬝ᵥ 𝐩), 𝐫₀ ε (-1) ∘SL 𝐱 i = 𝐫₀ ε (-1) ∘SL 𝐱 i ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 j + 𝐱 i ∘SL A ∘SL 𝐱 j - (𝐫₀ ε (-1) ∘SL 𝐱 j ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 i + 𝐱 j ∘SL A ∘SL 𝐱 i)d:ε:ˣi:Fin dj:Fin dA:𝓢(Space d, ) →L[] 𝓢(Space d, ) := 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1)hA:𝐱 i ∘SL A ∘SL 𝐱 j = 𝐱 j ∘SL A ∘SL 𝐱 i𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩), 𝐫₀ ε (-1) ∘SL 𝐱 j - 𝐱 j ∘SL (𝐩 ⬝ᵥ 𝐩), 𝐫₀ ε (-1) ∘SL 𝐱 i = 𝐫₀ ε (-1) ∘SL 𝐱 i ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 j + 𝐱 i ∘SL A ∘SL 𝐱 j - (𝐫₀ ε (-1) ∘SL 𝐱 j ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 i + 𝐱 j ∘SL A ∘SL 𝐱 i) d:ε:ˣi:Fin dj:Fin dA:𝓢(Space d, ) →L[] 𝓢(Space d, ) := 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1)hA:𝐱 i ∘SL A ∘SL 𝐱 j = 𝐱 j ∘SL A ∘SL 𝐱 i𝐫₀ ε (-1) ∘SL 𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩), 𝐱 j + 𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩), 𝐫₀ ε (-1) ∘SL 𝐱 j - (𝐫₀ ε (-1) ∘SL 𝐱 j ∘SL (𝐩 ⬝ᵥ 𝐩), 𝐱 i + 𝐱 j ∘SL (𝐩 ⬝ᵥ 𝐩), 𝐫₀ ε (-1) ∘SL 𝐱 i) = 𝐫₀ ε (-1) ∘SL 𝐱 i ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 j + 𝐱 i ∘SL A ∘SL 𝐱 j - (𝐫₀ ε (-1) ∘SL 𝐱 j ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 i + 𝐱 j ∘SL A ∘SL 𝐱 i) d:ε:ˣi:Fin dj:Fin dA:𝓢(Space d, ) →L[] 𝓢(Space d, ) := 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1)hA:𝐱 i ∘SL A ∘SL 𝐱 j = 𝐱 j ∘SL A ∘SL 𝐱 i𝐫₀ ε (-1) ∘SL (𝐱 i ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 j + 𝐱 i, 𝐱 j ∘SL (𝐩 ⬝ᵥ 𝐩)) + (𝐱 i ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1) + 𝐱 i, 𝐫₀ ε (-1) ∘SL (𝐩 ⬝ᵥ 𝐩)) ∘SL 𝐱 j - (𝐫₀ ε (-1) ∘SL (𝐱 j ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 i + 𝐱 j, 𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩)) + (𝐱 j ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1) + 𝐱 j, 𝐫₀ ε (-1) ∘SL (𝐩 ⬝ᵥ 𝐩)) ∘SL 𝐱 i) = 𝐫₀ ε (-1) ∘SL 𝐱 i ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 j + 𝐱 i ∘SL A ∘SL 𝐱 j - (𝐫₀ ε (-1) ∘SL 𝐱 j ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 i + 𝐱 j ∘SL A ∘SL 𝐱 i) d:ε:ˣi:Fin dj:Fin dA:𝓢(Space d, ) →L[] 𝓢(Space d, ) := 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1)hA:𝐱 i ∘SL A ∘SL 𝐱 j = 𝐱 j ∘SL A ∘SL 𝐱 i𝐫₀ ε (-1) ∘SL (𝐱 i ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 j + 𝐱 i, 𝐱 j ∘SL (𝐩 ⬝ᵥ 𝐩)) + (𝐱 i ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1) + 𝐱 i, 𝐫₀ ε (-1) ∘SL (𝐩 ⬝ᵥ 𝐩)) ∘SL 𝐱 j - 𝐫₀ ε (-1) ∘SL (𝐱 j ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 i + 𝐱 j, 𝐱 i ∘SL (𝐩 ⬝ᵥ 𝐩)) - (𝐱 j ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1) + 𝐱 j, 𝐫₀ ε (-1) ∘SL (𝐩 ⬝ᵥ 𝐩)) ∘SL 𝐱 i = 𝐫₀ ε (-1) ∘SL 𝐱 i ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 j + 𝐱 i ∘SL A ∘SL 𝐱 j - 𝐫₀ ε (-1) ∘SL 𝐱 j ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 i - 𝐱 j ∘SL A ∘SL 𝐱 i] All goals completed! 🐙 _ = 𝐫₀ ε (-1) ∘L (𝐱 i ∘L 𝐩[d] ⬝ᵥ 𝐩, 𝐱 j - 𝐱 j ∘L 𝐩[d] ⬝ᵥ 𝐩, 𝐱 i) := d:ε:ˣi:Fin dj:Fin dA:𝓢(Space d, ) →L[] 𝓢(Space d, ) := 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1)hA:𝐱 i ∘SL A ∘SL 𝐱 j = 𝐱 j ∘SL A ∘SL 𝐱 i𝐫₀ ε (-1) ∘SL 𝐱 i ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 j + 𝐱 i ∘SL A ∘SL 𝐱 j - (𝐫₀ ε (-1) ∘SL 𝐱 j ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 i + 𝐱 j ∘SL A ∘SL 𝐱 i) = 𝐫₀ ε (-1) ∘SL (𝐱 i ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 j - 𝐱 j ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 i) All goals completed! 🐙 _ = (-2 * I * ) 𝐫₀ ε (-1) ∘L 𝐋 i j := d:ε:ˣi:Fin dj:Fin dA:𝓢(Space d, ) →L[] 𝓢(Space d, ) := 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1)hA:𝐱 i ∘SL A ∘SL 𝐱 j = 𝐱 j ∘SL A ∘SL 𝐱 i𝐫₀ ε (-1) ∘SL (𝐱 i ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 j - 𝐱 j ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 i) = (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j simp_rw d:ε:ˣi:Fin dj:Fin dA:𝓢(Space d, ) →L[] 𝓢(Space d, ) := 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1)hA:𝐱 i ∘SL A ∘SL 𝐱 j = 𝐱 j ∘SL A ∘SL 𝐱 i𝐫₀ ε (-1) ∘SL (𝐱 i ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 j - 𝐱 j ∘SL 𝐩 ⬝ᵥ 𝐩, 𝐱 i) = (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i jd:ε:ˣi:Fin dj:Fin dA:𝓢(Space d, ) →L[] 𝓢(Space d, ) := 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1)hA:𝐱 i ∘SL A ∘SL 𝐱 j = 𝐱 j ∘SL A ∘SL 𝐱 i𝐫₀ ε (-1) ∘SL (𝐱 i ∘SL (-𝐱 j, 𝐩 ⬝ᵥ 𝐩) - 𝐱 j ∘SL (-𝐱 i, 𝐩 ⬝ᵥ 𝐩)) = (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j d:ε:ˣi:Fin dj:Fin dA:𝓢(Space d, ) →L[] 𝓢(Space d, ) := 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1)hA:𝐱 i ∘SL A ∘SL 𝐱 j = 𝐱 j ∘SL A ∘SL 𝐱 i𝐫₀ ε (-1) ∘SL (𝐱 i ∘SL (-((2 * I * ) 𝐩 j)) - 𝐱 j ∘SL (-((2 * I * ) 𝐩 i))) = (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j d:ε:ˣi:Fin dj:Fin dA:𝓢(Space d, ) →L[] 𝓢(Space d, ) := 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1)hA:𝐱 i ∘SL A ∘SL 𝐱 j = 𝐱 j ∘SL A ∘SL 𝐱 i𝐫₀ ε (-1) ∘SL (-𝐱 i ∘SL ((2 * I * ) 𝐩 j) - -𝐱 j ∘SL ((2 * I * ) 𝐩 i)) = (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j d:ε:ˣi:Fin dj:Fin dA:𝓢(Space d, ) →L[] 𝓢(Space d, ) := 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1)hA:𝐱 i ∘SL A ∘SL 𝐱 j = 𝐱 j ∘SL A ∘SL 𝐱 i𝐫₀ ε (-1) ∘SL (-((2 * I * ) 𝐱 i ∘SL 𝐩 j) - -((2 * I * ) 𝐱 j ∘SL 𝐩 i)) = (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j d:ε:ˣi:Fin dj:Fin dA:𝓢(Space d, ) →L[] 𝓢(Space d, ) := 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1)hA:𝐱 i ∘SL A ∘SL 𝐱 j = 𝐱 j ∘SL A ∘SL 𝐱 i𝐫₀ ε (-1) ∘SL (-(2 * I * ) 𝐱 i ∘SL 𝐩 j - -(2 * I * ) 𝐱 j ∘SL 𝐩 i) = (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j d:ε:ˣi:Fin dj:Fin dA:𝓢(Space d, ) →L[] 𝓢(Space d, ) := 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1)hA:𝐱 i ∘SL A ∘SL 𝐱 j = 𝐱 j ∘SL A ∘SL 𝐱 i𝐫₀ ε (-1) ∘SL ((-2 * I * ) 𝐱 i ∘SL 𝐩 j - (-2 * I * ) 𝐱 j ∘SL 𝐩 i) = (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j d:ε:ˣi:Fin dj:Fin dA:𝓢(Space d, ) →L[] 𝓢(Space d, ) := 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1)hA:𝐱 i ∘SL A ∘SL 𝐱 j = 𝐱 j ∘SL A ∘SL 𝐱 i𝐫₀ ε (-1) ∘SL ((-2 * I * ) (𝐱 i ∘SL 𝐩 j - 𝐱 j ∘SL 𝐩 i)) = (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j d:ε:ˣi:Fin dj:Fin dA:𝓢(Space d, ) →L[] 𝓢(Space d, ) := 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1)hA:𝐱 i ∘SL A ∘SL 𝐱 j = 𝐱 j ∘SL A ∘SL 𝐱 i(-2 * I * ) 𝐫₀ ε (-1) ∘SL (𝐱 i ∘SL 𝐩 j - 𝐱 j ∘SL 𝐩 i) = (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j All goals completed! 🐙]private lemma momentum_comm_radiusRegPow_position_symm {d : } (ε : ˣ) (s : ) (i j : Fin d) : 𝐩 i, 𝐫₀ ε s ∘L 𝐱 j = 𝐩 j, 𝐫₀ ε s ∘L 𝐱 i := d:ε:ˣs:i:Fin dj:Fin d𝐩 i, 𝐫₀ ε s ∘SL 𝐱 j = 𝐩 j, 𝐫₀ ε s ∘SL 𝐱 i All goals completed! 🐙d:ε:ˣi:Fin dj:Fin d (k : Fin d), 𝐱 ⬝ᵥ 𝐩, 𝐫₀ ε (-1) ∘SL 𝐱 k = (-I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐱 k d:ε:ˣi:Fin dj:Fin dk:Fin d𝐱 ⬝ᵥ 𝐩, 𝐫₀ ε (-1) ∘SL 𝐱 k = (-I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐱 k calc _ = -(I * ) (ε.1 ^ 2) 𝐫₀ ε (-1-2) ∘L 𝐱 k := d:ε:ˣi:Fin dj:Fin dk:Fin d𝐱 ⬝ᵥ 𝐩, 𝐫₀ ε (-1) ∘SL 𝐱 k = -(I * ) ε ^ 2 𝐫₀ ε (-1 - 2) ∘SL 𝐱 k All goals completed! 🐙 _ = (-I * * ε.1 ^ 2) 𝐫₀ ε (-3) ∘L 𝐱 k := d:ε:ˣi:Fin dj:Fin dk:Fin d-(I * ) ε ^ 2 𝐫₀ ε (-1 - 2) ∘SL 𝐱 k = (-I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐱 k d:ε:ˣi:Fin dj:Fin dk:Fin d(-(I * ) * ε ^ 2) 𝐫₀ ε (-1 - 2) ∘SL 𝐱 k = (-I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐱 k All goals completed! 🐙All goals completed! 🐙private lemma radiusRegInvCompPosition_comm {d : } (ε : ˣ) (i j : Fin d) : 𝐫₀ ε (-1) ∘L 𝐱 i, 𝐫₀ ε (-1) ∘L 𝐱 j = 0 := d:ε:ˣi:Fin dj:Fin d𝐫₀ ε (-1) ∘SL 𝐱 i, 𝐫₀ ε (-1) ∘SL 𝐱 j = 0 All goals completed! 🐙

⁅𝐀(ε)ᵢ, 𝐀(ε)ⱼ⁆ = (-2iℏm·𝐇(ε) + iℏmkε²·𝐫(ε)⁻³)𝐋ᵢⱼ

H:HydrogenAtomε:ˣi:Fin H.dj:Fin H.dc₁: := 2⁻¹ * I * * (H.d - 1)c₂: := H.m * H.k(-2 * I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j + 0 + c₂ ^ 2 0 - (-I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j + c₁ 0 - c₂ (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j - c₁ 0 + c₂ (I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐋 i j - (c₁ * c₂) 0 = ((-2 * I * * H.m) H.hamiltonianRegCLM ε + (I * * H.m * H.k * ε ^ 2) 𝐫₀ ε (-3)) ∘SL 𝐋 i j H:HydrogenAtomε:ˣi:Fin H.dj:Fin H.d(-2 * I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j + 0 + (H.m * H.k) ^ 2 0 - (-I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j + (2⁻¹ * I * * (H.d - 1)) 0 - (H.m * H.k) (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j - (2⁻¹ * I * * (H.d - 1)) 0 + (H.m * H.k) (I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐋 i j - (2⁻¹ * I * * (H.d - 1) * (H.m * H.k)) 0 = ((-2 * I * * H.m) H.hamiltonianRegCLM ε + (I * * H.m * H.k * ε ^ 2) 𝐫₀ ε (-3)) ∘SL 𝐋 i j simp_rw H:HydrogenAtomε:ˣi:Fin H.dj:Fin H.d(-2 * I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j + 0 + (H.m * H.k) ^ 2 0 - (-I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j + (2⁻¹ * I * * (H.d - 1)) 0 - (H.m * H.k) (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j - (2⁻¹ * I * * (H.d - 1)) 0 + (H.m * H.k) (I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐋 i j - (2⁻¹ * I * * (H.d - 1) * (H.m * H.k)) 0 = ((-2 * I * * H.m) H.hamiltonianRegCLM ε + (I * * H.m * H.k * ε ^ 2) 𝐫₀ ε (-3)) ∘SL 𝐋 i jH:HydrogenAtomε:ˣi:Fin H.dj:Fin H.d(-2 * I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j + 0 + (H.m * H.k) ^ 2 0 - (-I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j + (2⁻¹ * I * * (H.d - 1)) 0 - (H.m * H.k) (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j - (2⁻¹ * I * * (H.d - 1)) 0 + (H.m * H.k) (I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐋 i j - (2⁻¹ * I * * (H.d - 1) * (H.m * H.k)) 0 = ((-2 * I * * H.m) ((2 * H.m)⁻¹ (𝐩 ⬝ᵥ 𝐩) - H.k 𝐫₀ ε (-1)) + (I * * H.m * H.k * ε ^ 2) 𝐫₀ ε (-3)) ∘SL 𝐋 i j H:HydrogenAtomε:ˣi:Fin H.dj:Fin H.d(-2 * I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j + 0 + 0 - (-I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j + 0 - (H.m * H.k) (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j - 0 + (H.m * H.k) (I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐋 i j - 0 = ((-2 * I * * H.m) ((2 * H.m)⁻¹ (𝐩 ⬝ᵥ 𝐩) - H.k 𝐫₀ ε (-1)) + (I * * H.m * H.k * ε ^ 2) 𝐫₀ ε (-3)) ∘SL 𝐋 i j H:HydrogenAtomε:ˣi:Fin H.dj:Fin H.d(-2 * I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j - (-I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j - (H.m * H.k) (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j - 0 + (H.m * H.k) (I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐋 i j - 0 = ((-2 * I * * H.m) ((2 * H.m)⁻¹ (𝐩 ⬝ᵥ 𝐩) - H.k 𝐫₀ ε (-1)) + (I * * H.m * H.k * ε ^ 2) 𝐫₀ ε (-3)) ∘SL 𝐋 i j H:HydrogenAtomε:ˣi:Fin H.dj:Fin H.d(-2 * I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j - (-I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j - (H.m * H.k) (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j + (H.m * H.k) (I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐋 i j = ((-2 * I * * H.m) ((2 * H.m)⁻¹ (𝐩 ⬝ᵥ 𝐩) - H.k 𝐫₀ ε (-1)) + (I * * H.m * H.k * ε ^ 2) 𝐫₀ ε (-3)) ∘SL 𝐋 i j H:HydrogenAtomε:ˣi:Fin H.dj:Fin H.d(-2 * I * - -I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j - (H.m * H.k) (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j + (H.m * H.k) (I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐋 i j = ((-2 * I * * H.m) ((2 * H.m)⁻¹ (𝐩 ⬝ᵥ 𝐩) - H.k 𝐫₀ ε (-1)) + (I * * H.m * H.k * ε ^ 2) 𝐫₀ ε (-3)) ∘SL 𝐋 i j H:HydrogenAtomε:ˣi:Fin H.dj:Fin H.d(-2 * I * - -I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j - (H.m * H.k) (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j + (H.m * H.k) (I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐋 i j = ((-2 * I * * H.m) ((2 * H.m)⁻¹ (𝐩 ⬝ᵥ 𝐩) - H.k 𝐫₀ ε (-1)) + (I * * H.m * H.k * ε ^ 2) 𝐫₀ ε (-3)) ∘SL 𝐋 i j H:HydrogenAtomε:ˣi:Fin H.dj:Fin H.d(-2 * I * - -I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j - (H.m * H.k) (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j + (H.m * H.k) (I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐋 i j = ((-2 * I * * H.m) ((↑(2 * H.m))⁻¹ (𝐩 ⬝ᵥ 𝐩) - H.k 𝐫₀ ε (-1)) + (I * * H.m * H.k * ε ^ 2) 𝐫₀ ε (-3)) ∘SL 𝐋 i j H:HydrogenAtomε:ˣi:Fin H.dj:Fin H.d(-2 * I * - -I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j - (H.m * H.k) (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j + (H.m * H.k) (I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐋 i j = ((-2 * I * * H.m) ((2 * H.m)⁻¹ (𝐩 ⬝ᵥ 𝐩) - H.k 𝐫₀ ε (-1)) + (I * * H.m * H.k * ε ^ 2) 𝐫₀ ε (-3)) ∘SL 𝐋 i j H:HydrogenAtomε:ˣi:Fin H.dj:Fin H.d(-2 * I * - -I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j - (H.m * H.k) (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j + (H.m * H.k) (I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐋 i j = ((-2 * I * * H.m) ((2 * H.m)⁻¹ (𝐩 ⬝ᵥ 𝐩) - H.k 𝐫₀ ε (-1)) + (I * * H.m * H.k * ε ^ 2) 𝐫₀ ε (-3)) ∘SL 𝐋 i j H:HydrogenAtomε:ˣi:Fin H.dj:Fin H.d(-2 * I * - -I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j - (H.m * H.k) (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐋 i j + (H.m * H.k) (I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐋 i j = ((-2 * I * * H.m) (2 * H.m)⁻¹ (𝐩 ⬝ᵥ 𝐩) - (-2 * I * * H.m) H.k 𝐫₀ ε (-1) + (I * * H.m * H.k * ε ^ 2) 𝐫₀ ε (-3)) ∘SL 𝐋 i j H:HydrogenAtomε:ˣi:Fin H.dj:Fin H.d(-2 * I * - -I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j - (H.m * H.k * (-2 * I * )) 𝐫₀ ε (-1) ∘SL 𝐋 i j + (H.m * H.k * (I * * ε ^ 2)) 𝐫₀ ε (-3) ∘SL 𝐋 i j = ((-2 * I * * H.m * (2 * H.m)⁻¹) (𝐩 ⬝ᵥ 𝐩) - (-2 * I * * H.m * H.k) 𝐫₀ ε (-1) + (I * * H.m * H.k * ε ^ 2) 𝐫₀ ε (-3)) ∘SL 𝐋 i j H:HydrogenAtomε:ˣi:Fin H.dj:Fin H.d(-2 * I * - -I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j - (H.m * H.k * (-2 * I * )) 𝐫₀ ε (-1) ∘SL 𝐋 i j + (H.m * H.k * (I * * ε ^ 2)) 𝐫₀ ε (-3) ∘SL 𝐋 i j = ((-2 * I * * H.m * (2 * H.m)⁻¹) (𝐩 ⬝ᵥ 𝐩) - (-2 * I * * H.m * H.k) 𝐫₀ ε (-1)) ∘SL 𝐋 i j + ((I * * H.m * H.k * ε ^ 2) 𝐫₀ ε (-3)) ∘SL 𝐋 i j H:HydrogenAtomε:ˣi:Fin H.dj:Fin H.d(-2 * I * - -I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j - (H.m * H.k * (-2 * I * )) 𝐫₀ ε (-1) ∘SL 𝐋 i j + (H.m * H.k * (I * * ε ^ 2)) 𝐫₀ ε (-3) ∘SL 𝐋 i j = ((-2 * I * * H.m * (2 * H.m)⁻¹) (𝐩 ⬝ᵥ 𝐩)) ∘SL 𝐋 i j - ((-2 * I * * H.m * H.k) 𝐫₀ ε (-1)) ∘SL 𝐋 i j + ((I * * H.m * H.k * ε ^ 2) 𝐫₀ ε (-3)) ∘SL 𝐋 i j H:HydrogenAtomε:ˣi:Fin H.dj:Fin H.d(-2 * I * - -I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j - (H.m * H.k * (-2 * I * )) 𝐫₀ ε (-1) ∘SL 𝐋 i j + (H.m * H.k * (I * * ε ^ 2)) 𝐫₀ ε (-3) ∘SL 𝐋 i j = (-2 * I * * H.m * (2 * H.m)⁻¹) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j - (-2 * I * * H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐋 i j + (I * * H.m * H.k * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐋 i j] H:HydrogenAtomε:ˣi:Fin H.dj:Fin H.d-(I * ) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j - -(I * * H.m * H.k * 2) 𝐫₀ ε (-1) ∘SL 𝐋 i j + (I * * H.m * H.k * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐋 i j = -(I * * H.m * (↑H.m)⁻¹) (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j - -(I * * H.m * H.k * 2) 𝐫₀ ε (-1) ∘SL 𝐋 i j + (I * * H.m * H.k * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐋 i j All goals completed! 🐙
/- ## Hamiltonian / LRL vector commutators -/ private lemma pSqr_comm_pL_Lp {d : } (i : Fin d) : 𝐩[d] ⬝ᵥ 𝐩, 𝐩 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐩 = 0 := d:i:Fin d𝐩 ⬝ᵥ 𝐩, 𝐩 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐩 = 0 d:i:Fin d𝐩 ⬝ᵥ 𝐩, j, 𝐩 j ∘SL 𝐋 i j + j, 𝐋 i j ∘SL 𝐩 j = 0 All goals completed! 🐙private lemma r_comm_rx {d : } (ε : ˣ) (i : Fin d) : 𝐫₀[d] ε (-1), 𝐫₀ ε (-1) ∘L 𝐱 i = 0 := d:ε:ˣi:Fin d𝐫₀ ε (-1), 𝐫₀ ε (-1) ∘SL 𝐱 i = 0 All goals completed! 🐙private lemma xL_Lx_eq {d : } (ε : ˣ) (i : Fin d) : 𝐱 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐱 = (2 : ) (𝐱 ⬝ᵥ 𝐩) ∘L 𝐱 i + (-I * * (d - 3)) 𝐱 i + ((-2 : ) 𝐫₀ ε 2 ∘L 𝐩 i + (2 * ε.1 ^ 2 : ) 𝐩 i) := d:ε:ˣi:Fin d𝐱 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐱 = 2 (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) -- Change summand simp_rw d:ε:ˣi:Fin d𝐱 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐱 = 2 (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)d:ε:ˣi:Fin d i_1, 𝐱 i_1 * 𝐋 i i_1 + i_1, 𝐋 i i_1 * 𝐱 i_1 = 2 (∑ i, 𝐱 i * 𝐩 i) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, 𝐱 x ∘SL 𝐋 i x + x, 𝐋 i x ∘SL 𝐱 x = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (𝐱 x ∘SL 𝐋 i x + 𝐋 i x ∘SL 𝐱 x) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (𝐱 x ∘SL (𝐱 i ∘SL 𝐩 x - 𝐱 x ∘SL 𝐩 i) + (𝐱 i ∘SL 𝐩 x - 𝐱 x ∘SL 𝐩 i) ∘SL 𝐱 x) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (𝐱 x ∘SL 𝐱 i ∘SL 𝐩 x - 𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i + (𝐱 i ∘SL 𝐩 x - 𝐱 x ∘SL 𝐩 i) ∘SL 𝐱 x) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (𝐱 x ∘SL 𝐱 i ∘SL 𝐩 x - 𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i + ((𝐱 i ∘SL 𝐩 x) ∘SL 𝐱 x - (𝐱 x ∘SL 𝐩 i) ∘SL 𝐱 x)) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (𝐱 x ∘SL 𝐱 i ∘SL 𝐩 x - 𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i + (𝐱 i ∘SL 𝐩 x ∘SL 𝐱 x - 𝐱 x ∘SL 𝐩 i ∘SL 𝐱 x)) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (𝐱 x ∘SL 𝐱 i ∘SL 𝐩 x + 𝐱 i ∘SL 𝐩 x ∘SL 𝐱 x - (𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i + 𝐱 x ∘SL 𝐩 i ∘SL 𝐱 x)) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (𝐱 x ∘SL 𝐱 i ∘SL 𝐩 x + 𝐱 i ∘SL (𝐱 x ∘SL 𝐩 x - (I * ) δ[x,x] ContinuousLinearMap.id 𝓢(Space d, )) - (𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i + 𝐱 x ∘SL (𝐱 x ∘SL 𝐩 i - (I * ) δ[x,i] ContinuousLinearMap.id 𝓢(Space d, )))) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (𝐱 x ∘SL 𝐱 i ∘SL 𝐩 x + (𝐱 i ∘SL 𝐱 x ∘SL 𝐩 x - 𝐱 i ∘SL ((I * ) δ[x,x] ContinuousLinearMap.id 𝓢(Space d, ))) - (𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i + (𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i - 𝐱 x ∘SL ((I * ) δ[x,i] ContinuousLinearMap.id 𝓢(Space d, ))))) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (𝐱 x ∘SL 𝐱 i ∘SL 𝐩 x + (𝐱 i ∘SL 𝐱 x ∘SL 𝐩 x - (I * ) δ[x,x] 𝐱 i ∘SL ContinuousLinearMap.id 𝓢(Space d, )) - (𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i + (𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i - (I * ) δ[x,i] 𝐱 x ∘SL ContinuousLinearMap.id 𝓢(Space d, )))) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (𝐱 x ∘SL 𝐱 i ∘SL 𝐩 x + (𝐱 i ∘SL 𝐱 x ∘SL 𝐩 x - (I * ) δ[x,x] 𝐱 i) - (𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i + (𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i - (I * ) δ[x,i] 𝐱 x))) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, ((𝐱 x ∘SL 𝐱 i) ∘SL 𝐩 x + ((𝐱 i ∘SL 𝐱 x) ∘SL 𝐩 x - (I * ) δ[x,x] 𝐱 i) - ((𝐱 x ∘SL 𝐱 x) ∘SL 𝐩 i + ((𝐱 x ∘SL 𝐱 x) ∘SL 𝐩 i - (I * ) δ[x,i] 𝐱 x))) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, ((𝐱 x ∘SL 𝐱 i) ∘SL 𝐩 x + ((𝐱 x ∘SL 𝐱 i) ∘SL 𝐩 x - (I * ) δ[x,x] 𝐱 i) - ((𝐱 x ∘SL 𝐱 x) ∘SL 𝐩 i + ((𝐱 x ∘SL 𝐱 x) ∘SL 𝐩 i - (I * ) δ[x,i] 𝐱 x))) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, ((𝐱 x ∘SL 𝐱 i) ∘SL 𝐩 x + (𝐱 x ∘SL 𝐱 i) ∘SL 𝐩 x - (I * ) δ[x,x] 𝐱 i - ((𝐱 x ∘SL 𝐱 x) ∘SL 𝐩 i + (𝐱 x ∘SL 𝐱 x) ∘SL 𝐩 i - (I * ) δ[x,i] 𝐱 x)) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (2 (𝐱 x ∘SL 𝐱 i) ∘SL 𝐩 x - (I * ) δ[x,x] 𝐱 i - (2 (𝐱 x ∘SL 𝐱 x) ∘SL 𝐩 i - (I * ) δ[x,i] 𝐱 x)) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (2 (𝐱 x ∘SL 𝐱 i) ∘SL 𝐩 x - (I * ) δ[x,x] 𝐱 i + (I * ) δ[x,i] 𝐱 x - 2 (𝐱 x ∘SL 𝐱 x) ∘SL 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (2 (𝐱 x ∘SL 𝐱 i) ∘SL 𝐩 x + (I * ) δ[x,i] 𝐱 x - (I * ) δ[x,x] 𝐱 i - 2 (𝐱 x ∘SL 𝐱 x) ∘SL 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (2 𝐱 x ∘SL 𝐱 i ∘SL 𝐩 x + (I * ) δ[x,i] 𝐱 x - (I * ) δ[x,x] 𝐱 i - 2 𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (2 𝐱 x ∘SL (𝐩 x ∘SL 𝐱 i + 𝐱 i, 𝐩 x) + (I * ) δ[x,i] 𝐱 x - (I * ) δ[x,x] 𝐱 i - 2 𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (2 𝐱 x ∘SL (𝐩 x ∘SL 𝐱 i + (I * ) δ[i,x] ContinuousLinearMap.id 𝓢(Space d, )) + (I * ) δ[x,i] 𝐱 x - (I * ) δ[x,x] 𝐱 i - 2 𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (2 𝐱 x ∘SL (𝐩 x ∘SL 𝐱 i + (I * ) δ[i,x] ContinuousLinearMap.id 𝓢(Space d, )) + (I * ) δ[i,x] 𝐱 x - (I * ) δ[x,x] 𝐱 i - 2 𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (2 (𝐱 x ∘SL 𝐩 x ∘SL 𝐱 i + 𝐱 x ∘SL ((I * ) δ[i,x] ContinuousLinearMap.id 𝓢(Space d, ))) + (I * ) δ[i,x] 𝐱 x - (I * ) δ[x,x] 𝐱 i - 2 𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (2 (𝐱 x ∘SL 𝐩 x ∘SL 𝐱 i + (I * ) δ[i,x] 𝐱 x ∘SL ContinuousLinearMap.id 𝓢(Space d, )) + (I * ) δ[i,x] 𝐱 x - (I * ) δ[x,x] 𝐱 i - 2 𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (2 𝐱 x ∘SL 𝐩 x ∘SL 𝐱 i + 2 (I * ) δ[i,x] 𝐱 x ∘SL ContinuousLinearMap.id 𝓢(Space d, ) + (I * ) δ[i,x] 𝐱 x - (I * ) δ[x,x] 𝐱 i - 2 𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (2 𝐱 x ∘SL 𝐩 x ∘SL 𝐱 i + 2 (I * ) δ[i,x] 𝐱 x + (I * ) δ[i,x] 𝐱 x - (I * ) δ[x,x] 𝐱 i - 2 𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d x, (2 𝐱 x ∘SL 𝐩 x ∘SL 𝐱 i + (2 (I * ) δ[i,x] 𝐱 x + (I * ) δ[i,x] 𝐱 x) - (I * ) δ[x,x] 𝐱 i - 2 𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) d:ε:ˣi:Fin d x, (2 𝐱 x ∘SL 𝐩 x ∘SL 𝐱 i + (2 (I * ) δ[i,x] 𝐱 x + (I * ) δ[i,x] 𝐱 x) - (I * ) δ[x,x] 𝐱 i - 2 𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) d:ε:ˣi:Fin d x, (2 𝐱 x ∘SL 𝐩 x ∘SL 𝐱 i + ((2 * (I * )) δ[i,x] 𝐱 x + (I * ) δ[i,x] 𝐱 x) - (I * ) δ[x,x] 𝐱 i - 2 𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) d:ε:ˣi:Fin d x, (2 𝐱 x ∘SL 𝐩 x ∘SL 𝐱 i + (2 * (I * ) + I * ) δ[i,x] 𝐱 x - (I * ) δ[x,x] 𝐱 i - 2 𝐱 x ∘SL 𝐱 x ∘SL 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) d:ε:ˣi:Fin d x, (2 (𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (2 * (I * ) + I * ) δ[i,x] 𝐱 x - (I * ) δ[x,x] 𝐱 i - 2 (𝐱 x ∘SL 𝐱 x) ∘SL 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) d:ε:ˣi:Fin d x, (2 (𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (2 * (I * ) + I * ) δ[i,x] 𝐱 x - (I * ) 1 𝐱 i - 2 (𝐱 x ∘SL 𝐱 x) ∘SL 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) d:ε:ˣi:Fin d x, (2 (𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (2 * (I * ) + I * ) δ[i,x] 𝐱 x - (I * ) 𝐱 i - 2 (𝐱 x ∘SL 𝐱 x) ∘SL 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i))] -- Split/do sums simp_rw d:ε:ˣi:Fin d x, (2 (𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (2 * (I * ) + I * ) δ[i,x] 𝐱 x - (I * ) 𝐱 i - 2 (𝐱 x ∘SL 𝐱 x) ∘SL 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i))d:ε:ˣi:Fin d x, (2 (𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (2 * (I * ) + I * ) δ[i,x] 𝐱 x) - x, (I * ) 𝐱 i - x, 2 (𝐱 x ∘SL 𝐱 x) ∘SL 𝐩 i = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) d:ε:ˣi:Fin d x, 2 (𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + x, (2 * (I * ) + I * ) δ[i,x] 𝐱 x - x, (I * ) 𝐱 i - x, 2 (𝐱 x ∘SL 𝐱 x) ∘SL 𝐩 i = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) d:ε:ˣi:Fin d2 x, (𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + (2 * (I * ) + I * ) x, δ[i,x] 𝐱 x - (I * ) x, 𝐱 i - 2 x, (𝐱 x ∘SL 𝐱 x) ∘SL 𝐩 i = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) d:ε:ˣi:Fin d2 (∑ i, 𝐱 i ∘SL 𝐩 i) ∘SL 𝐱 i + (2 * (I * ) + I * ) x, δ[i,x] 𝐱 x - (I * ) x, 𝐱 i - 2 (∑ i, 𝐱 i ∘SL 𝐱 i) ∘SL 𝐩 i = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) d:ε:ˣi:Fin d2 (∑ i, 𝐱 i ∘SL 𝐩 i) ∘SL 𝐱 i + (2 * (I * ) + I * ) 𝐱 i - (I * ) x, 𝐱 i - 2 (∑ i, 𝐱 i ∘SL 𝐱 i) ∘SL 𝐩 i = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) d:ε:ˣi:Fin d2 (∑ i, 𝐱 i ∘SL 𝐩 i) ∘SL 𝐱 i + (2 * (I * ) + I * ) 𝐱 i - (I * ) Finset.univ.card 𝐱 i - 2 (∑ i, 𝐱 i ∘SL 𝐱 i) ∘SL 𝐩 i = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) d:ε:ˣi:Fin d2 (∑ i, 𝐱 i ∘SL 𝐩 i) ∘SL 𝐱 i + (2 * (I * ) + I * ) 𝐱 i - (I * ) Fintype.card (Fin d) 𝐱 i - 2 (∑ i, 𝐱 i ∘SL 𝐱 i) ∘SL 𝐩 i = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) d:ε:ˣi:Fin d2 (∑ i, 𝐱 i ∘SL 𝐩 i) ∘SL 𝐱 i + (2 * (I * ) + I * ) 𝐱 i - (I * ) d 𝐱 i - 2 (∑ i, 𝐱 i ∘SL 𝐱 i) ∘SL 𝐩 i = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) d:ε:ˣi:Fin d2 (∑ i, 𝐱 i ∘SL 𝐩 i) ∘SL 𝐱 i + (2 * (I * ) + I * ) 𝐱 i - (I * ) d 𝐱 i - 2 (∑ i, 𝐱 i ∘SL 𝐱 i) ∘SL 𝐩 i = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) d:ε:ˣi:Fin d2 (∑ i, 𝐱 i ∘SL 𝐩 i) ∘SL 𝐱 i + (2 * (I * ) + I * ) 𝐱 i - (I * ) d 𝐱 i - 2 (𝐫₀ ε 2 - ε ^ 2 ContinuousLinearMap.id 𝓢(Space d, )) ∘SL 𝐩 i = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) d:ε:ˣi:Fin d2 (∑ i, 𝐱 i ∘SL 𝐩 i) ∘SL 𝐱 i + (2 * (I * ) + I * ) 𝐱 i - (I * ) d 𝐱 i - 2 (𝐫₀ ε 2 ∘SL 𝐩 i - (ε ^ 2 ContinuousLinearMap.id 𝓢(Space d, )) ∘SL 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) d:ε:ˣi:Fin d2 (∑ i, 𝐱 i ∘SL 𝐩 i) ∘SL 𝐱 i + (2 * (I * ) + I * ) 𝐱 i - (I * ) d 𝐱 i - 2 (𝐫₀ ε 2 ∘SL 𝐩 i - ε ^ 2 ContinuousLinearMap.id 𝓢(Space d, ) ∘SL 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) d:ε:ˣi:Fin d2 (∑ i, 𝐱 i ∘SL 𝐩 i) ∘SL 𝐱 i + (2 * (I * ) + I * ) 𝐱 i - (I * ) d 𝐱 i - 2 (𝐫₀ ε 2 ∘SL 𝐩 i - ε ^ 2 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) d:ε:ˣi:Fin d2 (∑ i, 𝐱 i ∘SL 𝐩 i) ∘SL 𝐱 i + (2 * (I * ) + I * ) 𝐱 i - (I * ) d 𝐱 i - (2 𝐫₀ ε 2 ∘SL 𝐩 i - 2 ε ^ 2 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i))] -- Clean up coefficients simp_rw d:ε:ˣi:Fin d2 (∑ i, 𝐱 i ∘SL 𝐩 i) ∘SL 𝐱 i + (2 * (I * ) + I * ) 𝐱 i - (I * ) d 𝐱 i - (2 𝐫₀ ε 2 ∘SL 𝐩 i - 2 ε ^ 2 𝐩 i) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i))d:ε:ˣi:Fin d2 (∑ i, 𝐱 i ∘SL 𝐩 i) ∘SL 𝐱 i + ((2 * (I * ) + I * ) 𝐱 i - (I * ) d 𝐱 i - (2 𝐫₀ ε 2 ∘SL 𝐩 i - 2 ε ^ 2 𝐩 i)) = 2 (∑ x, 𝐱 x ∘SL 𝐩 x) ∘SL 𝐱 i + ((-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) d:ε:ˣi:Fin d(2 * (I * ) + I * ) 𝐱 i - (I * ) d 𝐱 i - (2 𝐫₀ ε 2 ∘SL 𝐩 i - 2 ε ^ 2 𝐩 i) = (-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d(2 * (I * ) + I * ) 𝐱 i - (I * * d) 𝐱 i - (2 𝐫₀ ε 2 ∘SL 𝐩 i - 2 ε ^ 2 𝐩 i) = (-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d(2 * (I * ) + I * - I * * d) 𝐱 i - (2 𝐫₀ ε 2 ∘SL 𝐩 i - 2 ε ^ 2 𝐩 i) = (-I * * (d - 3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d(2 * (I * ) + I * + -(I * * d)) 𝐱 i + -(2 𝐫₀ ε 2 ∘SL 𝐩 i + -(2 ε ^ 2 𝐩 i)) = (-I * * (d + -3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d(2 * (I * ) + I * + -(I * * d)) 𝐱 i + (-(2 𝐫₀ ε 2 ∘SL 𝐩 i) + - -(2 ε ^ 2 𝐩 i)) = (-I * * (d + -3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d(2 * (I * ) + I * + -(I * * d)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + - -2 ε ^ 2 𝐩 i) = (-I * * (d + -3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d(2 * (I * ) + I * + -(I * * d)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + - -2 (ε ^ 2) 𝐩 i) = (-I * * (d + -3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d(2 * (I * ) + I * + -(I * * d)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (- -2 * (ε ^ 2)) 𝐩 i) = (-I * * (d + -3)) 𝐱 i + ((-2) 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d(2 * (I * ) + I * + -(I * * d)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (- -2 * (ε ^ 2)) 𝐩 i) = (-I * * (d + -3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d(2 * (I * ) + I * + -(I * * d)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (- -2 * (ε ^ 2)) 𝐩 i) = (-I * * (d + -3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * (ε ^ 2)) 𝐩 i) d:ε:ˣi:Fin d(2 * (I * ) + I * + -(I * * d)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (- -2 * ε ^ 2) 𝐩 i) = (-I * * (d + -3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d(2 * (I * ) + I * + -(I * * d)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (- -2 * ε ^ 2) 𝐩 i) = (-I * * (d + -3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) d:ε:ˣi:Fin d(2 * (I * ) + I * + -(I * * d)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i) = (-I * * (d + -3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)] All goals completed! 🐙d:ε:ˣi:Fin d(2 * I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ( ^ 2 * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐩 i = (I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐱) + (-2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i simp_rw d:ε:ˣi:Fin d(2 * I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ( ^ 2 * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐩 i = (I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐱) + (-2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 id:ε:ˣi:Fin d(2 * I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ( ^ 2 * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐩 i = (I * ) 𝐫₀ ε (-3) ∘SL (2 (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐱 i + (-2 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐩 i)) + (-2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i d:ε:ˣi:Fin d(2 * I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ( ^ 2 * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐩 i = (I * ) (𝐫₀ ε (-3) ∘SL (2 (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i) + 𝐫₀ ε (-3) ∘SL ((-I * * (d - 3)) 𝐱 i) + (𝐫₀ ε (-3) ∘SL (-2 𝐫₀ ε 2 ∘SL 𝐩 i) + 𝐫₀ ε (-3) ∘SL ((2 * ε ^ 2) 𝐩 i))) + (-2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i d:ε:ˣi:Fin d(2 * I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ( ^ 2 * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐩 i = (I * ) (2 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + (-I * * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + (-2 𝐫₀ ε (-3) ∘SL 𝐫₀ ε 2 ∘SL 𝐩 i + (2 * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i)) + (-2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i d:ε:ˣi:Fin d(2 * I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ( ^ 2 * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐩 i = (I * ) 2 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + (I * ) (-I * * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + ((I * ) -2 𝐫₀ ε (-3) ∘SL 𝐫₀ ε 2 ∘SL 𝐩 i + (I * ) (2 * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i) + (-2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i d:ε:ˣi:Fin d(2 * I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ( ^ 2 * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐩 i = (I * ) 2 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + (I * ) (-I * * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + ((I * ) (-2) 𝐫₀ ε (-3) ∘SL 𝐫₀ ε 2 ∘SL 𝐩 i + (I * ) (2 * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i) + (-2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i d:ε:ˣi:Fin d(2 * I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ( ^ 2 * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐩 i = (I * * 2) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + (I * * (-I * * (d - 3))) 𝐫₀ ε (-3) ∘SL 𝐱 i + ((I * * (-2)) 𝐫₀ ε (-3) ∘SL 𝐫₀ ε 2 ∘SL 𝐩 i + (I * * (2 * ε ^ 2)) 𝐫₀ ε (-3) ∘SL 𝐩 i) + (-2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i d:ε:ˣi:Fin d(2 * I * ) (𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩)) ∘SL 𝐱 i + ( ^ 2 * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐩 i = (I * * 2) (𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩)) ∘SL 𝐱 i + (I * * (-I * * (d - 3))) 𝐫₀ ε (-3) ∘SL 𝐱 i + ((I * * (-2)) (𝐫₀ ε (-3) ∘SL 𝐫₀ ε 2) ∘SL 𝐩 i + (I * * (2 * ε ^ 2)) 𝐫₀ ε (-3) ∘SL 𝐩 i) + (-2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i d:ε:ˣi:Fin d(2 * I * ) (𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩)) ∘SL 𝐱 i + ( ^ 2 * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐩 i = (I * * 2) (𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩)) ∘SL 𝐱 i + (I * * (-I * * (d - 3))) 𝐫₀ ε (-3) ∘SL 𝐱 i + ((I * * (-2)) 𝐫₀ ε (-3 + 2) ∘SL 𝐩 i + (I * * (2 * ε ^ 2)) 𝐫₀ ε (-3) ∘SL 𝐩 i) + (-2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i d:ε:ˣi:Fin d(2 * I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ( ^ 2 * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐩 i = (I * * 2) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + (I * * (-I * * (d - 3))) 𝐫₀ ε (-3) ∘SL 𝐱 i + ((I * * (-2)) 𝐫₀ ε (-3 + 2) ∘SL 𝐩 i + (I * * (2 * ε ^ 2)) 𝐫₀ ε (-3) ∘SL 𝐩 i) + (-2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i d:ε:ˣi:Fin d(2 * I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + (( ^ 2 * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐩 i) = (I * * 2) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ((I * * (-I * * (d - 3))) 𝐫₀ ε (-3) ∘SL 𝐱 i + ((I * * (-2)) 𝐫₀ ε (-3 + 2) ∘SL 𝐩 i + ((I * * (2 * ε ^ 2)) 𝐫₀ ε (-3) ∘SL 𝐩 i + (-2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i))) d:ε:ˣi:Fin d(2 * I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + (( ^ 2 * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐩 i) = (I * * 2) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ((I * * (-I * * (d - 3))) 𝐫₀ ε (-3) ∘SL 𝐱 i + ((I * * (-2)) 𝐫₀ ε (-3 + 2) ∘SL 𝐩 i + (I * * (2 * ε ^ 2) + -2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i)) d:ε:ˣi:Fin d(2 * I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ((( ^ 2) * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐩 i) = (I * * 2) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ((I * * (-I * * (d - 3))) 𝐫₀ ε (-3) ∘SL 𝐱 i + ((I * * (-2)) 𝐫₀ ε (-3 + 2) ∘SL 𝐩 i + (I * * (2 * (ε ^ 2)) + -2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i)) d:ε:ˣi:Fin d(2 * I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ((( ^ 2) * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐩 i) = (I * * 2) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ((I * * (-I * * (d - 3))) 𝐫₀ ε (-3) ∘SL 𝐱 i + ((I * * (-2)) 𝐫₀ ε (-3 + 2) ∘SL 𝐩 i + (I * * (2 * (ε ^ 2)) + -2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i)) d:ε:ˣi:Fin d(2 * I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ((( ^ 2) * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐩 i) = (I * * 2) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ((I * * (-I * * (d - 3))) 𝐫₀ ε (-3) ∘SL 𝐱 i + ((I * * -2) 𝐫₀ ε (-3 + 2) ∘SL 𝐩 i + (I * * (2 * (ε ^ 2)) + -2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i)) d:ε:ˣi:Fin d(2 * I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + (( ^ 2 * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐩 i) = (I * * 2) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ((I * * (-I * * (d - 3))) 𝐫₀ ε (-3) ∘SL 𝐱 i + ((I * * -2) 𝐫₀ ε (-3 + 2) ∘SL 𝐩 i + (I * * (2 * ε ^ 2) + -2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i)) d:ε:ˣi:Fin d(2 * I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + (( ^ 2 * (d - 3)) 𝐫₀ ε (-3) ∘SL 𝐱 i + (-2 * I * ) 𝐫₀ ε (-1) ∘SL 𝐩 i) = (I * * 2) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ((I * * (-I * * (d - 3))) 𝐫₀ ε (-3) ∘SL 𝐱 i + ((I * * -2) 𝐫₀ ε (-3 + 2) ∘SL 𝐩 i + (I * * (2 * ε ^ 2) + -2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i))] d:ε:ˣi:Fin d(I * * 2) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ((-( ^ 2 * 3) + ^ 2 * d) 𝐫₀ ε (-3) ∘SL 𝐱 i + -(I * * 2) 𝐫₀ ε (-1) ∘SL 𝐩 i) = (I * * 2) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐩) ∘SL 𝐱 i + ((I ^ 2 * ^ 2 * 3 - I ^ 2 * ^ 2 * d) 𝐫₀ ε (-3) ∘SL 𝐱 i + (-(I * * 2) 𝐫₀ ε (-1) ∘SL 𝐩 i + 0 𝐫₀ ε (-3) ∘SL 𝐩 i)) All goals completed! 🐙private lemma r_comm_pL_Lp {d : } (ε : ˣ) (i : Fin d) : 𝐫₀[d] ε (-1), 𝐩 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐩 = -((I * ) 𝐫₀ ε (-3) ∘L (𝐱 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐱)) := d:ε:ˣi:Fin d𝐫₀ ε (-1), 𝐩 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐩 = -((I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐱)) calc _ = j, (𝐫₀[d] ε (-1), 𝐩 j ∘L 𝐋 i j + 𝐋 i j ∘L 𝐫₀[d] ε (-1), 𝐩 j) := d:ε:ˣi:Fin d𝐫₀ ε (-1), 𝐩 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐩 = j, (𝐫₀ ε (-1), 𝐩 j ∘SL 𝐋 i j + 𝐋 i j ∘SL 𝐫₀ ε (-1), 𝐩 j) All goals completed! 🐙 _ = -((I * ) j, (𝐫₀ ε (-3) ∘L 𝐱 j ∘L 𝐋 i j + (𝐋 i j ∘L 𝐫₀ ε (-3)) ∘L 𝐱 j)) := d:ε:ˣi:Fin d j, (𝐫₀ ε (-1), 𝐩 j ∘SL 𝐋 i j + 𝐋 i j ∘SL 𝐫₀ ε (-1), 𝐩 j) = -((I * ) j, (𝐫₀ ε (-3) ∘SL 𝐱 j ∘SL 𝐋 i j + (𝐋 i j ∘SL 𝐫₀ ε (-3)) ∘SL 𝐱 j)) d:ε:ˣi:Fin d(-1 * I * ) x, (𝐫₀ ε (-1 - 2) ∘SL 𝐱 x ∘SL 𝐋 i x + 𝐋 i x ∘SL 𝐫₀ ε (-1 - 2) ∘SL 𝐱 x) = -(I * ) x, (𝐫₀ ε (-3) ∘SL 𝐱 x ∘SL 𝐋 i x + 𝐋 i x ∘SL 𝐫₀ ε (-3) ∘SL 𝐱 x) All goals completed! 🐙 _ = -((I * ) 𝐫₀ ε (-3) ∘L (𝐱 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐱)) := d:ε:ˣi:Fin d-((I * ) j, (𝐫₀ ε (-3) ∘SL 𝐱 j ∘SL 𝐋 i j + (𝐋 i j ∘SL 𝐫₀ ε (-3)) ∘SL 𝐱 j)) = -((I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐱)) simp_rw d:ε:ˣi:Fin d-((I * ) j, (𝐫₀ ε (-3) ∘SL 𝐱 j ∘SL 𝐋 i j + (𝐋 i j ∘SL 𝐫₀ ε (-3)) ∘SL 𝐱 j)) = -((I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐱))d:ε:ˣi:Fin d-((I * ) x, (𝐫₀ ε (-3) ∘SL 𝐱 x ∘SL 𝐋 i x + (𝐫₀ ε (-3) ∘SL 𝐋 i x) ∘SL 𝐱 x)) = -((I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐱)) d:ε:ˣi:Fin d-((I * ) x, (𝐫₀ ε (-3) ∘SL 𝐱 x ∘SL 𝐋 i x + 𝐫₀ ε (-3) ∘SL 𝐋 i x ∘SL 𝐱 x)) = -((I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐱)) d:ε:ˣi:Fin d-((I * ) x, 𝐫₀ ε (-3) ∘SL (𝐱 x ∘SL 𝐋 i x + 𝐋 i x ∘SL 𝐱 x)) = -((I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐱)) d:ε:ˣi:Fin d-((I * ) 𝐫₀ ε (-3) ∘SL i_1, (𝐱 i_1 ∘SL 𝐋 i i_1 + 𝐋 i i_1 ∘SL 𝐱 i_1)) = -((I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐱)) d:ε:ˣi:Fin d-((I * ) 𝐫₀ ε (-3) ∘SL ( x, 𝐱 x ∘SL 𝐋 i x + x, 𝐋 i x ∘SL 𝐱 x)) = -((I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐱)) d:ε:ˣi:Fin d-((I * ) 𝐫₀ ε (-3) ∘SL ( x, 𝐱 x ∘SL 𝐋 i x + x, 𝐋 i x ∘SL 𝐱 x)) = -((I * ) 𝐫₀ ε (-3) ∘SL ( i_1, 𝐱 i_1 * 𝐋 i i_1 + i_1, 𝐋 i i_1 * 𝐱 i_1)) All goals completed! 🐙]

⁅𝐇(ε), 𝐀(ε)ᵢ⁆ = iℏk·ε²𝐫(ε)⁻³𝐩ᵢ - 3ℏ²k/2·ε²𝐫(ε)⁻⁵𝐱ᵢ

H:HydrogenAtomε:ˣi:Fin H.dh:H.m * H.k * (H.m⁻¹ * 2⁻¹) = 2⁻¹ * H.kH.hamiltonianRegCLM ε, H.lrlOperator ε i = (-2⁻¹ * H.k) (𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1) ∘SL 𝐱 i + 𝐫₀ ε (-1), 𝐩 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐩) H:HydrogenAtomε:ˣi:Fin H.dh:H.m * H.k * (H.m⁻¹ * 2⁻¹) = 2⁻¹ * H.k2⁻¹ ((2 * H.m)⁻¹ 0 - H.k 𝐫₀ ε (-1), 𝐩 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐩) - (H.m * H.k) ((2 * H.m)⁻¹ 𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1) ∘SL 𝐱 i - H.k 𝐫₀ ε (-1), 𝐫₀ ε (-1) ∘SL 𝐱 i) = (-2⁻¹ * H.k) (𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1) ∘SL 𝐱 i + 𝐫₀ ε (-1), 𝐩 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐩) All goals completed! 🐙 simp_rw H:HydrogenAtomε:ˣi:Fin H.d(-2⁻¹ * H.k) (𝐩 ⬝ᵥ 𝐩, 𝐫₀ ε (-1) ∘SL 𝐱 i + 𝐫₀ ε (-1), 𝐩 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐩) = (I * * H.k * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i - (3 / 2 * ^ 2 * H.k * ε ^ 2) 𝐫₀ ε (-5) ∘SL 𝐱 iH:HydrogenAtomε:ˣi:Fin H.d(-2⁻¹ * H.k) ((I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐱) + ((-2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i + (3 * ^ 2 * ε ^ 2) 𝐫₀ ε (-5) ∘SL 𝐱 i) + 𝐫₀ ε (-1), 𝐩 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐩) = (I * * H.k * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i - (3 / 2 * ^ 2 * H.k * ε ^ 2) 𝐫₀ ε (-5) ∘SL 𝐱 i H:HydrogenAtomε:ˣi:Fin H.d(-2⁻¹ * H.k) ((I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐱) + ((-2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i + (3 * ^ 2 * ε ^ 2) 𝐫₀ ε (-5) ∘SL 𝐱 i) + -((I * ) 𝐫₀ ε (-3) ∘SL (𝐱 ⬝ᵥ 𝐋 i + 𝐋 i ⬝ᵥ 𝐱))) = (I * * H.k * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i - (3 / 2 * ^ 2 * H.k * ε ^ 2) 𝐫₀ ε (-5) ∘SL 𝐱 i H:HydrogenAtomε:ˣi:Fin H.d(-2⁻¹ * H.k) ((-2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i + (3 * ^ 2 * ε ^ 2) 𝐫₀ ε (-5) ∘SL 𝐱 i) = (I * * H.k * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i - (3 / 2 * ^ 2 * H.k * ε ^ 2) 𝐫₀ ε (-5) ∘SL 𝐱 i H:HydrogenAtomε:ˣi:Fin H.d(-2⁻¹ * H.k) (-2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i + (-2⁻¹ * H.k) (3 * ^ 2 * ε ^ 2) 𝐫₀ ε (-5) ∘SL 𝐱 i = (I * * H.k * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i - (3 / 2 * ^ 2 * H.k * ε ^ 2) 𝐫₀ ε (-5) ∘SL 𝐱 i H:HydrogenAtomε:ˣi:Fin H.d(-2⁻¹ * H.k) (-2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i + (-2⁻¹ * H.k) (3 * ^ 2 * ε ^ 2) 𝐫₀ ε (-5) ∘SL 𝐱 i = (I * * H.k * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i + -((3 / 2 * ^ 2 * H.k * ε ^ 2) 𝐫₀ ε (-5) ∘SL 𝐱 i) H:HydrogenAtomε:ˣi:Fin H.d(-2⁻¹ * H.k) (-2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i + (-2⁻¹ * H.k) (3 * ^ 2 * ε ^ 2) 𝐫₀ ε (-5) ∘SL 𝐱 i = (I * * H.k * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i + -(3 / 2 * ^ 2 * H.k * ε ^ 2) 𝐫₀ ε (-5) ∘SL 𝐱 i H:HydrogenAtomε:ˣi:Fin H.d(-2⁻¹ * H.k) (-2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i + (-2⁻¹ * H.k) (3 * ^ 2 * ε ^ 2) 𝐫₀ ε (-5) ∘SL 𝐱 i = (I * * H.k * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i + (-(3 / 2) * ^ 2 * H.k * ε ^ 2) 𝐫₀ ε (-5) ∘SL 𝐱 i H:HydrogenAtomε:ˣi:Fin H.d(-2⁻¹ * H.k) (-2 * I * * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i + (-2⁻¹ * H.k) (3 * ^ 2 * ε ^ 2) 𝐫₀ ε (-5) ∘SL 𝐱 i = (I * * H.k * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i + (-(3 / 2) * ^ 2 * H.k * ε ^ 2) 𝐫₀ ε (-5) ∘SL 𝐱 i H:HydrogenAtomε:ˣi:Fin H.d((-2⁻¹ * H.k) * (-2 * I * * ε ^ 2)) 𝐫₀ ε (-3) ∘SL 𝐩 i + ((-2⁻¹ * H.k) * (3 * ^ 2 * ε ^ 2)) 𝐫₀ ε (-5) ∘SL 𝐱 i = (I * * H.k * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i + (-(3 / 2) * ^ 2 * H.k * ε ^ 2) 𝐫₀ ε (-5) ∘SL 𝐱 i H:HydrogenAtomε:ˣi:Fin H.d((-2⁻¹) * H.k * (-2 * I * * ε ^ 2)) 𝐫₀ ε (-3) ∘SL 𝐩 i + ((-2⁻¹) * H.k * (3 * ( ^ 2) * (ε ^ 2))) 𝐫₀ ε (-5) ∘SL 𝐱 i = (I * * H.k * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i + ((-(3 / 2)) * ( ^ 2) * H.k * (ε ^ 2)) 𝐫₀ ε (-5) ∘SL 𝐱 i H:HydrogenAtomε:ˣi:Fin H.d(-2⁻¹ * H.k * (-2 * I * * ε ^ 2)) 𝐫₀ ε (-3) ∘SL 𝐩 i + (-2⁻¹ * H.k * (3 * ( ^ 2) * (ε ^ 2))) 𝐫₀ ε (-5) ∘SL 𝐱 i = (I * * H.k * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i + (-(3 / 2) * ( ^ 2) * H.k * (ε ^ 2)) 𝐫₀ ε (-5) ∘SL 𝐱 i H:HydrogenAtomε:ˣi:Fin H.d(-(↑2)⁻¹ * H.k * (-2 * I * * ε ^ 2)) 𝐫₀ ε (-3) ∘SL 𝐩 i + (-(↑2)⁻¹ * H.k * (3 * ( ^ 2) * (ε ^ 2))) 𝐫₀ ε (-5) ∘SL 𝐱 i = (I * * H.k * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i + (-(3 / 2) * ( ^ 2) * H.k * (ε ^ 2)) 𝐫₀ ε (-5) ∘SL 𝐱 i H:HydrogenAtomε:ˣi:Fin H.d(-(↑2)⁻¹ * H.k * (-2 * I * * ε ^ 2)) 𝐫₀ ε (-3) ∘SL 𝐩 i + (-(↑2)⁻¹ * H.k * (3 * ( ^ 2) * (ε ^ 2))) 𝐫₀ ε (-5) ∘SL 𝐱 i = (I * * H.k * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i + (-(3 / 2) * ( ^ 2) * H.k * (ε ^ 2)) 𝐫₀ ε (-5) ∘SL 𝐱 i H:HydrogenAtomε:ˣi:Fin H.d(-(↑2)⁻¹ * H.k * (-2 * I * * ε ^ 2)) 𝐫₀ ε (-3) ∘SL 𝐩 i + (-(↑2)⁻¹ * H.k * (3 * ^ 2 * ε ^ 2)) 𝐫₀ ε (-5) ∘SL 𝐱 i = (I * * H.k * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i + (-(3 / 2) * ^ 2 * H.k * ε ^ 2) 𝐫₀ ε (-5) ∘SL 𝐱 i H:HydrogenAtomε:ˣi:Fin H.d(-2⁻¹ * H.k * (-2 * I * * ε ^ 2)) 𝐫₀ ε (-3) ∘SL 𝐩 i + (-2⁻¹ * H.k * (3 * ^ 2 * ε ^ 2)) 𝐫₀ ε (-5) ∘SL 𝐱 i = (I * * H.k * ε ^ 2) 𝐫₀ ε (-3) ∘SL 𝐩 i + (-(3 / 2) * ^ 2 * H.k * ε ^ 2) 𝐫₀ ε (-5) ∘SL 𝐱 i] All goals completed! 🐙
All goals completed! 🐙All goals completed! 🐙d:2⁻¹ i, j, (𝐋 i j ∘SL 𝐩 j ∘SL 𝐩 i + 𝐋 j i ∘SL 𝐩 i ∘SL 𝐩 j) = 0 conv_lhs => d:i:Fin dj:Fin d| 𝐋 i j ∘SL 𝐩 j ∘SL 𝐩 i + 𝐋 j i ∘SL 𝐩 i ∘SL 𝐩 j d:i:Fin dj:Fin d| 𝐋 i j ∘SL 𝐩 i ∘SL 𝐩 j + (-𝐋 i j) ∘SL 𝐩 i ∘SL 𝐩 j All goals completed! 🐙d:2⁻¹ i, j, (𝐩 i ∘SL 𝐩 j ∘SL 𝐋 i j + 𝐩 j ∘SL 𝐩 i ∘SL 𝐋 j i) = 0 conv_lhs => d:i:Fin dj:Fin d| 𝐩 i ∘SL 𝐩 j ∘SL 𝐋 i j + 𝐩 j ∘SL 𝐩 i ∘SL 𝐋 j i d:i:Fin dj:Fin d| (𝐩 i ∘SL 𝐩 j) ∘SL 𝐋 i j + (𝐩 i ∘SL 𝐩 j) ∘SL (-𝐋 i j) All goals completed! 🐙d:2⁻¹ i, k, j, (𝐋 i j ∘SL 𝐩 j ∘SL 𝐩 k ∘SL 𝐋 i k + 𝐋 k j ∘SL 𝐩 j ∘SL 𝐩 i ∘SL 𝐋 k i) = (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋² conv_lhs => d:i:Fin dj:Fin dk:Fin d| 𝐋 i k ∘SL 𝐩 k ∘SL 𝐩 j ∘SL 𝐋 i j + 𝐋 j k ∘SL 𝐩 k ∘SL 𝐩 i ∘SL 𝐋 j i calc _ = (𝐋 i k ∘L 𝐩 k ∘L 𝐩 j - 𝐋 j k ∘L 𝐩 k ∘L 𝐩 i) ∘L 𝐋 i j := d:i:Fin dj:Fin dk:Fin d𝐋 i k ∘SL 𝐩 k ∘SL 𝐩 j ∘SL 𝐋 i j + 𝐋 j k ∘SL 𝐩 k ∘SL 𝐩 i ∘SL 𝐋 j i = (𝐋 i k ∘SL 𝐩 k ∘SL 𝐩 j - 𝐋 j k ∘SL 𝐩 k ∘SL 𝐩 i) ∘SL 𝐋 i j All goals completed! 🐙 _ = (𝐱 i ∘L 𝐩 k ∘L 𝐩 k ∘L 𝐩 j - 𝐱 k ∘L 𝐩 i ∘L 𝐩 k ∘L 𝐩 j - (𝐱 j ∘L 𝐩 k ∘L 𝐩 k ∘L 𝐩 i - 𝐱 k ∘L 𝐩 j ∘L 𝐩 k ∘L 𝐩 i)) ∘L 𝐋 i j := d:i:Fin dj:Fin dk:Fin d(𝐋 i k ∘SL 𝐩 k ∘SL 𝐩 j - 𝐋 j k ∘SL 𝐩 k ∘SL 𝐩 i) ∘SL 𝐋 i j = (𝐱 i ∘SL 𝐩 k ∘SL 𝐩 k ∘SL 𝐩 j - 𝐱 k ∘SL 𝐩 i ∘SL 𝐩 k ∘SL 𝐩 j - (𝐱 j ∘SL 𝐩 k ∘SL 𝐩 k ∘SL 𝐩 i - 𝐱 k ∘SL 𝐩 j ∘SL 𝐩 k ∘SL 𝐩 i)) ∘SL 𝐋 i j simp_rw d:i:Fin dj:Fin dk:Fin d(𝐋 i k ∘SL 𝐩 k ∘SL 𝐩 j - 𝐋 j k ∘SL 𝐩 k ∘SL 𝐩 i) ∘SL 𝐋 i j = (𝐱 i ∘SL 𝐩 k ∘SL 𝐩 k ∘SL 𝐩 j - 𝐱 k ∘SL 𝐩 i ∘SL 𝐩 k ∘SL 𝐩 j - (𝐱 j ∘SL 𝐩 k ∘SL 𝐩 k ∘SL 𝐩 i - 𝐱 k ∘SL 𝐩 j ∘SL 𝐩 k ∘SL 𝐩 i)) ∘SL 𝐋 i jd:i:Fin dj:Fin dk:Fin d((𝐱 i ∘SL 𝐩 k - 𝐱 k ∘SL 𝐩 i) ∘SL 𝐩 k ∘SL 𝐩 j - (𝐱 j ∘SL 𝐩 k - 𝐱 k ∘SL 𝐩 j) ∘SL 𝐩 k ∘SL 𝐩 i) ∘SL (𝐱 i ∘SL 𝐩 j - 𝐱 j ∘SL 𝐩 i) = (𝐱 i ∘SL 𝐩 k ∘SL 𝐩 k ∘SL 𝐩 j - 𝐱 k ∘SL 𝐩 i ∘SL 𝐩 k ∘SL 𝐩 j - (𝐱 j ∘SL 𝐩 k ∘SL 𝐩 k ∘SL 𝐩 i - 𝐱 k ∘SL 𝐩 j ∘SL 𝐩 k ∘SL 𝐩 i)) ∘SL (𝐱 i ∘SL 𝐩 j - 𝐱 j ∘SL 𝐩 i) d:i:Fin dj:Fin dk:Fin d((𝐱 i ∘SL 𝐩 k) ∘SL 𝐩 k ∘SL 𝐩 j) ∘SL (𝐱 i ∘SL 𝐩 j - 𝐱 j ∘SL 𝐩 i) - ((𝐱 k ∘SL 𝐩 i) ∘SL 𝐩 k ∘SL 𝐩 j) ∘SL (𝐱 i ∘SL 𝐩 j - 𝐱 j ∘SL 𝐩 i) - (((𝐱 j ∘SL 𝐩 k) ∘SL 𝐩 k ∘SL 𝐩 i) ∘SL (𝐱 i ∘SL 𝐩 j - 𝐱 j ∘SL 𝐩 i) - ((𝐱 k ∘SL 𝐩 j) ∘SL 𝐩 k ∘SL 𝐩 i) ∘SL (𝐱 i ∘SL 𝐩 j - 𝐱 j ∘SL 𝐩 i)) = (𝐱 i ∘SL 𝐩 k ∘SL 𝐩 k ∘SL 𝐩 j) ∘SL (𝐱 i ∘SL 𝐩 j - 𝐱 j ∘SL 𝐩 i) - (𝐱 k ∘SL 𝐩 i ∘SL 𝐩 k ∘SL 𝐩 j) ∘SL (𝐱 i ∘SL 𝐩 j - 𝐱 j ∘SL 𝐩 i) - ((𝐱 j ∘SL 𝐩 k ∘SL 𝐩 k ∘SL 𝐩 i) ∘SL (𝐱 i ∘SL 𝐩 j - 𝐱 j ∘SL 𝐩 i) - (𝐱 k ∘SL 𝐩 j ∘SL 𝐩 k ∘SL 𝐩 i) ∘SL (𝐱 i ∘SL 𝐩 j - 𝐱 j ∘SL 𝐩 i)) All goals completed! 🐙] _ = (𝐱 i ∘L 𝐩 j ∘L 𝐩 k ∘L 𝐩 k - 𝐱 j ∘L 𝐩 i ∘L 𝐩 k ∘L 𝐩 k) ∘L 𝐋 i j := d:i:Fin dj:Fin dk:Fin d(𝐱 i ∘SL 𝐩 k ∘SL 𝐩 k ∘SL 𝐩 j - 𝐱 k ∘SL 𝐩 i ∘SL 𝐩 k ∘SL 𝐩 j - (𝐱 j ∘SL 𝐩 k ∘SL 𝐩 k ∘SL 𝐩 i - 𝐱 k ∘SL 𝐩 j ∘SL 𝐩 k ∘SL 𝐩 i)) ∘SL 𝐋 i j = (𝐱 i ∘SL 𝐩 j ∘SL 𝐩 k ∘SL 𝐩 k - 𝐱 j ∘SL 𝐩 i ∘SL 𝐩 k ∘SL 𝐩 k) ∘SL 𝐋 i j simp_rw d:i:Fin dj:Fin dk:Fin d(𝐱 i ∘SL 𝐩 k ∘SL 𝐩 k ∘SL 𝐩 j - 𝐱 k ∘SL 𝐩 i ∘SL 𝐩 k ∘SL 𝐩 j - (𝐱 j ∘SL 𝐩 k ∘SL 𝐩 k ∘SL 𝐩 i - 𝐱 k ∘SL 𝐩 j ∘SL 𝐩 k ∘SL 𝐩 i)) ∘SL 𝐋 i j = (𝐱 i ∘SL 𝐩 j ∘SL 𝐩 k ∘SL 𝐩 k - 𝐱 j ∘SL 𝐩 i ∘SL 𝐩 k ∘SL 𝐩 k) ∘SL 𝐋 i jd:i:Fin dj:Fin dk:Fin d(𝐱 i ∘SL 𝐩 k ∘SL 𝐩 j ∘SL 𝐩 k - 𝐱 k ∘SL 𝐩 i ∘SL 𝐩 j ∘SL 𝐩 k - (𝐱 j ∘SL 𝐩 k ∘SL 𝐩 i ∘SL 𝐩 k - 𝐱 k ∘SL 𝐩 j ∘SL 𝐩 i ∘SL 𝐩 k)) ∘SL 𝐋 i j = (𝐱 i ∘SL 𝐩 j ∘SL 𝐩 k ∘SL 𝐩 k - 𝐱 j ∘SL 𝐩 i ∘SL 𝐩 k ∘SL 𝐩 k) ∘SL 𝐋 i j d:i:Fin dj:Fin dk:Fin d(𝐱 i ∘SL (𝐩 k ∘SL 𝐩 j) ∘SL 𝐩 k - 𝐱 k ∘SL (𝐩 i ∘SL 𝐩 j) ∘SL 𝐩 k - (𝐱 j ∘SL (𝐩 k ∘SL 𝐩 i) ∘SL 𝐩 k - 𝐱 k ∘SL (𝐩 j ∘SL 𝐩 i) ∘SL 𝐩 k)) ∘SL 𝐋 i j = (𝐱 i ∘SL (𝐩 j ∘SL 𝐩 k) ∘SL 𝐩 k - 𝐱 j ∘SL (𝐩 i ∘SL 𝐩 k) ∘SL 𝐩 k) ∘SL 𝐋 i j d:i:Fin dj:Fin dk:Fin d(𝐱 i ∘SL (𝐩 j ∘SL 𝐩 k) ∘SL 𝐩 k - 𝐱 k ∘SL (𝐩 i ∘SL 𝐩 j) ∘SL 𝐩 k - (𝐱 j ∘SL (𝐩 i ∘SL 𝐩 k) ∘SL 𝐩 k - 𝐱 k ∘SL (𝐩 j ∘SL 𝐩 i) ∘SL 𝐩 k)) ∘SL 𝐋 i j = (𝐱 i ∘SL (𝐩 j ∘SL 𝐩 k) ∘SL 𝐩 k - 𝐱 j ∘SL (𝐩 i ∘SL 𝐩 k) ∘SL 𝐩 k) ∘SL 𝐋 i j d:i:Fin dj:Fin dk:Fin d(𝐱 i ∘SL (𝐩 j ∘SL 𝐩 k) ∘SL 𝐩 k - 𝐱 k ∘SL (𝐩 j ∘SL 𝐩 i) ∘SL 𝐩 k - (𝐱 j ∘SL (𝐩 i ∘SL 𝐩 k) ∘SL 𝐩 k - 𝐱 k ∘SL (𝐩 j ∘SL 𝐩 i) ∘SL 𝐩 k)) ∘SL 𝐋 i j = (𝐱 i ∘SL (𝐩 j ∘SL 𝐩 k) ∘SL 𝐩 k - 𝐱 j ∘SL (𝐩 i ∘SL 𝐩 k) ∘SL 𝐩 k) ∘SL 𝐋 i j All goals completed! 🐙] _ = 𝐋 i j ∘L (𝐩 k ∘L 𝐩 k) ∘L 𝐋 i j := d:i:Fin dj:Fin dk:Fin d(𝐱 i ∘SL 𝐩 j ∘SL 𝐩 k ∘SL 𝐩 k - 𝐱 j ∘SL 𝐩 i ∘SL 𝐩 k ∘SL 𝐩 k) ∘SL 𝐋 i j = 𝐋 i j ∘SL (𝐩 k ∘SL 𝐩 k) ∘SL 𝐋 i j simp_rw d:i:Fin dj:Fin dk:Fin d(𝐱 i ∘SL 𝐩 j ∘SL 𝐩 k ∘SL 𝐩 k - 𝐱 j ∘SL 𝐩 i ∘SL 𝐩 k ∘SL 𝐩 k) ∘SL 𝐋 i j = 𝐋 i j ∘SL (𝐩 k ∘SL 𝐩 k) ∘SL 𝐋 i jd:i:Fin dj:Fin dk:Fin d(((𝐱 i ∘SL 𝐩 j) ∘SL 𝐩 k) ∘SL 𝐩 k - ((𝐱 j ∘SL 𝐩 i) ∘SL 𝐩 k) ∘SL 𝐩 k) ∘SL 𝐋 i j = ((𝐋 i j ∘SL 𝐩 k) ∘SL 𝐩 k) ∘SL 𝐋 i j d:i:Fin dj:Fin dk:Fin d(((𝐱 i ∘SL 𝐩 j - 𝐱 j ∘SL 𝐩 i) ∘SL 𝐩 k) ∘SL 𝐩 k) ∘SL 𝐋 i j = ((𝐋 i j ∘SL 𝐩 k) ∘SL 𝐩 k) ∘SL 𝐋 i j All goals completed! 🐙] d:2⁻¹ i, j, k, 𝐋 i j ∘SL (𝐩 k ∘SL 𝐩 k) ∘SL 𝐋 i j = 2⁻¹ i, j, 𝐋 i j ∘SL (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i jd:2⁻¹ i, j, 𝐋 i j ∘SL (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j = (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋² d:2⁻¹ i, j, k, 𝐋 i j ∘SL (𝐩 k ∘SL 𝐩 k) ∘SL 𝐋 i j = 2⁻¹ i, j, 𝐋 i j ∘SL (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j simp_rw d:2⁻¹ i, j, k, 𝐋 i j ∘SL (𝐩 k ∘SL 𝐩 k) ∘SL 𝐋 i j = 2⁻¹ i, j, 𝐋 i j ∘SL (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i jd:2⁻¹ x, x_1, 𝐋 x x_1 ∘SL i, (𝐩 i ∘SL 𝐩 i) ∘SL 𝐋 x x_1 = 2⁻¹ i, j, 𝐋 i j ∘SL (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j d:2⁻¹ x, x_1, 𝐋 x x_1 ∘SL (∑ i, 𝐩 i ∘SL 𝐩 i) ∘SL 𝐋 x x_1 = 2⁻¹ i, j, 𝐋 i j ∘SL (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j d:2⁻¹ x, x_1, (𝐋 x x_1 ∘SL i, 𝐩 i ∘SL 𝐩 i) ∘SL 𝐋 x x_1 = 2⁻¹ x, x_1, (𝐋 x x_1 ∘SL (𝐩 ⬝ᵥ 𝐩)) ∘SL 𝐋 x x_1 d:2⁻¹ x, x_1, (𝐋 x x_1 ∘SL i, 𝐩 i ∘SL 𝐩 i) ∘SL 𝐋 x x_1 = 2⁻¹ x, x_1, (𝐋 x x_1 ∘SL i, 𝐩 i * 𝐩 i) ∘SL 𝐋 x x_1 All goals completed! 🐙] simp_rw d:2⁻¹ i, j, 𝐋 i j ∘SL (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 i j = (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋²d:2⁻¹ x, x_1, (𝐋 x x_1 ∘SL (𝐩 ⬝ᵥ 𝐩)) ∘SL 𝐋 x x_1 = (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋² d:2⁻¹ x, x_1, ((𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 x x_1) ∘SL 𝐋 x x_1 = (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋² d:2⁻¹ x, x_1, (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋 x x_1 ∘SL 𝐋 x x_1 = (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋² d:2⁻¹ (𝐩 ⬝ᵥ 𝐩) ∘SL i, i_1, 𝐋 i i_1 ∘SL 𝐋 i i_1 = (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋² d:(𝐩 ⬝ᵥ 𝐩) ∘SL (2⁻¹ i, i_1, 𝐋 i i_1 ∘SL 𝐋 i i_1) = (𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋² All goals completed! 🐙]All goals completed! 🐙All goals completed! 🐙private lemma sum_prx (d : ) (ε : ˣ) : i, 𝐩 i ∘L 𝐫₀[d] ε (-1) ∘L 𝐱 i = 𝐫₀ ε (-1) ∘L (𝐱 ⬝ᵥ 𝐩) - (I * * (d - 1)) 𝐫₀ ε (-1) - (I * * ε.1 ^ 2) 𝐫₀ ε (-3) := d:ε:ˣ i, 𝐩 i ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 i = 𝐫₀ ε (-1) ∘SL (𝐱 ⬝ᵥ 𝐩) - (I * * (d - 1)) 𝐫₀ ε (-1) - (I * * ε ^ 2) 𝐫₀ ε (-3) calc _ = i, (𝐫₀ ε (-1) ∘L 𝐩 i ∘L 𝐱 i + (I * ) 𝐫₀ ε (-3) ∘L 𝐱 i ∘L 𝐱 i) := d:ε:ˣ i, 𝐩 i ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 i = i, (𝐫₀ ε (-1) ∘SL 𝐩 i ∘SL 𝐱 i + (I * ) 𝐫₀ ε (-3) ∘SL 𝐱 i ∘SL 𝐱 i) simp_rw d:ε:ˣ i, 𝐩 i ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 i = i, (𝐫₀ ε (-1) ∘SL 𝐩 i ∘SL 𝐱 i + (I * ) 𝐫₀ ε (-3) ∘SL 𝐱 i ∘SL 𝐱 i)d:ε:ˣ x, (𝐩 x ∘SL 𝐫₀ ε (-1)) ∘SL 𝐱 x = x, ((𝐫₀ ε (-1) ∘SL 𝐩 x) ∘SL 𝐱 x + (I * ) (𝐫₀ ε (-3) ∘SL 𝐱 x) ∘SL 𝐱 x) d:ε:ˣ x, (𝐫₀ ε (-1) ∘SL 𝐩 x - ((-1) * I * ) 𝐫₀ ε (-1 - 2) ∘SL 𝐱 x) ∘SL 𝐱 x = x, ((𝐫₀ ε (-1) ∘SL 𝐩 x) ∘SL 𝐱 x + (I * ) (𝐫₀ ε (-3) ∘SL 𝐱 x) ∘SL 𝐱 x)] d:ε:ˣ x, (𝐫₀ ε (-1) ∘SL 𝐩 x - ((-1) * I * ) 𝐫₀ ε (-3) ∘SL 𝐱 x) ∘SL 𝐱 x = x, ((𝐫₀ ε (-1) ∘SL 𝐩 x) ∘SL 𝐱 x + (I * ) (𝐫₀ ε (-3) ∘SL 𝐱 x) ∘SL 𝐱 x) All goals completed! 🐙 _ = i, (𝐫₀ ε (-1) ∘L 𝐱 i ∘L 𝐩 i - (I * ) 𝐫₀ ε (-1) + (I * ) 𝐫₀ ε (-3) ∘L 𝐱 i ∘L 𝐱 i) := d:ε:ˣ i, (𝐫₀ ε (-1) ∘SL 𝐩 i ∘SL 𝐱 i + (I * ) 𝐫₀ ε (-3) ∘SL 𝐱 i ∘SL 𝐱 i) = i, (𝐫₀ ε (-1) ∘SL 𝐱 i ∘SL 𝐩 i - (I * ) 𝐫₀ ε (-1) + (I * ) 𝐫₀ ε (-3) ∘SL 𝐱 i ∘SL 𝐱 i) All goals completed! 🐙 _ = 𝐫₀ ε (-1) ∘L i, 𝐱 i ∘L 𝐩 i + (-d * I * ) 𝐫₀ ε (-1) + (I * ) 𝐫₀ ε (-3) ∘L i, 𝐱 i ∘L 𝐱 i := d:ε:ˣ i, (𝐫₀ ε (-1) ∘SL 𝐱 i ∘SL 𝐩 i - (I * ) 𝐫₀ ε (-1) + (I * ) 𝐫₀ ε (-3) ∘SL 𝐱 i ∘SL 𝐱 i) = 𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐩 i + (-d * I * ) 𝐫₀ ε (-1) + (I * ) 𝐫₀ ε (-3) ∘SL i, 𝐱 i ∘SL 𝐱 i All goals completed! 🐙 _ = 𝐫₀ ε (-1) ∘L (𝐱 ⬝ᵥ 𝐩) - (I * * (d - 1)) 𝐫₀ ε (-1) - (I * * ε.1 ^ 2) 𝐫₀ ε (-3) := d:ε:ˣ𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐩 i + (-d * I * ) 𝐫₀ ε (-1) + (I * ) 𝐫₀ ε (-3) ∘SL i, 𝐱 i ∘SL 𝐱 i = 𝐫₀ ε (-1) ∘SL (𝐱 ⬝ᵥ 𝐩) - (I * * (d - 1)) 𝐫₀ ε (-1) - (I * * ε ^ 2) 𝐫₀ ε (-3) d:ε:ˣ𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐩 i + (-d * I * ) 𝐫₀ ε (-1) + ((I * ) 𝐫₀ ε (-3 + 2) - (I * * ε ^ 2) 𝐫₀ ε (-3)) = 𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐩 i - (I * * (d - 1)) 𝐫₀ ε (-1) - (I * * ε ^ 2) 𝐫₀ ε (-3) d:ε:ˣ𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐩 i + -(d * I * ) 𝐫₀ ε (-1) + ((I * ) 𝐫₀ ε (-1) - (I * * ε ^ 2) 𝐫₀ ε (-3)) = 𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐩 i - (d * I * - I * ) 𝐫₀ ε (-1) - (I * * ε ^ 2) 𝐫₀ ε (-3) simp_rw d:ε:ˣ𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐩 i + -(d * I * ) 𝐫₀ ε (-1) + ((I * ) 𝐫₀ ε (-1) - (I * * ε ^ 2) 𝐫₀ ε (-3)) = 𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐩 i - (d * I * - I * ) 𝐫₀ ε (-1) - (I * * ε ^ 2) 𝐫₀ ε (-3)d:ε:ˣ𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐩 i + -(d * I * ) 𝐫₀ ε (-1) + (I * ) 𝐫₀ ε (-1) - (I * * ε ^ 2) 𝐫₀ ε (-3) = 𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐩 i - (d * I * - I * ) 𝐫₀ ε (-1) - (I * * ε ^ 2) 𝐫₀ ε (-3) d:ε:ˣ𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐩 i + (-(d * I * ) 𝐫₀ ε (-1) + (I * ) 𝐫₀ ε (-1)) - (I * * ε ^ 2) 𝐫₀ ε (-3) = 𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐩 i - (d * I * - I * ) 𝐫₀ ε (-1) - (I * * ε ^ 2) 𝐫₀ ε (-3) d:ε:ˣ𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐩 i + (-(d * I * ) + I * ) 𝐫₀ ε (-1) - (I * * ε ^ 2) 𝐫₀ ε (-3) = 𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐩 i - (d * I * - I * ) 𝐫₀ ε (-1) - (I * * ε ^ 2) 𝐫₀ ε (-3) d:ε:ˣ𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐩 i + (-(d * I * ) + I * ) 𝐫₀ ε (-1) + -((I * * ε ^ 2) 𝐫₀ ε (-3)) = 𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐩 i + -((d * I * + -(I * )) 𝐫₀ ε (-1)) + -((I * * ε ^ 2) 𝐫₀ ε (-3)) d:ε:ˣ𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐩 i + (-(d * I * ) + I * ) 𝐫₀ ε (-1) + -(I * * ε ^ 2) 𝐫₀ ε (-3) = 𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐩 i + -(d * I * + -(I * )) 𝐫₀ ε (-1) + -(I * * ε ^ 2) 𝐫₀ ε (-3)] All goals completed! 🐙d:ε:ˣ𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐩 i = 𝐫₀ ε (-1) ∘SL (𝐱 ⬝ᵥ 𝐩); All goals completed! 🐙private lemma sum_rxrx (d : ) (ε : ˣ) : i, 𝐫₀[d] ε (-1) ∘L 𝐱 i ∘L 𝐫₀ ε (-1) ∘L 𝐱 i = ContinuousLinearMap.id 𝓢(Space d, ) - (ε.1 ^ 2) 𝐫₀ ε (-2) := d:ε:ˣ i, 𝐫₀ ε (-1) ∘SL 𝐱 i ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 i = ContinuousLinearMap.id 𝓢(Space d, ) - ε ^ 2 𝐫₀ ε (-2) simp_rw d:ε:ˣ i, 𝐫₀ ε (-1) ∘SL 𝐱 i ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 i = ContinuousLinearMap.id 𝓢(Space d, ) - ε ^ 2 𝐫₀ ε (-2)d:ε:ˣ𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 i = ContinuousLinearMap.id 𝓢(Space d, ) - ε ^ 2 𝐫₀ ε (-2) d:ε:ˣ𝐫₀ ε (-1) ∘SL x, (𝐱 x ∘SL 𝐫₀ ε (-1)) ∘SL 𝐱 x = ContinuousLinearMap.id 𝓢(Space d, ) - ε ^ 2 𝐫₀ ε (-2) d:ε:ˣ𝐫₀ ε (-1) ∘SL x, (𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL 𝐱 x = ContinuousLinearMap.id 𝓢(Space d, ) - ε ^ 2 𝐫₀ ε (-2) d:ε:ˣ𝐫₀ ε (-1) ∘SL x, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐱 x = ContinuousLinearMap.id 𝓢(Space d, ) - ε ^ 2 𝐫₀ ε (-2) d:ε:ˣ𝐫₀ ε (-1) ∘SL 𝐫₀ ε (-1) ∘SL i, 𝐱 i ∘SL 𝐱 i = ContinuousLinearMap.id 𝓢(Space d, ) - ε ^ 2 𝐫₀ ε (-2) d:ε:ˣ(𝐫₀ ε (-1) ∘SL 𝐫₀ ε (-1)) ∘SL i, 𝐱 i ∘SL 𝐱 i = ContinuousLinearMap.id 𝓢(Space d, ) - ε ^ 2 𝐫₀ ε (-2) d:ε:ˣ𝐫₀ ε (-1 + -1) ∘SL i, 𝐱 i ∘SL 𝐱 i = ContinuousLinearMap.id 𝓢(Space d, ) - ε ^ 2 𝐫₀ ε (-2) d:ε:ˣ𝐫₀ ε (-1 + -1) ∘SL (𝐫₀ ε 2 - ε ^ 2 ContinuousLinearMap.id 𝓢(Space d, )) = ContinuousLinearMap.id 𝓢(Space d, ) - ε ^ 2 𝐫₀ ε (-2)] d:ε:ˣ𝐫₀ ε (-2) ∘SL (𝐫₀ ε 2 - ε ^ 2 ContinuousLinearMap.id 𝓢(Space d, )) = ContinuousLinearMap.id 𝓢(Space d, ) - ε ^ 2 𝐫₀ ε (-2) All goals completed! 🐙

The square of the (regularized) LRL vector operator is related to the (regularized) Hamiltonian 𝐇(ε) of the hydrogen atom, square of the angular momentum 𝐋² and powers of 𝐫(ε) as 𝐀(ε)² = 2m·𝐇(ε)(𝐋² + ¼ℏ²(d-1)²) + m²k²(𝟙 - ε²·𝐫(ε)⁻²) - ½(d-1)mkℏ²ε²𝐫(ε)⁻³.

lemma lrlOperatorSqr_eq (ε : ˣ) : H.lrlOperator ε ⬝ᵥ H.lrlOperator ε = (2 * H.m) (H.hamiltonianRegCLM ε) ∘L (𝐋² + (4⁻¹ * ^ 2 * (H.d - 1) ^ 2 : ) ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) - ε.1 ^ 2 𝐫₀ ε (-2)) - (2⁻¹ * ^2 * H.m * H.k * (H.d - 1) * ε.1 ^ 2) 𝐫₀ ε (-3) := H:HydrogenAtomε:ˣH.lrlOperator ε ⬝ᵥ H.lrlOperator ε = (2 * H.m) H.hamiltonianRegCLM ε ∘SL (𝐋² + (4⁻¹ * ^ 2 * (H.d - 1) ^ 2) ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) - ε ^ 2 𝐫₀ ε (-2)) - (2⁻¹ * ^ 2 * H.m * H.k * (H.d - 1) * ε ^ 2) 𝐫₀ ε (-3) simp_rw H:HydrogenAtomε:ˣH.lrlOperator ε ⬝ᵥ H.lrlOperator ε = (2 * H.m) H.hamiltonianRegCLM ε ∘SL (𝐋² + (4⁻¹ * ^ 2 * (H.d - 1) ^ 2) ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) - ε ^ 2 𝐫₀ ε (-2)) - (2⁻¹ * ^ 2 * H.m * H.k * (H.d - 1) * ε ^ 2) 𝐫₀ ε (-3)H:HydrogenAtomε:ˣ i, H.lrlOperator ε i * H.lrlOperator ε i = (2 * H.m) H.hamiltonianRegCLM ε ∘SL (𝐋² + (4⁻¹ * ^ 2 * (H.d - 1) ^ 2) ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) - ε ^ 2 𝐫₀ ε (-2)) - (2⁻¹ * ^ 2 * H.m * H.k * (H.d - 1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ x, H.lrlOperator ε x ∘SL H.lrlOperator ε x = (2 * H.m) H.hamiltonianRegCLM ε ∘SL (𝐋² + (4⁻¹ * ^ 2 * (H.d - 1) ^ 2) ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) - ε ^ 2 𝐫₀ ε (-2)) - (2⁻¹ * ^ 2 * H.m * H.k * (H.d - 1) * ε ^ 2) 𝐫₀ ε (-3)] conv_lhs => H:HydrogenAtomε:ˣi:Fin H.d| H.lrlOperator ε i; H:HydrogenAtomε:ˣi:Fin H.d| 𝐋 i ⬝ᵥ 𝐩 + (2⁻¹ * I * * (H.d - 1)) 𝐩 i - (H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 i conv_lhs => H:HydrogenAtomε:ˣi:Fin H.d| H.lrlOperator ε i; H:HydrogenAtomε:ˣi:Fin H.d| 𝐩 ⬝ᵥ 𝐋 i - (2⁻¹ * I * * (H.d - 1)) 𝐩 i - (H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 i simp_rw H:HydrogenAtomε:ˣ i, (𝐋 i ⬝ᵥ 𝐩 + (2⁻¹ * I * * (H.d - 1)) 𝐩 i - (H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 i) ∘SL (𝐩 ⬝ᵥ 𝐋 i - (2⁻¹ * I * * (H.d - 1)) 𝐩 i - (H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 i) = (2 * H.m) H.hamiltonianRegCLM ε ∘SL (𝐋² + (4⁻¹ * ^ 2 * (H.d - 1) ^ 2) ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) - ε ^ 2 𝐫₀ ε (-2)) - (2⁻¹ * ^ 2 * H.m * H.k * (H.d - 1) * ε ^ 2) 𝐫₀ ε (-3)H:HydrogenAtomε:ˣ x, ( i, 𝐋 x i * 𝐩 i + (2⁻¹ * I * * (H.d - 1)) 𝐩 x - (H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL ( i, 𝐩 i * 𝐋 x i - (2⁻¹ * I * * (H.d - 1)) 𝐩 x - (H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x) = (2 * H.m) H.hamiltonianRegCLM ε ∘SL (𝐋² + (4⁻¹ * ^ 2 * (H.d - 1) ^ 2) ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) - ε ^ 2 𝐫₀ ε (-2)) - (2⁻¹ * ^ 2 * H.m * H.k * (H.d - 1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ x, ( x_1, 𝐋 x x_1 ∘SL 𝐩 x_1 + (2⁻¹ * I * * (H.d - 1)) 𝐩 x - (H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL ( x_1, 𝐩 x_1 ∘SL 𝐋 x x_1 - (2⁻¹ * I * * (H.d - 1)) 𝐩 x - (H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x) = (2 * H.m) H.hamiltonianRegCLM ε ∘SL (𝐋² + (4⁻¹ * ^ 2 * (H.d - 1) ^ 2) ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) - ε ^ 2 𝐫₀ ε (-2)) - (2⁻¹ * ^ 2 * H.m * H.k * (H.d - 1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ x, ( x_1, 𝐋 x x_1 ∘SL 𝐩 x_1 + (2⁻¹ * I * * (H.d + -1)) 𝐩 x + -((H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x)) ∘SL ( x_1, 𝐩 x_1 ∘SL 𝐋 x x_1 + -((2⁻¹ * I * * (H.d + -1)) 𝐩 x) + -((H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x)) = (2 * H.m) H.hamiltonianRegCLM ε ∘SL (𝐋² + (4⁻¹ * ^ 2 * (H.d + -1) ^ 2) ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) + -(ε ^ 2 𝐫₀ ε (-2))) + -((2⁻¹ * ^ 2 * H.m * H.k * (H.d + -1) * ε ^ 2) 𝐫₀ ε (-3)) H:HydrogenAtomε:ˣ x, ( x_1, 𝐋 x x_1 ∘SL 𝐩 x_1 + (2⁻¹ * I * * (H.d + -1)) 𝐩 x + -(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL ( x_1, 𝐩 x_1 ∘SL 𝐋 x x_1 + -(2⁻¹ * I * * (H.d + -1)) 𝐩 x + -(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x) = (2 * H.m) H.hamiltonianRegCLM ε ∘SL (𝐋² + (4⁻¹ * ^ 2 * (H.d + -1) ^ 2) ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) + -ε ^ 2 𝐫₀ ε (-2)) + -(2⁻¹ * ^ 2 * H.m * H.k * (H.d + -1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ x, ((∑ x_1, 𝐋 x x_1 ∘SL 𝐩 x_1) ∘SL ( x_1, 𝐩 x_1 ∘SL 𝐋 x x_1 + -(2⁻¹ * I * * (H.d + -1)) 𝐩 x + -(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x) + ((2⁻¹ * I * * (H.d + -1)) 𝐩 x) ∘SL ( x_1, 𝐩 x_1 ∘SL 𝐋 x x_1 + -(2⁻¹ * I * * (H.d + -1)) 𝐩 x + -(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x) + (-(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL ( x_1, 𝐩 x_1 ∘SL 𝐋 x x_1 + -(2⁻¹ * I * * (H.d + -1)) 𝐩 x + -(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x)) = (2 * H.m) H.hamiltonianRegCLM ε ∘SL (𝐋² + (4⁻¹ * ^ 2 * (H.d + -1) ^ 2) ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) + -ε ^ 2 𝐫₀ ε (-2)) + -(2⁻¹ * ^ 2 * H.m * H.k * (H.d + -1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ x, ((∑ x_1, 𝐋 x x_1 ∘SL 𝐩 x_1) ∘SL x_1, 𝐩 x_1 ∘SL 𝐋 x x_1 + (∑ x_1, 𝐋 x x_1 ∘SL 𝐩 x_1) ∘SL (-(2⁻¹ * I * * (H.d + -1)) 𝐩 x) + (∑ x_1, 𝐋 x x_1 ∘SL 𝐩 x_1) ∘SL (-(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x) + (((2⁻¹ * I * * (H.d + -1)) 𝐩 x) ∘SL x_1, 𝐩 x_1 ∘SL 𝐋 x x_1 + ((2⁻¹ * I * * (H.d + -1)) 𝐩 x) ∘SL (-(2⁻¹ * I * * (H.d + -1)) 𝐩 x) + ((2⁻¹ * I * * (H.d + -1)) 𝐩 x) ∘SL (-(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x)) + ((-(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL x_1, 𝐩 x_1 ∘SL 𝐋 x x_1 + (-(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL (-(2⁻¹ * I * * (H.d + -1)) 𝐩 x) + (-(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL (-(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x))) = (2 * H.m) (H.hamiltonianRegCLM ε ∘SL 𝐋² + H.hamiltonianRegCLM ε ∘SL ((4⁻¹ * ^ 2 * (H.d + -1) ^ 2) ContinuousLinearMap.id 𝓢(Space H.d, ))) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) + -ε ^ 2 𝐫₀ ε (-2)) + -(2⁻¹ * ^ 2 * H.m * H.k * (H.d + -1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ x, ((∑ x_1, 𝐋 x x_1 ∘SL 𝐩 x_1) ∘SL x_1, 𝐩 x_1 ∘SL 𝐋 x x_1 + (∑ x_1, 𝐋 x x_1 ∘SL 𝐩 x_1) ∘SL (-(2⁻¹ * I * * (H.d + -1)) 𝐩 x) + (∑ x_1, 𝐋 x x_1 ∘SL 𝐩 x_1) ∘SL (-(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x) + ((2⁻¹ * I * * (H.d + -1)) 𝐩 x ∘SL x_1, 𝐩 x_1 ∘SL 𝐋 x x_1 + (2⁻¹ * I * * (H.d + -1)) 𝐩 x ∘SL (-(2⁻¹ * I * * (H.d + -1)) 𝐩 x) + (2⁻¹ * I * * (H.d + -1)) 𝐩 x ∘SL (-(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x)) + (-(H.m * H.k) (𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL x_1, 𝐩 x_1 ∘SL 𝐋 x x_1 + -(H.m * H.k) (𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL (-(2⁻¹ * I * * (H.d + -1)) 𝐩 x) + -(H.m * H.k) (𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL (-(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐱 x))) = (2 * H.m) (H.hamiltonianRegCLM ε ∘SL 𝐋² + H.hamiltonianRegCLM ε ∘SL ((4⁻¹ * ^ 2 * (H.d + -1) ^ 2) ContinuousLinearMap.id 𝓢(Space H.d, ))) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) + -ε ^ 2 𝐫₀ ε (-2)) + -(2⁻¹ * ^ 2 * H.m * H.k * (H.d + -1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ x, ((∑ x_1, 𝐋 x x_1 ∘SL 𝐩 x_1) ∘SL x_1, 𝐩 x_1 ∘SL 𝐋 x x_1 + -(2⁻¹ * I * * (H.d + -1)) (∑ x_1, 𝐋 x x_1 ∘SL 𝐩 x_1) ∘SL 𝐩 x + -(H.m * H.k) (∑ x_1, 𝐋 x x_1 ∘SL 𝐩 x_1) ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x + ((2⁻¹ * I * * (H.d + -1)) 𝐩 x ∘SL x_1, 𝐩 x_1 ∘SL 𝐋 x x_1 + (2⁻¹ * I * * (H.d + -1)) -(2⁻¹ * I * * (H.d + -1)) 𝐩 x ∘SL 𝐩 x + (2⁻¹ * I * * (H.d + -1)) -(H.m * H.k) 𝐩 x ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x) + (-(H.m * H.k) (𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL x_1, 𝐩 x_1 ∘SL 𝐋 x x_1 + -(H.m * H.k) -(2⁻¹ * I * * (H.d + -1)) (𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL 𝐩 x + -(H.m * H.k) -(H.m * H.k) (𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x)) = (2 * H.m) (H.hamiltonianRegCLM ε ∘SL 𝐋² + (4⁻¹ * ^ 2 * (H.d + -1) ^ 2) H.hamiltonianRegCLM ε ∘SL ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) + -ε ^ 2 𝐫₀ ε (-2)) + -(2⁻¹ * ^ 2 * H.m * H.k * (H.d + -1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ x, ( i, (𝐋 x i ∘SL 𝐩 i) ∘SL x_1, 𝐩 x_1 ∘SL 𝐋 x x_1 + -(2⁻¹ * I * * (H.d + -1)) i, (𝐋 x i ∘SL 𝐩 i) ∘SL 𝐩 x + -(H.m * H.k) i, (𝐋 x i ∘SL 𝐩 i) ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x + ((2⁻¹ * I * * (H.d + -1)) 𝐩 x ∘SL x_1, 𝐩 x_1 ∘SL 𝐋 x x_1 + (2⁻¹ * I * * (H.d + -1)) -(2⁻¹ * I * * (H.d + -1)) 𝐩 x ∘SL 𝐩 x + (2⁻¹ * I * * (H.d + -1)) -(H.m * H.k) 𝐩 x ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x) + (-(H.m * H.k) (𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL x_1, 𝐩 x_1 ∘SL 𝐋 x x_1 + -(H.m * H.k) -(2⁻¹ * I * * (H.d + -1)) (𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL 𝐩 x + -(H.m * H.k) -(H.m * H.k) (𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x)) = (2 * H.m) (H.hamiltonianRegCLM ε ∘SL 𝐋² + (4⁻¹ * ^ 2 * (H.d + -1) ^ 2) H.hamiltonianRegCLM ε ∘SL ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) + -ε ^ 2 𝐫₀ ε (-2)) + -(2⁻¹ * ^ 2 * H.m * H.k * (H.d + -1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ x, ( x_1, i, (𝐋 x x_1 ∘SL 𝐩 x_1) ∘SL 𝐩 i ∘SL 𝐋 x i + -(2⁻¹ * I * * (H.d + -1)) i, (𝐋 x i ∘SL 𝐩 i) ∘SL 𝐩 x + -(H.m * H.k) i, (𝐋 x i ∘SL 𝐩 i) ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x + ((2⁻¹ * I * * (H.d + -1)) i, 𝐩 x ∘SL 𝐩 i ∘SL 𝐋 x i + (2⁻¹ * I * * (H.d + -1)) -(2⁻¹ * I * * (H.d + -1)) 𝐩 x ∘SL 𝐩 x + (2⁻¹ * I * * (H.d + -1)) -(H.m * H.k) 𝐩 x ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x) + (-(H.m * H.k) i, (𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL 𝐩 i ∘SL 𝐋 x i + -(H.m * H.k) -(2⁻¹ * I * * (H.d + -1)) (𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL 𝐩 x + -(H.m * H.k) -(H.m * H.k) (𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x)) = (2 * H.m) (H.hamiltonianRegCLM ε ∘SL 𝐋² + (4⁻¹ * ^ 2 * (H.d + -1) ^ 2) H.hamiltonianRegCLM ε ∘SL ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) + -ε ^ 2 𝐫₀ ε (-2)) + -(2⁻¹ * ^ 2 * H.m * H.k * (H.d + -1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ x, x_1, i, (𝐋 x x_1 ∘SL 𝐩 x_1) ∘SL 𝐩 i ∘SL 𝐋 x i + x, -(2⁻¹ * I * * (H.d + -1)) i, (𝐋 x i ∘SL 𝐩 i) ∘SL 𝐩 x + x, -(H.m * H.k) i, (𝐋 x i ∘SL 𝐩 i) ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x + ( x, (2⁻¹ * I * * (H.d + -1)) i, 𝐩 x ∘SL 𝐩 i ∘SL 𝐋 x i + x, (2⁻¹ * I * * (H.d + -1)) -(2⁻¹ * I * * (H.d + -1)) 𝐩 x ∘SL 𝐩 x + x, (2⁻¹ * I * * (H.d + -1)) -(H.m * H.k) 𝐩 x ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x) + ( x, -(H.m * H.k) i, (𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL 𝐩 i ∘SL 𝐋 x i + x, -(H.m * H.k) -(2⁻¹ * I * * (H.d + -1)) (𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL 𝐩 x + x, -(H.m * H.k) -(H.m * H.k) (𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x) = (2 * H.m) (H.hamiltonianRegCLM ε ∘SL 𝐋² + (4⁻¹ * ^ 2 * (H.d + -1) ^ 2) H.hamiltonianRegCLM ε ∘SL ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) + -ε ^ 2 𝐫₀ ε (-2)) + -(2⁻¹ * ^ 2 * H.m * H.k * (H.d + -1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ x, x_1, i, (𝐋 x x_1 ∘SL 𝐩 x_1) ∘SL 𝐩 i ∘SL 𝐋 x i + -(2⁻¹ * I * * (H.d + -1)) x, i, (𝐋 x i ∘SL 𝐩 i) ∘SL 𝐩 x + -(H.m * H.k) x, i, (𝐋 x i ∘SL 𝐩 i) ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x + ((2⁻¹ * I * * (H.d + -1)) x, i, 𝐩 x ∘SL 𝐩 i ∘SL 𝐋 x i + (2⁻¹ * I * * (H.d + -1)) -(2⁻¹ * I * * (H.d + -1)) x, 𝐩 x ∘SL 𝐩 x + (2⁻¹ * I * * (H.d + -1)) -(H.m * H.k) x, 𝐩 x ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x) + (-(H.m * H.k) x, i, (𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL 𝐩 i ∘SL 𝐋 x i + -(H.m * H.k) -(2⁻¹ * I * * (H.d + -1)) x, (𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL 𝐩 x + -(H.m * H.k) -(H.m * H.k) x, (𝐫₀ ε (-1) ∘SL 𝐱 x) ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x) = (2 * H.m) (H.hamiltonianRegCLM ε ∘SL 𝐋² + (4⁻¹ * ^ 2 * (H.d + -1) ^ 2) H.hamiltonianRegCLM ε ∘SL ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) + -ε ^ 2 𝐫₀ ε (-2)) + -(2⁻¹ * ^ 2 * H.m * H.k * (H.d + -1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ x, x_1, x_2, 𝐋 x x_1 ∘SL 𝐩 x_1 ∘SL 𝐩 x_2 ∘SL 𝐋 x x_2 + -(2⁻¹ * I * * (H.d + -1)) x, x_1, 𝐋 x x_1 ∘SL 𝐩 x_1 ∘SL 𝐩 x + -(H.m * H.k) x, x_1, 𝐋 x x_1 ∘SL 𝐩 x_1 ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x + ((2⁻¹ * I * * (H.d + -1)) x, i, 𝐩 x ∘SL 𝐩 i ∘SL 𝐋 x i + (2⁻¹ * I * * (H.d + -1)) -(2⁻¹ * I * * (H.d + -1)) x, 𝐩 x ∘SL 𝐩 x + (2⁻¹ * I * * (H.d + -1)) -(H.m * H.k) x, 𝐩 x ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x) + (-(H.m * H.k) x, x_1, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐩 x_1 ∘SL 𝐋 x x_1 + -(H.m * H.k) -(2⁻¹ * I * * (H.d + -1)) x, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐩 x + -(H.m * H.k) -(H.m * H.k) x, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x) = (2 * H.m) (H.hamiltonianRegCLM ε ∘SL 𝐋² + (4⁻¹ * ^ 2 * (H.d + -1) ^ 2) H.hamiltonianRegCLM ε ∘SL ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) + -ε ^ 2 𝐫₀ ε (-2)) + -(2⁻¹ * ^ 2 * H.m * H.k * (H.d + -1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ(𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋² + -(2⁻¹ * I * * (H.d + -1)) x, x_1, 𝐋 x x_1 ∘SL 𝐩 x_1 ∘SL 𝐩 x + -(H.m * H.k) x, x_1, 𝐋 x x_1 ∘SL 𝐩 x_1 ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x + ((2⁻¹ * I * * (H.d + -1)) x, i, 𝐩 x ∘SL 𝐩 i ∘SL 𝐋 x i + (2⁻¹ * I * * (H.d + -1)) -(2⁻¹ * I * * (H.d + -1)) x, 𝐩 x ∘SL 𝐩 x + (2⁻¹ * I * * (H.d + -1)) -(H.m * H.k) x, 𝐩 x ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x) + (-(H.m * H.k) x, x_1, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐩 x_1 ∘SL 𝐋 x x_1 + -(H.m * H.k) -(2⁻¹ * I * * (H.d + -1)) x, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐩 x + -(H.m * H.k) -(H.m * H.k) x, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x) = (2 * H.m) (H.hamiltonianRegCLM ε ∘SL 𝐋² + (4⁻¹ * ^ 2 * (H.d + -1) ^ 2) H.hamiltonianRegCLM ε ∘SL ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) + -ε ^ 2 𝐫₀ ε (-2)) + -(2⁻¹ * ^ 2 * H.m * H.k * (H.d + -1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ(𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋² + -(2⁻¹ * I * * (H.d + -1)) 0 + -(H.m * H.k) x, x_1, 𝐋 x x_1 ∘SL 𝐩 x_1 ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x + ((2⁻¹ * I * * (H.d + -1)) x, i, 𝐩 x ∘SL 𝐩 i ∘SL 𝐋 x i + (2⁻¹ * I * * (H.d + -1)) -(2⁻¹ * I * * (H.d + -1)) x, 𝐩 x ∘SL 𝐩 x + (2⁻¹ * I * * (H.d + -1)) -(H.m * H.k) x, 𝐩 x ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x) + (-(H.m * H.k) x, x_1, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐩 x_1 ∘SL 𝐋 x x_1 + -(H.m * H.k) -(2⁻¹ * I * * (H.d + -1)) x, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐩 x + -(H.m * H.k) -(H.m * H.k) x, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x) = (2 * H.m) (H.hamiltonianRegCLM ε ∘SL 𝐋² + (4⁻¹ * ^ 2 * (H.d + -1) ^ 2) H.hamiltonianRegCLM ε ∘SL ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) + -ε ^ 2 𝐫₀ ε (-2)) + -(2⁻¹ * ^ 2 * H.m * H.k * (H.d + -1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ(𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋² + -(2⁻¹ * I * * (H.d + -1)) 0 + -(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐋² + ((2⁻¹ * I * * (H.d + -1)) x, i, 𝐩 x ∘SL 𝐩 i ∘SL 𝐋 x i + (2⁻¹ * I * * (H.d + -1)) -(2⁻¹ * I * * (H.d + -1)) x, 𝐩 x ∘SL 𝐩 x + (2⁻¹ * I * * (H.d + -1)) -(H.m * H.k) x, 𝐩 x ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x) + (-(H.m * H.k) x, x_1, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐩 x_1 ∘SL 𝐋 x x_1 + -(H.m * H.k) -(2⁻¹ * I * * (H.d + -1)) x, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐩 x + -(H.m * H.k) -(H.m * H.k) x, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x) = (2 * H.m) (H.hamiltonianRegCLM ε ∘SL 𝐋² + (4⁻¹ * ^ 2 * (H.d + -1) ^ 2) H.hamiltonianRegCLM ε ∘SL ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) + -ε ^ 2 𝐫₀ ε (-2)) + -(2⁻¹ * ^ 2 * H.m * H.k * (H.d + -1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ(𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋² + -(2⁻¹ * I * * (H.d + -1)) 0 + -(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐋² + ((2⁻¹ * I * * (H.d + -1)) 0 + (2⁻¹ * I * * (H.d + -1)) -(2⁻¹ * I * * (H.d + -1)) x, 𝐩 x ∘SL 𝐩 x + (2⁻¹ * I * * (H.d + -1)) -(H.m * H.k) x, 𝐩 x ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x) + (-(H.m * H.k) x, x_1, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐩 x_1 ∘SL 𝐋 x x_1 + -(H.m * H.k) -(2⁻¹ * I * * (H.d + -1)) x, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐩 x + -(H.m * H.k) -(H.m * H.k) x, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x) = (2 * H.m) (H.hamiltonianRegCLM ε ∘SL 𝐋² + (4⁻¹ * ^ 2 * (H.d + -1) ^ 2) H.hamiltonianRegCLM ε ∘SL ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) + -ε ^ 2 𝐫₀ ε (-2)) + -(2⁻¹ * ^ 2 * H.m * H.k * (H.d + -1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ(𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋² + -(2⁻¹ * I * * (H.d + -1)) 0 + -(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐋² + ((2⁻¹ * I * * (H.d + -1)) 0 + (2⁻¹ * I * * (H.d + -1)) -(2⁻¹ * I * * (H.d + -1)) x, 𝐩 x ∘SL 𝐩 x + (2⁻¹ * I * * (H.d + -1)) -(H.m * H.k) (𝐫₀ ε (-1) ∘SL (𝐱 ⬝ᵥ 𝐩) - (I * * (H.d - 1)) 𝐫₀ ε (-1) - (I * * ε ^ 2) 𝐫₀ ε (-3))) + (-(H.m * H.k) x, x_1, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐩 x_1 ∘SL 𝐋 x x_1 + -(H.m * H.k) -(2⁻¹ * I * * (H.d + -1)) x, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐩 x + -(H.m * H.k) -(H.m * H.k) x, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x) = (2 * H.m) (H.hamiltonianRegCLM ε ∘SL 𝐋² + (4⁻¹ * ^ 2 * (H.d + -1) ^ 2) H.hamiltonianRegCLM ε ∘SL ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) + -ε ^ 2 𝐫₀ ε (-2)) + -(2⁻¹ * ^ 2 * H.m * H.k * (H.d + -1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ(𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋² + -(2⁻¹ * I * * (H.d + -1)) 0 + -(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐋² + ((2⁻¹ * I * * (H.d + -1)) 0 + (2⁻¹ * I * * (H.d + -1)) -(2⁻¹ * I * * (H.d + -1)) x, 𝐩 x ∘SL 𝐩 x + (2⁻¹ * I * * (H.d + -1)) -(H.m * H.k) (𝐫₀ ε (-1) ∘SL (𝐱 ⬝ᵥ 𝐩) - (I * * (H.d - 1)) 𝐫₀ ε (-1) - (I * * ε ^ 2) 𝐫₀ ε (-3))) + (-(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐋² + -(H.m * H.k) -(2⁻¹ * I * * (H.d + -1)) x, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐩 x + -(H.m * H.k) -(H.m * H.k) x, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x) = (2 * H.m) (H.hamiltonianRegCLM ε ∘SL 𝐋² + (4⁻¹ * ^ 2 * (H.d + -1) ^ 2) H.hamiltonianRegCLM ε ∘SL ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) + -ε ^ 2 𝐫₀ ε (-2)) + -(2⁻¹ * ^ 2 * H.m * H.k * (H.d + -1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ(𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋² + -(2⁻¹ * I * * (H.d + -1)) 0 + -(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐋² + ((2⁻¹ * I * * (H.d + -1)) 0 + (2⁻¹ * I * * (H.d + -1)) -(2⁻¹ * I * * (H.d + -1)) x, 𝐩 x ∘SL 𝐩 x + (2⁻¹ * I * * (H.d + -1)) -(H.m * H.k) (𝐫₀ ε (-1) ∘SL (𝐱 ⬝ᵥ 𝐩) - (I * * (H.d - 1)) 𝐫₀ ε (-1) - (I * * ε ^ 2) 𝐫₀ ε (-3))) + (-(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐋² + -(H.m * H.k) -(2⁻¹ * I * * (H.d + -1)) 𝐫₀ ε (-1) ∘SL (𝐱 ⬝ᵥ 𝐩) + -(H.m * H.k) -(H.m * H.k) x, 𝐫₀ ε (-1) ∘SL 𝐱 x ∘SL 𝐫₀ ε (-1) ∘SL 𝐱 x) = (2 * H.m) (H.hamiltonianRegCLM ε ∘SL 𝐋² + (4⁻¹ * ^ 2 * (H.d + -1) ^ 2) H.hamiltonianRegCLM ε ∘SL ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) + -ε ^ 2 𝐫₀ ε (-2)) + -(2⁻¹ * ^ 2 * H.m * H.k * (H.d + -1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ(𝐩 ⬝ᵥ 𝐩) ∘SL 𝐋² + -(2⁻¹ * I * * (H.d + -1)) 0 + -(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐋² + ((2⁻¹ * I * * (H.d + -1)) 0 + (2⁻¹ * I * * (H.d + -1)) -(2⁻¹ * I * * (H.d + -1)) x, 𝐩 x ∘SL 𝐩 x + (2⁻¹ * I * * (H.d + -1)) -(H.m * H.k) (𝐫₀ ε (-1) ∘SL (𝐱 ⬝ᵥ 𝐩) - (I * * (H.d - 1)) 𝐫₀ ε (-1) - (I * * ε ^ 2) 𝐫₀ ε (-3))) + (-(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐋² + -(H.m * H.k) -(2⁻¹ * I * * (H.d + -1)) 𝐫₀ ε (-1) ∘SL (𝐱 ⬝ᵥ 𝐩) + -(H.m * H.k) -(H.m * H.k) (ContinuousLinearMap.id 𝓢(Space H.d, ) - ε ^ 2 𝐫₀ ε (-2))) = (2 * H.m) (H.hamiltonianRegCLM ε ∘SL 𝐋² + (4⁻¹ * ^ 2 * (H.d + -1) ^ 2) H.hamiltonianRegCLM ε ∘SL ContinuousLinearMap.id 𝓢(Space H.d, )) + (H.m ^ 2 * H.k ^ 2) (ContinuousLinearMap.id 𝓢(Space H.d, ) + -ε ^ 2 𝐫₀ ε (-2)) + -(2⁻¹ * ^ 2 * H.m * H.k * (H.d + -1) * ε ^ 2) 𝐫₀ ε (-3)] H:HydrogenAtomε:ˣ(∑ x, 𝐩 x ∘SL 𝐩 x) ∘SL 𝐋² + (-H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐋² + ((2⁻¹ * I * * (H.d + -1) * (-2⁻¹ * I * * (H.d + -1))) x, 𝐩 x ∘SL 𝐩 x + ((2⁻¹ * I * * (H.d + -1) * (-H.m * H.k)) 𝐫₀ ε (-1) ∘SL x, 𝐱 x ∘SL 𝐩 x + (2⁻¹ * I * * (H.d + -1) * (-H.m * H.k * (-I * * (H.d + -1)))) 𝐫₀ ε (-1) + (2⁻¹ * I * * (H.d + -1) * (-H.m * H.k * (-I * * ε ^ 2))) 𝐫₀ ε (-3))) + ((-H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐋² + (-H.m * H.k * (-2⁻¹ * I * * (H.d + -1))) 𝐫₀ ε (-1) ∘SL x, 𝐱 x ∘SL 𝐩 x + ((-H.m * H.k * (-H.m * H.k)) ContinuousLinearMap.id 𝓢(Space H.d, ) + (-H.m * H.k * (-H.m * H.k * -ε ^ 2)) 𝐫₀ ε (-2))) = (2 * H.m) ((2 * H.m)⁻¹ x, 𝐩 x ∘SL 𝐩 x + -H.k 𝐫₀ ε (-1)) ∘SL 𝐋² + (2 * H.m * (4⁻¹ * ^ 2 * (H.d + -1) ^ 2)) ((2 * H.m)⁻¹ x, 𝐩 x ∘SL 𝐩 x + -H.k 𝐫₀ ε (-1)) ∘SL ContinuousLinearMap.id 𝓢(Space H.d, ) + ((H.m ^ 2 * H.k ^ 2) ContinuousLinearMap.id 𝓢(Space H.d, ) + (H.m ^ 2 * H.k ^ 2 * -ε ^ 2) 𝐫₀ ε (-2)) + (-2⁻¹ * ^ 2 * H.m * H.k * (H.d + -1) * ε ^ 2) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣ(∑ x, 𝐩 x ∘SL 𝐩 x) ∘SL 𝐋² + -(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐋² + ((I ^ 2 * ^ 2 * (-1 / 4) + I ^ 2 * ^ 2 * H.d * (1 / 2) + I ^ 2 * ^ 2 * H.d ^ 2 * (-1 / 4)) x, 𝐩 x ∘SL 𝐩 x + ((H.m * H.k * I * * (1 / 2) + H.m * H.k * I * * H.d * (-1 / 2)) 𝐫₀ ε (-1) ∘SL x, 𝐱 x ∘SL 𝐩 x + (H.m * H.k * I ^ 2 * ^ 2 * (1 / 2) - H.m * H.k * I ^ 2 * ^ 2 * H.d + H.m * H.k * I ^ 2 * ^ 2 * H.d ^ 2 * (1 / 2)) 𝐫₀ ε (-1) + (H.m * H.k * I ^ 2 * ^ 2 * H.d * ε ^ 2 * (1 / 2) + H.m * H.k * I ^ 2 * ^ 2 * ε ^ 2 * (-1 / 2)) 𝐫₀ ε (-3))) + (-(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐋² + (H.m * H.k * I * * (-1 / 2) + H.m * H.k * I * * H.d * (1 / 2)) 𝐫₀ ε (-1) ∘SL x, 𝐱 x ∘SL 𝐩 x + ((H.m ^ 2 * H.k ^ 2) ContinuousLinearMap.id 𝓢(Space H.d, ) + -(H.m ^ 2 * H.k ^ 2 * ε ^ 2) 𝐫₀ ε (-2))) = (H.m * 2) (((↑H.m)⁻¹ * (1 / 2)) x, 𝐩 x ∘SL 𝐩 x + -H.k 𝐫₀ ε (-1)) ∘SL 𝐋² + (H.m * ^ 2 * (-1 + H.d) ^ 2 * (1 / 2)) (((↑H.m)⁻¹ * (1 / 2)) x, 𝐩 x ∘SL 𝐩 x + -H.k 𝐫₀ ε (-1)) ∘SL ContinuousLinearMap.id 𝓢(Space H.d, ) + ((H.m ^ 2 * H.k ^ 2) ContinuousLinearMap.id 𝓢(Space H.d, ) + -(H.m ^ 2 * H.k ^ 2 * ε ^ 2) 𝐫₀ ε (-2)) + (H.m * H.k * ^ 2 * ε ^ 2 * (-1 + H.d) * (-1 / 2)) 𝐫₀ ε (-3) H:HydrogenAtomε:ˣx✝¹:𝓢(Space H.d, )x✝:Space H.d(((∑ x, 𝐩 x ∘SL 𝐩 x) ∘SL 𝐋² + -(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐋² + ((I ^ 2 * ^ 2 * (-1 / 4) + I ^ 2 * ^ 2 * H.d * (1 / 2) + I ^ 2 * ^ 2 * H.d ^ 2 * (-1 / 4)) x, 𝐩 x ∘SL 𝐩 x + ((H.m * H.k * I * * (1 / 2) + H.m * H.k * I * * H.d * (-1 / 2)) 𝐫₀ ε (-1) ∘SL x, 𝐱 x ∘SL 𝐩 x + (H.m * H.k * I ^ 2 * ^ 2 * (1 / 2) - H.m * H.k * I ^ 2 * ^ 2 * H.d + H.m * H.k * I ^ 2 * ^ 2 * H.d ^ 2 * (1 / 2)) 𝐫₀ ε (-1) + (H.m * H.k * I ^ 2 * ^ 2 * H.d * ε ^ 2 * (1 / 2) + H.m * H.k * I ^ 2 * ^ 2 * ε ^ 2 * (-1 / 2)) 𝐫₀ ε (-3))) + (-(H.m * H.k) 𝐫₀ ε (-1) ∘SL 𝐋² + (H.m * H.k * I * * (-1 / 2) + H.m * H.k * I * * H.d * (1 / 2)) 𝐫₀ ε (-1) ∘SL x, 𝐱 x ∘SL 𝐩 x + ((H.m ^ 2 * H.k ^ 2) ContinuousLinearMap.id 𝓢(Space H.d, ) + -(H.m ^ 2 * H.k ^ 2 * ε ^ 2) 𝐫₀ ε (-2)))) x✝¹) x✝ = (((H.m * 2) (((↑H.m)⁻¹ * (1 / 2)) x, 𝐩 x ∘SL 𝐩 x + -H.k 𝐫₀ ε (-1)) ∘SL 𝐋² + (H.m * ^ 2 * (-1 + H.d) ^ 2 * (1 / 2)) (((↑H.m)⁻¹ * (1 / 2)) x, 𝐩 x ∘SL 𝐩 x + -H.k 𝐫₀ ε (-1)) ∘SL ContinuousLinearMap.id 𝓢(Space H.d, ) + ((H.m ^ 2 * H.k ^ 2) ContinuousLinearMap.id 𝓢(Space H.d, ) + -(H.m ^ 2 * H.k ^ 2 * ε ^ 2) 𝐫₀ ε (-2)) + (H.m * H.k * ^ 2 * ε ^ 2 * (-1 + H.d) * (-1 / 2)) 𝐫₀ ε (-3)) x✝¹) x✝ H:HydrogenAtomε:ˣx✝¹:𝓢(Space H.d, )x✝:Space H.d((∑ x, 𝐩 x ∘SL 𝐩 x) (𝐋² x✝¹)) x✝ + -(H.m * H.k) * ((𝐫₀ ε (-1)) (𝐋² x✝¹)) x✝ + ((I ^ 2 * ^ 2 * (-1 / 4) + I ^ 2 * ^ 2 * H.d * (1 / 2) + I ^ 2 * ^ 2 * H.d ^ 2 * (-1 / 4)) * ((∑ x, 𝐩 x ∘SL 𝐩 x) x✝¹) x✝ + ((H.m * H.k * I * * (1 / 2) + H.m * H.k * I * * H.d * (-1 / 2)) * ((𝐫₀ ε (-1)) ((∑ x, 𝐱 x ∘SL 𝐩 x) x✝¹)) x✝ + (H.m * H.k * I ^ 2 * ^ 2 * (1 / 2) - H.m * H.k * I ^ 2 * ^ 2 * H.d + H.m * H.k * I ^ 2 * ^ 2 * H.d ^ 2 * (1 / 2)) * ((𝐫₀ ε (-1)) x✝¹) x✝ + (H.m * H.k * I ^ 2 * ^ 2 * H.d * ε ^ 2 * (1 / 2) + H.m * H.k * I ^ 2 * ^ 2 * ε ^ 2 * (-1 / 2)) * ((𝐫₀ ε (-3)) x✝¹) x✝)) + (-(H.m * H.k) * ((𝐫₀ ε (-1)) (𝐋² x✝¹)) x✝ + (H.m * H.k * I * * (-1 / 2) + H.m * H.k * I * * H.d * (1 / 2)) * ((𝐫₀ ε (-1)) ((∑ x, 𝐱 x ∘SL 𝐩 x) x✝¹)) x✝ + (H.m ^ 2 * H.k ^ 2 * (id x✝¹) x✝ + -(H.m ^ 2 * H.k ^ 2 * ε ^ 2) * ((𝐫₀ ε (-2)) x✝¹) x✝)) = H.m * 2 * ((↑H.m)⁻¹ * (1 / 2) * ((∑ x, 𝐩 x ∘SL 𝐩 x) (𝐋² x✝¹)) x✝ + -H.k * ((𝐫₀ ε (-1)) (𝐋² x✝¹)) x✝) + H.m * ^ 2 * (-1 + H.d) ^ 2 * (1 / 2) * ((↑H.m)⁻¹ * (1 / 2) * ((∑ x, 𝐩 x ∘SL 𝐩 x) (id x✝¹)) x✝ + -H.k * ((𝐫₀ ε (-1)) (id x✝¹)) x✝) + (H.m ^ 2 * H.k ^ 2 * (id x✝¹) x✝ + -(H.m ^ 2 * H.k ^ 2 * ε ^ 2) * ((𝐫₀ ε (-2)) x✝¹) x✝) + H.m * H.k * ^ 2 * ε ^ 2 * (-1 + H.d) * (-1 / 2) * ((𝐫₀ ε (-3)) x✝¹) x✝ All goals completed! 🐙