As corrobrating evidence, I can mention the syntax-case implementation in
SRFI-72. That implementation satisfies declarative descriptions of hygiene.
However, the implementation technique is based on an "implicitized" version
of explicit renaming, not marking/substitution. There are some highly
obscure corner cases where it behaves differently from the marking algorithm,
while still satisfying hygiene. I have to recheck, but I think these
ambiguities should be resolved by specifying the algorithm as is
done here (though perhaps a little more detail might be required).