A certified split point lets a parallel lexer cut unlexed input at a single byte with the serial token stream provably preserved, but several conventional token sets in the predecessor's controlled study certify no byte once string, comment, or whitespace-run forms are included (arXiv:2608.03473v2). We generalize from a byte to a bounded window, a byte string after which the position where the current token began is known, regardless of surrounding context. We certify the directly usable form of that recovery, namely that the token covering the window's final byte begins at the reported origin. The certificate is conditional on occurrence and may be vacuous; every applicability figure counts only windows carrying an asserted completely tokenizable occurrence witness. We give a conservative model of a maximal-munch scanner's possible histories across a window, prove it sound, and decide reachability in that model exactly by exhausting a finite quotient of its reachable configurations. Within the flat, completely tokenizable scope, model-positive answers are semantic certificates; negatives are relative to the model, which deliberately refuses some windows a greedy scanner would allow. Whether the model certifies any window, plain or witnessed, is PSPACE-complete, and a shortest window can need $2^{Ω(\sqrt{n})}$ bytes over n live states. Two smaller searches decide plain model existence, the second shipped in release 2.2.0 of munch. In a sample of 400 random token sets, 322 of the 337 sets certifying no byte gain a witnessed window, with zero inconclusive searches, and every exact-empty row of the predecessor's study gains a witnessed window of two to four bytes. The analysis runs once after automaton construction, using only the compiled tables and no input. A boundary profile marks each gap of a window forced, crossed or open, and a window-local cut is sound exactly at forced gaps.

翻译：暂无翻译