A relaxation-free variant of Dijkstra's shortest path algorithm

Question

I have come up with a relaxation-free variant of Dijkstra's shortest path algorithm, and I would like to see if it's correct. Here is the pseudocode for finding the shortest distance from a node $\alpha$ to another node $\beta$.

1. Initialize an empty priority queue $Q$ and an empty hash map $H$.
2. Add $\alpha$ to $Q$ with a "distance" of $0$.
3. While $Q$ is not empty,
   1. Pop the node with the shortest distance. Denote the node with $n$ and its distance with $d$.
   2. If $n = \beta$, then return $d$.
   3. If $n$ is present in $H$, then continue to the next iteration.
   4. Add $n$ to $H$ with a distance value of $d$.
   5. For each neighbor $m$ of $n$, denote the distance from $n$ to $m$ with $w$
      1. Add $m$ to $Q$ with a distance value of $d + w$.
4. If we reach here, then it's impossible to reach $b$ from $a$.

(Note that you can replace the hash map $H$ with a hash set because only the presence of keys matters. I used a hash map solely to make the analysis easier.)

---

Analysis: First we show that when we pop a "distance" of $d$ from $Q$, all valid "routes" starting from $\alpha$ with a "distance" smaller than $d$ have already been "explored". Suppose there exists an unexplored shorter route. Denote the last explored node on that route with $u$ (there exists at least one explored node on that route, i.e. $\alpha$), and the first unexplored node on that route with $v$ (such a node exists since the route is unexplored). Since $u$ has been explored, $Q$ contains all of its immediate neighbours, including $v$. The distance between $a$ and $v$ is smaller than the total distance of that route, which is smaller than $d$ by construction. Given that $v$ is in $Q$ with a smaller distance than $d$, the priority queue should popped it before popping $n$, but $u$ is still unexplored when processing $n$, which creates a contradiction.

If a newly popped node $n$ is not in $H$, then $n$ has not been reached until now, which means it is impossible to reach $n$ with a distance shorter than $d$. Thus, $d$ is the shortest possible distance from $a$ to $n$, so the algorithm always gives the correct result.

Question: Am I right? How do I express the proof of correctness more formally? The analysis above doesn't seem formal enough since I did not rigorously define concepts like "distance", "route", "explore", "first", and "last". This is probably in turn because the pseudocode is not clear enough to enable rigorous reasoning, so I am happy to provide clarification.

As a bonus, does my variant run faster or take less space than the vanilla algorithm?

---

(I am aware that we have a similar question on this site, but my algorithm is different from Leo's. Moreover, Leo edited their question after an answer has been posted, rendering it stale.)