"Every variable occurs at most four times" is split into the two consequences the two halves of the theorem actually use. $app_inj$ — distinct occurrences of one variable carry distinct appearance indices — is what the correctness of the reduction needs: it makes the deadlines of one variable's occurrences pairwise distinct. $var_le$ is what its running time needs: without a bound tying the number of variables to the length of the word, a two-entry word could declare $2^{100}$ variables, and the reduction would have to emit that many jobs. Requiring surjectivity of the appearance index would give both, and more than either needs.

The appearance index is part of the input rather than something a reader computes. It is what the reduction of Theorem 2 turns into a deadline, and requiring it to be supplied and to be consistent is what makes the deadlines of one variable's occurrences distinct. That all four indices actually occur is never used, and is not required here; what is required instead is the weaker $var_le$, which is the part of the counting a reduction running in bounded time cannot do without.

A formula is presented directly, not as a satisfying assignment or any other certificate: the yes-instances are the satisfiable words, and satisfiability is quantified over assignments to the variables the word declares.

Sign bits are numbers, $1$ for a positive occurrence and anything else for a negative one, because a word RAM holds numbers. Reading a sign is then a comparison, as the emitted machine does.