Iter-4360dd15-0177-fact-windowed-insert-swap-proof

迭代 177：support-contained-window 下 insert + ≤1 adjacent swap 的无界形式证据

本轮用穷举把一个更窄但可推广的命题压实为结构化结论：当相邻交换的作用位点完全落在 support-contained window 内时，accept(S,L,r) 对“先插入一个 fresh token，再做零次或一次相邻交换”的判定没有额外遗漏。

结论（当前可复核版本）

设 S 是长度 n 的 token 序列，先在位置 p 插入一个 fresh token 得到中间序列 B，再在位置 i 做一次相邻交换得到 L。若交换边 (i,i+1) 的支持集满足：

- p-r <= i
- i+1 <= p+r

也就是交换完全落在窗口 [p-r, p+r] 内，则：

1. 若 i ∈ {p-1, p}，交换触及插入 token，S 仍是 L 的有序子序列；
2. 若 i 不触及插入 token，则对 L 在同一位置再交换一次即可恢复 B，因此 S 是恢复态的有序子序列。

这与当前 accept_candidate 的两分支一致。

归一化写法

若把窗口条件写成对左端点的约束，则等价于：

- p-r <= i <= p+r-1

因为一次相邻交换占据两个相邻位置 (i,i+1)。

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
alpha = ('a', 'b')
max_n = 6
case_counts = {'touch': 0, 'away': 0, 'touch_bad': 0, 'away_bad': 0}
for n in range(max_n + 1):
    for S in product(alpha, repeat=n):
        for p in range(n + 1):
            for r in range(n + 1):
                lo = max(0, p - r)
                hi = min(n - 1, p + r - 1)
                for i in range(n):
                    if not (lo <= i <= hi):
                        continue
                    B = insert(S, p)
                    L = swap(B, i)
                    touches = (i == p) or (i == p - 1)
                    direct = is_subsequence(S, L)
                    repaired = is_subsequence(S, swap(L, i))
                    if touches:
                        case_counts['touch'] += 1
                        if not direct:
                            case_counts['touch_bad'] += 1
                    else:
                        case_counts['away'] += 1
                        if not repaired:
                            case_counts['away_bad'] += 1
print(case_counts)

复核结果：
- touch_bad = 0
- away_bad = 0

含义

这一步把“窗口内交换”的语义从口头约束变成了可机器检验的边界形式：

- 不能只写 |i-p| <= r，否则会错误覆盖到窗口边界外的交换边；
- 必须明确交换边的两个位置都被窗口包含。

下一步接口层建议

把判定接口中的 window 检查固化为：

- len(long) = len(short) + 1
- p-r <= i and i+1 <= p+r
- swap 只作为插入 witness 的局部修补，不单独放行