> I think the first sentence is very confusing...
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.
Thanks for responding. I don't know APL, so was just trying to follow the body text. I should have also mentioned at the outset: This idea and algorithm is very neat!
> 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
I'm claiming that one part of this argument remains to be shown: Namely, that the sequence of partial sums of the tail sequence itself (i.e., the sequence s_{i+1}, s_{i+1}+s_{i+2}, ..., s_{i+1}+...+s_n) never dips below 1. This is clearly a necessary condition (since if it's violated, the result after rotation will be invalid), and I don't yet see how it's implied by what you've written (certainly I can construct a sequence of 1s and -1s that sum to N+1 but do have some initial partial sum below 1).
For me, the fact that the argument you have made so far doesn't "make use of" the "rightmost lowest" property of i's construction is also a hint that there might be a gap here. (In my experience, when you choose/construct a witness this way, i.e., to optimise some quantity, it's always so that you can later show a contradiction to rule out some troublesome case.)