Provably Lossless Reversible Transliteration: A Formal Specification and an Exhaustive-Verification Methodology

Reversible, deterministic, lossless transliteration is a named open problem in multilingual NLP, where back-transliteration of model output is a recognized lossy bottleneck. Reversible transliteration itself is old (ISO 9, the Buckwalter scheme, ICU reversible transforms, invertible finite-state transducers, NOOR-TR); what is missing is a script-agnostic formal specification carrying machine-checkable obligations at full Unicode breadth, with an explicit record of which obligations are proven and which are only tested. This note specifies reversible transliteration as seven properties (R1 to R7) with a stated dependency structure, and gives a verification methodology that tags each obligation as proof by exhaustion over finite Unicode domains, structural proof, or property testing. The formal core is classical coding theory (a uniquely decodable code induces an injective homomorphism with a left inverse; McMillan; Sardinas and Patterson), which we instantiate. The construction that makes the code total over all of Unicode is an elementary escaping scheme, for which we give explicit sufficient conditions (Lemma 2). The contribution is the specification and the tagged-assurance methodology; context-dependent and greedy disambiguation stay open, and no new coding result is claimed. The note does not claim first existence of reversible transliteration, nor that any shipping implementation is reversible. Companion to the XMR metric note (doi:10.5281/zenodo.19323513).