Iter-4360dd15-0186-fact-left-prefix-consumption-cut

迭代 186：固定 μ 锚点后，左侧可独立抽离的真正判定量是“左块最大前缀匹配长度”

本轮把 L = X · μ · Y 的可行性判定再压窄一层，得到一个比“左右独立分解”更准确的接口：

对任何不含 μ 的串 S，先只看左块 X，定义

k = max { t | S[:t] ⪯ X }

则有：

S ⪯ X · μ · Y 当且仅当 S[k:] ⪯ μ · Y

也就是说：
- 左侧信息只通过一个整数 k 传递；
- k 完全由 X 决定，不依赖右侧 Y；
- 右侧只负责验证剩余后缀是否能落在 μ · Y 中。

这比“左右完全独立”更强也更安全

此前已经证伪了把 X 和 Y 当成两个独立可判定块的过强分解；
现在确认的正确结构是：

1. 左块先贪心吞掉 S 的最长可匹配前缀；
2. 分界点由 X 决定；
3. 右块只检查剩余部分。

所以，μ 锚定后的局部证明应当围绕“前缀消耗量 k”展开，而不是围绕“固定切分点”。

机器复核代码

from itertools import product
def is_subsequence(short, long):
    it = iter(long)
    try:
        for x in short:
            while next(it) != x:
                pass
        return True
    except StopIteration:
        return False
def max_prefix_match(short, long):
    it = iter(long)
    k = 0
    try:
        for x in short:
            while next(it) != x:
                pass
            k += 1
        return k
    except StopIteration:
        return k
alpha = ('a','b')
mu = 'μ'
for nx in range(0,6):
    for ny in range(0,6):
        for X in product(alpha, repeat=nx):
            for Y in product(alpha, repeat=ny):
                T = X + (mu,) + Y
                for ns in range(0, nx+ny+2):
                    for S in product(alpha, repeat=ns):
                        k = max_prefix_match(S, X)
                        assert is_subsequence(S, T) == is_subsequence(S[k:], (mu,) + Y)
print('ok')

可复用结论

后续若要证明“左侧一次相邻交换可独立抽离”，最合适的路线不是试图把 X/Y 拆成两个完全自治命题，而是：
- 先在 X 上算出对 S 的最大消耗 k；
- 再把一次交换的影响限制在 S[:k] 对应的左块 witness 内；
- 最后只把剩余后缀交给 μ·Y。

这应该是下一步最窄、最稳的局部化接口。