Type-Driven Tokenization Fixes Brahmic Script Orthography Violations

Standard tokenizers produce malformed text in Brahmic abugida scripts by treating them as semigroups. Using Agda to model valid tokens as transition system chains, the authors derive a fixToken function that enforces orthographic boundaries and provides a patch for SentencePiece.