@spelunker Is there anything in particular you need explained or clarified?
While my current implementation is javascript, I didn't "write" it so much as prompted ChatGPT to write it, and since I did it very step by step, it should be easy to follow.
Here is the chatGPT conversation: https://sharegpt.com/c/fyOiNHy
It didn't make any mistakes, so it is pretty easy to follow, but I was careful in terms of prompting it to do one thing at a time.
Here is the codepen: https://codepen.io/karmatics/pen/KKxeEEJ?editors=1010
First I asked ChatGPT to parse ranked ballots and put them into a reasonable data structure. Then I had it so it could clone that data structure and remove a candidate (from the list of candidates as well as from the ballots), to allow for elimination.
Then I made a function "doPlurality" to do a plurality calculation on that, and return the winner(s) in an array (in case of tie it can be more than one). Then I had that function be able to do it inverted, to find the plurality loser.
Then I had it make a function "doIRV": to do an IRV tabulation on it, which in turn calls the "doPlurality" function multiple times, inverted so it picks the loser so that candidate can be eliminated. Then I made sure doIRV could be inverted itself.
Finally, I made doIRV so it can recurse to a given depth, which means that, instead of calling doPlurality to find candidates to eliminate, it calls doIRV. (until it reaches the specified depth, when it will call doPlurality)
I'm not sure what you are looking for as a formal definition, but if you need something else please let me know. It would be awesome if you were able to do some kind of proof.