Classical panic-mode recovery skips a failed scan forward by convention, promising progress but no repair-universal boundary guarantee for where it lands. We choose the resume position by theorem, via a committed-prefix lemma over certificates posted for parallel lexing (arXiv:2608.03473, arXiv:2608.09761): a position is a sound recovery point when every prefix repair whose scan commits through the certificate's returned evidence places a token boundary there. This quantifier is strictly stronger than its complete-repair special case, and at a sound recovery point the inclusion is strict precisely when no repair completes while some scan commits through the evidence. The evidence-returning interface pairs each answer with the interval it rests on, so a caller who knows what the scanner cannot check decides whether the boundary transfers to the intended input. The search provably terminates; the guarantee is relative to the active mode's automaton. For an automaton of n states the quantifier is decided exactly from the preserved tail by at most n + 1 representative repairs, and a shortest reaching repair has at most n - 1 symbols and a shortest counterrepair at most n, both tight. Every anchor of an m-byte input is profiled in $O(nm + n|Σ|)$ time. The shipped repair routines are the complete-repair case, which proves their contracts. In a deterministic corruption study of munch's procedure beside skip-one and delimiter recovery, every certified answer whose evidence survives the damage passes its landing check on every move, 40,885 of 40,885, while the 5,595 first answers resting on evidence the damage reached land 1,589 times, reported, not asserted. Of the 16,808 trials labeled beyond repair, 13,522 resume on a suffix that tokenizes whole, where both quantifiers are provably empty, and 3,286 stay undetermined, their damaged inputs not archived.
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.
Table-driven DFA lexing is sequential, since each transition depends on the previous byte's state. Scanning one input in parallel needs each chunk's entry state, which existing methods recover by simulation, speculation, prescanning, or overlap. We give two conditions under which none is needed. For a longest-match scanner restarting from q0 at every token boundary, a byte b is a certified split symbol when no reachable state other than q0 has a b-transition whose target can reach acceptance, and q0 is not re-entrant if it has one. Every occurrence of such a byte in completely tokenizable input begins a token, so chunks starting there reproduce the serial sequence of kinds and lengths. The condition is necessary and sufficient, but one string, comment, or whitespace run can remove every useful certificate. Comments and whitespace are usually discarded, so we weaken the guarantee to equality after deleting a declared discarded set and give a second condition, a precomputed constant-time one-bit test. It is sound but incomplete and more permissive, strictly so on suitable token sets and discarded sets. It recovers newline for a conventional C-like tokenization and tab, newline and carriage return for JSON, and refuses newline where block comments are unrestricted. Safety modulo the discarded set is decidable in PSPACE for every token automaton and in polynomial time for literal vocabularies, and every unsafe byte has a replayable counterexample. On the fifteen token sets studied the second condition is already exact. Splitting at exact certificates in munch reaches 92.6-95.3% parallel efficiency at eight threads on a restricted CPU set and a 512 MiB corpus, and a 3.46-3.94x end-to-end speedup at four threads, on one machine. It turns delimiter-based parallel lexing from a language-specific assumption into a property a compiler checks.