A striking aspects in the theory of shared-memory distributed systems is that the existence of algorithms depends on subtle assumptions at the level of granularity of interaction, both regarding scheduling and memory models. A central result in this context is the Variable Coverage Theorem (VC Theorem): “Any n-processor no-deadlock mutual exclusion algorithm using only read/write registers must use at least n shared variables.” The traditional textbook proofs of this result are informal and based on different operational models of shared-memory systems involving a detailed combinatorial analysis of the scheduling in the chosen model. In these notes, we revisit the VC Theorem from an axiomatic perspective. We transcribe the proofs into a strict formal argument using modal logic. Thus abstracting from the concrete operational setting, we are able to separate the purely combinatorial parts of the proofs from those aspects that pertain to the read/write interaction architecture and those that relate to the concrete mutex synchronisation problem. Specifically, we characterise the key limitation of the read/write memory model from which the impossibility result ultimately stems, in a single closure axiom, the Variable Cover Axiom. This axiom plays a role akin to the Pumping Lemma for regular or context-free languages.