BugZoo: tokenizer/import boundary

Tokenization usually happens outside the tensor graph, which makes it easy for a model import to silently disagree about vocabulary size, padding, EOS, or special-token IDs. LLM inference-engine bug studies include tokenizer/config mismatch classes among real production failures:

https://arxiv.org/abs/2506.09713

TorchLean's current contract is focused: once tokens enter the verified fragment, token IDs can be represented as Fin vocabularySize, making out-of-vocabulary IDs unrepresentable. Bounds alone do not establish that two tokenizers assign the same token to the same ID, or that padding and end-of-sequence metadata matches the model. Importers must check those agreements.

structure NN.Examples.BugZoo.TokenizerBoundary.Metadata : Type

The tokenizer metadata that must agree with the model's embedding table.

• vocabularySize : ℕ
• paddingTokenId : Fin self.vocabularySize
• endOfSequenceTokenId : Fin self.vocabularySize

theorem NN.Examples.BugZoo.TokenizerBoundary.padding_lt_vocabulary (contract : Metadata) : ↑contract.paddingTokenId < contract.vocabularySize

The padding token is in range by construction.

theorem NN.Examples.BugZoo.TokenizerBoundary.token_lt_vocabulary {vocabularySize sequenceLength : ℕ} (sequence : TorchLean.Tensor (Fin vocabularySize) [sequenceLength]) (position : Fin sequenceLength) : ↑sequence[position] < vocabularySize

Every imported token ID is in range by construction.