B.5.MPC:5.3 - Maintain an admission bound through material tokens
A demonstration room should contain at most three visitors. Initially the room is empty and three distinct material cards are available. An attendant gives a free card to one visitor before entry. That visitor keeps it while inside and returns it after leaving. A new visitor waits for a card when none is free.
For this case, every entrance and exit follows the procedure, each card is exclusively assigned to one visitor at a time, and cards are neither lost nor duplicated. The material arrangement makes exclusive acquisition possible: taking the available card removes that same card from the free stock. A photograph or printed copy of the card is not accepted for entry.
First consider a moment when every assigned card is held by a visitor inside and every other card is free. The one-card-per-visitor rule gives:
occupancy = 3 − number of free cards
During admission and return, cards can also be held by visitors outside. A visitor may already hold a card while waiting to enter; a departed visitor may still be walking to its return point. To preserve the physical meaning during those intervals, distinguish four states for each card:
| State | Physical interpretation |
|---|---|
| Free | The card is available for a new admission. |
| Reserved | The card is held by a visitor who has not yet entered. |
| Inside | The card is held by its visitor inside the room. |
| Awaiting return | Its visitor has left, but the card is not yet free. |
Let F, R, I and E count cards in those four states. Every card occupies exactly one state, so F + R + I + E = 3. Under the visitor-to-card rule, occupancy = I. Therefore:
occupancy = I = 3 − F − R − E
occupancy ≤ 3 − F ≤ 3
The transition procedure has four ordinary operations: issue one free card to a waiting visitor; admit that card’s visitor; let the visitor leave with the card; and return the departed visitor’s card to the free stock. Their state changes are Free → Reserved → Inside → Awaiting return → Free. A cancelled admission can return a Reserved card directly to Free while its visitor remains outside.
Each operation moves one existing card between states. Issuing a card requires a free card; entering requires its exclusive reservation; returning it requires that its visitor is already outside. Those conditions preserve the total stock and the association between visitors inside and Inside cards. The argument establishes the capacity bound for every sequence of those permitted operations, including overlapping visits.
Work two entries followed by one exit:
| Operation just completed | F | R | I | E | Occupancy |
|---|---|---|---|---|---|
| Initial arrangement | 3 | 0 | 0 | 0 | 0 |
| Issue card A | 2 | 1 | 0 | 0 | 0 |
| Visitor A enters | 2 | 0 | 1 | 0 | 1 |
| Issue card B | 1 | 1 | 1 | 0 | 1 |
| Visitor B enters | 1 | 0 | 2 | 0 | 2 |
| Visitor A leaves | 1 | 0 | 1 | 1 | 1 |
| Return card A | 2 | 0 | 1 | 0 | 1 |
Counting free cards gives an upper bound on occupancy during handover and return. It gives the exact occupancy when R = E = 0. That distinction changes what an observer may infer from the same stock. The admission rule can preserve the bound without an exact instantaneous occupancy readout.
Connect the abstract transition rule to the physical means. Exclusive possession realizes consumption of a free token. Carrying it through entry preserves the visitor association. Returning it only after exit prevents its use for a fourth visitor while the first three remain inside. If a visitor passes their card to someone outside while staying inside, the allowed-transition premise fails: the reused card no longer represents one occupied or reserved place.
A second entrance needs access to the same total stock. A copied stock of three additional accepted cards permits six simultaneous admissions, even if both attendants follow their local rule correctly. A shared pool of the original three cards preserves the common bound. Partitioning those same cards, for example two at one entrance and one at the other, also preserves it. The partition can make a visitor wait at one entrance while a card is free at the other; redistribution then needs a transfer of an existing free card.
The useful result is a conditional admission design and an interpretation of its observable stock. Its computational contribution is a finite-state procedure that answers whether an admission can proceed and maintains the relevant count. People and material transfers can execute it without a digital program. The invariant does not establish fair waiting, fast entry or detection of every procedural violation; those are different questions with their own needed contributions.
The coordinating Method makes the physical card and room-boundary rules, mathematical invariant and executing procedure agree. This is also why changing the stock or the return rule changes the joint result even when the counting arithmetic remains correct.