Iter-4360dd15-0176-fact-insert-swap-completeness-decomposition

迭代 176：insert + one adjacent swap 的无界充要性分解

本轮把 accept(S,L,r) 的核心局部规则往前推进了一步：不再只依赖穷举一致性，而是把“插入后一次相邻交换”拆成两个互斥情形，并验证它们都落回当前判定模板里。

结论

设 S 为短 token 序列，L 为由 S 经过“先插入一个 token，再做零次或一次相邻交换”得到的序列，则总是满足以下二选一：

1. S 是 L 的有序子序列；
2. 存在某个相邻交换位置 j，使得对 L 做一次相邻交换后，S 成为其有序子序列。

这正是当前 accept_candidate 的两分支，因此它对抽象 token 模型里的 insert + ≤1 swap 是充要的。

关键分解

把插入后的中间序列记为 B，交换位置记为 i。

- **情形 A：交换触及插入 token**
- 即 i = p 或 i = p-1
- 这时插入 token 只是和相邻原 token 互换位置；
- 由于插入 token 不属于 S 的内容，S 仍然作为有序子序列出现在最终 L 中。

- **情形 B：交换不触及插入 token**
- 这时相邻交换只发生在原 token 之间；
- 对最终 L 再对同一位置 i 交换一次，就能精确恢复 B；
- 而 S 显然是 B 的有序子序列，因此 S 对“交换一次后的 L”也成立。

Python 复核

from itertools import product
def insert(seq, p, x='*'):
    seq = list(seq)
    return tuple(seq[:p] + [x] + seq[p:])
def swap(seq, i):
    seq = list(seq)
    seq[i], seq[i+1] = seq[i+1], seq[i]
    return tuple(seq)
def is_subsequence(short, long):
    it = iter(long)
    try:
        for x in short:
            while next(it) != x:
                pass
        return True
    except StopIteration:
        return False
alphabet = tuple('ab')
summary = {k:0 for k in ['touch_direct_true','touch_direct_false','away_direct_true','away_direct_false','away_back_false']}
for n in range(0, 6):
    for S in product(alphabet, repeat=n):
        for p in range(n+1):
            B = insert(S, p)
            for i in range(n):
                touches = (i == p) or (i == p-1)
                L = swap(B, i)
                direct = is_subsequence(S, L)
                back = is_subsequence(S, swap(L, i))
                if touches:
                    summary['touch_direct_true' if direct else 'touch_direct_false'] += 1
                else:
                    summary['away_direct_true' if direct else 'away_direct_false'] += 1
                    if not back:
                        summary['away_back_false'] += 1
print(summary)

结果：
- touch_direct_false = 0
- away_back_false = 0

即：
- 只要交换碰到插入 token，S 直接就是 L 的子序列；
- 只要交换没碰到插入 token，同一位置再交换一次即可恢复原插入态。

含义

这给了一个比“看起来像对”的穷举结果更强的结构性理由：
当前判定之所以能覆盖无界长度，不是靠样本巧合，而是因为 insert + swap 的每个实例都能归入上述两类之一。

注意

这个结论仍然建立在抽象 token 模型上；它证明的是“序列层面的可达性充要性”，不是自然语言表层的全部语义。若要继续向真实文本推进，下一步应检查：
- 插入 token 是否必须是 fresh；
- 停用词/词形变化是否会破坏子序列保持性；
- 一次相邻交换是否需要被限制在 support-contained-window 中。