AI 中文总结
本文提出延迟接受算法的可达状态算子形式化，通过三个不变量证明终止与稳定性，并区分轨迹性质与格结构及策略证明性，提供结构诊断表，不涉及新复杂性结论。
AI 中文摘要
我们给出了一对一延迟接受的可达状态算子形式化，该形式化针对严格且可能不完整的偏好列表。为每个活跃的提议者定义了一个局部更新算子，而调度器则选择应用哪个局部更新。在从规范的空初始状态可达的状态上，三个不变量是直接的：提议边的集合严格增长，每个提议者至多访问每个可接受的接收者一次，并且每个接收者持有迄今为止收到的最偏好的提议。这些不变量产生了至多|E|次提议后的终止以及每个可达终止状态的稳定性。经典拒绝引理随后给出了提议者最优性和调度无关性。我们将这些轨迹陈述与两个逻辑上不同的结果分开：完整稳定匹配集合的分配格结构和单侧策略证明性。一个诊断表记录了当模型改变二分划分、序数比较、提议不可逆性或接收者选择规则时，哪个证明义务会丢失。本文没有提出新的复杂性主张；其目的是对经典证明架构及其架构局限性进行精确的算子级描述。
英文摘要
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 initial state, three invariants are immediate: the set of proposed edges grows strictly, every proposer visits each acceptable receiver at most once, and every receiver holds its most-preferred proposal received so far. These invariants yield termination after at most |E| proposals and stability of every terminal reachable state. The classical rejection lemma then gives proposer optimality and schedule independence. We separate these trajectory statements from two logically different results: the distributive-lattice structure of the full stable-matching set and one-sided strategy-proofness. A diagnostic table records which proof obligation is lost when a model changes the bipartition, ordinal comparisons, proposal irreversibility, or receiver choice rule. The paper makes no new complexity claim; its purpose is a precise operator-level account of the classical proof architecture and of the limits of that architecture.
Comments6 pages, 1 table. Structural note on deferred acceptance with strict, possibly incomplete preference lists
