A Reachable-State Operator Formulation of Deferred Acceptance: Progress Invariants and Structural Diagnostics

We give a reachable-state operator formulation of one-to-one deferred acceptance with strict, possibly incomplete preference lists. A local update operator is defined for each active proposer, while a scheduler selects which local update is applied. On the states reachable from the canonical empty i