The Observation Theory EncyclopediaFrom TSKAboutBy kindBy chapterBy Lean fileLedgerProvenance

quantization concept

DefinitionReplacing each number with one of a small set of allowed values so that it can be stored in a few bits. Chapter 0 section 0.11. Also quantiz.
ExampleRounding 1.37 to a step of 0.5 gives 1.5, an error of 0.13.
BookData Mining as Observation, draft 0.2, commit f3914f0; entry id quantization, kind concept.
Statusno ledger row names this entry. Corrections: none recorded.
Defining equation

Book equation 11.1.

Assumptions and scope
  • Replacing each number with one of a small set of allowed values so that it can be stored in a few bits. A uniform quantizer with a given step has error at most half the step and zero error on a level, and halving the step halves the bound.
  • Those are the identity reader’s bounds. What a quantizer does to a consumer is the flip’s question, and the key quantizer table of chapter 11 is the case in which the smaller reconstruction error was the worse code.
Prior artnone recorded
Evidencelean/DataMiningAsObservation/Quantization.lean
Reviewednot yet reviewed; generated 2026-09-10 from records at the commits on the provenance page.
1 bit, 2 levels2 bits, 4 levels3 bits, 8 levels4 bits, 16 levels
Replacing each number with one of a small set of values.

Equation

Book equation 11.1.

\[\cos\big(k,\hat k\big)=0.995\qquad\text{while}\qquad \mathrm{PPL}:\ 12.24\ \to\ 10643.\]

Conditions

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

Ledger

none

First stated

Chapter 0 section 0.11 and chapter 11 section 11.2 of Data Mining as Observation, with the program’s quantizer table in turboquant-pro/docs/KV_KEYS_FINDING.md:1-49.

Measurements

none

Failures and corrections

none

Invariance envelope

none declared

Machine checked

lean/DataMiningAsObservation/Quantization.lean, theorems error_le_half_step, quantize_level, half_step_bound, sq_error_le, finer_step, at observation-data-mining f3914f0; what the check covers is stated in the book’s appendix C.

Used in

Data Mining as Observation chapters 0, 2, 3, 4, 7, 8, 10, 11.

Related

bit; codebook; per-channel quantizer; direction-only quantizer; the flip.

See also

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

Ledger rows that cite the entry’s records without naming it: GO-2 (neg. half: not reconstruction), NEG-2.

Sources-table rows that share a record with the entry without naming it: chapter 1 section 1.4, chapter 2 section 2.5, chapter 3 section 3.2, chapter 8 section 8.2, chapter 8 section 8.9, chapter 11 section 11.1, chapter 11 section 11.2.

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.

← quadratic formquery, key, value →