The Observation Theory EncyclopediaFrom TSKAboutBy kindBy chapterBy Lean fileLedgerProvenance

token concept

DefinitionA piece of text, roughly a word, the unit a language model reads and writes. Chapter 0 section 0.11.
ExampleThe word unbelievable may be three tokens, un, believ, and able.
BookData Mining as Observation, draft 0.2, commit f3914f0; entry id token, kind concept.
Statusno ledger row names this entry. Corrections: none recorded.
Defining equation

Book equation 0.22.

Assumptions and scope
  • A piece of text, roughly a word, the unit a language model reads and writes. A model reads a sequence of tokens and outputs a probability for the next one, and perplexity is two to the power of the average bits per token, so it is at least one and equals the vocabulary size for a uniform guess.
  • The key-value cache stores one key and one value per token per head, and a generation of 512 tokens under a wrong codebook was where the retracted degradation curve was measured. Token counts are the budget in every serving row of chapter 13.
Prior artnone recorded
Evidencelean/DataMiningAsObservation/Perplexity.lean
Reviewednot yet reviewed; generated 2026-09-10 from records at the commits on the provenance page.
thereaderdoesnotseethis.two tokens for one word
A piece of text, roughly a word, the unit a language model reads.

Equation

Book equation 0.22.

\[\mathrm{PPL}=2^{H},\qquad H=-\frac1T\sum_{t=1}^{T}\log_2 p\big(w_t\mid w_{<t}\big).\]

Book equation 0.23.

\[\operatorname{softmax}(z)_i=\frac{e^{z_i}}{\sum_j e^{z_j}},\qquad \text{output}=\sum_i\operatorname{softmax}\!\Big(\frac{q\cdot k_i}{\sqrt{d}}\Big)_{\!i}\,v_i.\]

Conditions

Conditions are curated in entries.toml rather than read from a record.

Ledger

none

First stated

Chapter 0 section 0.11 of Data Mining as Observation, with the program’s serving measurements in geometric-observation/experiments/GO-kv-serving-flip-NOTES.md.

Measurements

none

Failures and corrections

none

Invariance envelope

none declared

Machine checked

lean/DataMiningAsObservation/Perplexity.lean, theorems bits_nonneg, one_le_perplexity, perplexity_uniform, perplexity_mono, bits_of_finding, at observation-data-mining f3914f0; what the check covers is stated in the book’s appendix C.

Used in

Data Mining as Observation primer S, chapters 0, 4, 8, 11, 12, 13.

Related

perplexity; attention; KV cache; rotary position embedding; teacher forcing.

See also

Book equations stated beside the entry’s terms, not defining it: 11.1.

Sources-table rows that share a record with the entry without naming it: chapter 13 section 13.6.

Status

Generated 2026-09-10 by encyclopedia/generate.py; book at observation-data-mining f3914f0; the commit of every record is listed in the encyclopedia’s provenance.

← thresholdtrace →