Nearest-codeword quantization for finite codebooks

A codebook is a finite table, so the natural quantizer is exhaustive: scan every word, keep the finite entries, and select one whose denotation is closest to the target. This module provides that quantizer, nearestCode, together with the theorem that its result minimizes the distance |x - c| over all finite codewords c.

The tie policy is fixed and simple: the scan runs in ascending order of the unsigned word value, and a candidate replaces the current best only when it is strictly closer. A tie therefore resolves to the lower word. Applications that need a different tie rule, or a rule for reserved words, can still define their own quantizer against the same table.

The scalar type only needs subtraction, negation, and a linear order so that |x - c| is defined and comparable. No ordered-group axioms are used by the minimality proof.

def FloatLib.Floats.Formats.Codebook.finiteEntries {width : ℕ} {α : Type u} (book : Codebook width α) : List (book.Code × α)

All codewords with a finite denotation, paired with that denotation, in ascending order of the unsigned word value. Exceptional words are omitted.

theorem FloatLib.Floats.Formats.Codebook.mem_finiteEntries_iff {width : ℕ} {α : Type u} (book : Codebook width α) (code : book.Code) (value : α) : (code, value) ∈ book.finiteEntries ↔ book.denote code = Numerics.NumericalValue.finite value

A word appears in finiteEntries with a value exactly when the table decodes it to that value.

def FloatLib.Floats.Formats.Codebook.closerEntry {width : ℕ} {α : Type u} [AddGroup α] [LinearOrder α] {book : Codebook width α} (x : α) (best : Option (book.Code × α)) (entry : book.Code × α) : Option (book.Code × α)

Keep the current best entry unless the candidate is strictly closer to x.

def FloatLib.Floats.Formats.Codebook.nearestCode {width : ℕ} {α : Type u} [AddGroup α] [LinearOrder α] (book : Codebook width α) (x : α) : Option book.Code

The first finite codeword whose denotation minimizes |x - c|, scanning words in ascending unsigned order and replacing the current best only on a strict improvement. Ties resolve to the lower word. The result is none exactly when the table has no finite entry.

theorem FloatLib.Floats.Formats.Codebook.foldl_closerEntry_isSome {width : ℕ} {α : Type u} [AddGroup α] [LinearOrder α] {book : Codebook width α} (x : α) (entries : List (book.Code × α)) (start : book.Code × α) : ∃ (result : book.Code × α), List.foldl (closerEntry x) (some start) entries = some result

Folding closerEntry from a present accumulator always yields a present result.

theorem FloatLib.Floats.Formats.Codebook.foldl_closerEntry_spec {width : ℕ} {α : Type u} [AddGroup α] [LinearOrder α] {book : Codebook width α} (x : α) (entries : List (book.Code × α)) (acc : Option (book.Code × α)) (selected : book.Code × α) (hfold : List.foldl (closerEntry x) acc entries = some selected) : (selected ∈ entries ∨ acc = some selected) ∧ (∀ entry ∈ entries, |x - selected.2| ≤ |x - entry.2|) ∧ ∀ (current : book.Code × α), acc = some current → |x - selected.2| ≤ |x - current.2|

The fold invariant behind nearestCode: a selected entry comes from the scanned list or the initial accumulator, and it is at least as close to x as every scanned entry and as the initial accumulator.

theorem FloatLib.Floats.Formats.Codebook.nearestCode_spec {width : ℕ} {α : Type u} [AddGroup α] [LinearOrder α] (book : Codebook width α) (x : α) (code : book.Code) (hnearest : book.nearestCode x = some code) : ∃ (value : α), book.denote code = Numerics.NumericalValue.finite value ∧ ∀ (other : BitVec width) (otherValue : α), book.denote other = Numerics.NumericalValue.finite otherValue → |x - value| ≤ |x - otherValue|

The selected codeword is finite and its denotation is at least as close to x as the denotation of every finite codeword in the table.

theorem FloatLib.Floats.Formats.Codebook.nearestCode_isSome_of_denote_finite {width : ℕ} {α : Type u} [AddGroup α] [LinearOrder α] (book : Codebook width α) (x : α) {code : book.Code} {value : α} (hfinite : book.denote code = Numerics.NumericalValue.finite value) : ∃ (nearest : book.Code), book.nearestCode x = some nearest

A table with at least one finite word always has a nearest codeword.