Fair. You clearly engage with my article on a real level. More comments like yours will probably make my writing better. So, thanks!
That said, the code does precisely define s_i, which is s[i] in linearized notation. I scribbled the article together at 2am after a long day at work because a colleague asked for it and assume that you know APL or are at least willing try reading the code blocks.
> I think there's a much clearer way to prove this...
Honestly, I'm not a fan of arguments by contradiction when a clear constructive proof is available: The sequence of partial sums ends in 1; there is a rightmost partial sum that achieves the minimum partial sum, -N, say at index i. The remaining 1s and ¯1s, from index i+1 to the end, clearly must sum to N+1. Thus, left-rotating the sequence by i elements results in a strict ballot sequence. This is procedural and directly translates to the code.