Executable affine rational quantization

For a positive rational scale s, zero point z, and integer code interval [qmin, qmax], this module executes nearest-even affine quantization:

quantize x   = clamp (roundEven (x / s) + z)
dequantize k = s * (k - z)

Exact rational parameters keep the scalar kernel executable and make its mathematical denotation independent of host floating-point behavior. Downstream tensor libraries can lift the scalar operation pointwise without introducing a second quantization semantics.

The equations follow the integer-arithmetic quantization scheme used by common neural-network runtimes. See Jacob et al., "Quantization and Training of Neural Networks for Efficient Integer-Arithmetic-Only Inference," CVPR 2018, doi:10.1109/CVPR.2018.00286.

structure FloatLib.Numerics.Quantization.AffineQuantizer : Type

Parameters of a bounded nearest-even affine quantizer.

• scale : ℚ

  Exact distance between adjacent reconstructed values.

• zeroPoint : ℤ

  Integer code representing zero when it lies in the code range.

• qmin : ℤ

  Smallest stored code.

• qmax : ℤ

  Largest stored code.

• scale_pos : 0 < self.scale

  A quantization scale is strictly positive.

• codeRange : self.qmin ≤ self.qmax

  The code interval is nonempty.

@[inline]

def FloatLib.Numerics.Quantization.AffineQuantizer.clampCode (q : AffineQuantizer) (code : ℤ) : ℤ

Saturate an integer to the quantizer's code interval, using the shared saturating clamp.

@[inline]

def FloatLib.Numerics.Quantization.AffineQuantizer.rawCode (q : AffineQuantizer) (x : ℚ) : ℤ

Integer code before saturation.

@[inline]

def FloatLib.Numerics.Quantization.AffineQuantizer.quantize (q : AffineQuantizer) (x : ℚ) : ℤ

Quantize an exact rational and saturate the result to the stored code interval.

@[inline]

def FloatLib.Numerics.Quantization.AffineQuantizer.dequantize (q : AffineQuantizer) (code : ℤ) : ℚ

Reconstruct the exact rational denoted by an integer code.

@[inline]

def FloatLib.Numerics.Quantization.AffineQuantizer.roundedValue (q : AffineQuantizer) (x : ℚ) : ℚ

Mathematical value produced by executable affine quantization.

theorem FloatLib.Numerics.Quantization.AffineQuantizer.clampCode_mem (q : AffineQuantizer) (code : ℤ) : q.qmin ≤ q.clampCode code ∧ q.clampCode code ≤ q.qmax

Saturation always returns a valid code.

@[simp]

theorem FloatLib.Numerics.Quantization.AffineQuantizer.clampCode_eq_self (q : AffineQuantizer) {code : ℤ} (hlo : q.qmin ≤ code) (hhi : code ≤ q.qmax) : q.clampCode code = code

Saturation fixes a code already inside the representable interval.

theorem FloatLib.Numerics.Quantization.AffineQuantizer.quantize_mem (q : AffineQuantizer) (x : ℚ) : q.qmin ≤ q.quantize x ∧ q.quantize x ≤ q.qmax

Every quantized scalar lies in the declared code interval.

@[simp]

theorem FloatLib.Numerics.Quantization.AffineQuantizer.dequantize_zeroPoint (q : AffineQuantizer) : q.dequantize q.zeroPoint = 0

Dequantizing the zero point gives exact zero.

@[simp]

theorem FloatLib.Numerics.Quantization.AffineQuantizer.quantize_dequantize (q : AffineQuantizer) {code : ℤ} (hlo : q.qmin ≤ code) (hhi : code ≤ q.qmax) : q.quantize (q.dequantize code) = code

Every in-range integer code survives an executable quantize/dequantize round trip.

theorem FloatLib.Numerics.Quantization.AffineQuantizer.dequantize_rawCode_error_le (q : AffineQuantizer) (x : ℚ) : |q.dequantize (q.rawCode x) - x| ≤ q.scale / 2

Before saturation, reconstruction differs from the input by at most half a quantization step.

theorem FloatLib.Numerics.Quantization.AffineQuantizer.dequantize_quantize_error_le (q : AffineQuantizer) (x : ℚ) (hlo : q.qmin ≤ q.rawCode x) (hhi : q.rawCode x ≤ q.qmax) : |q.roundedValue x - x| ≤ q.scale / 2

The half-step bound survives saturation whenever clipping is inactive.

General numerical-system view

@[reducible, inline]

abbrev FloatLib.Numerics.Quantization.AffineQuantizer.StoredCode (q : AffineQuantizer) : Set ℤ

An integer code in the quantizer's closed storage interval.

Using Mathlib's interval subtype keeps range reasoning interoperable and avoids a project-local proof-carrying record for the standard qmin ≤ value ≤ qmax invariant.

@[inline]

def FloatLib.Numerics.Quantization.AffineQuantizer.quantizeCode (q : AffineQuantizer) (x : ℚ) : ↑q.StoredCode

Store the executable quantization result together with its erased range proof.

def FloatLib.Numerics.Quantization.AffineQuantizer.numericalSystem (q : AffineQuantizer) : NumericalSystem

Numerical system whose codes denote their exact affine reconstruction.

@[reducible, inline]

abbrev FloatLib.Numerics.Quantization.AffineQuantizer.At (q : AffineQuantizer) (value : NumericalValue ℚ) : Type

An affine-quantized code with an erased proof of its complete denotation.

@[reducible, inline]

abbrev FloatLib.Numerics.Quantization.AffineQuantizer.AtFinite (q : AffineQuantizer) (value : ℚ) : Type

An affine-quantized code with an erased proof of its reconstructed rational value.

@[simp]

theorem FloatLib.Numerics.Quantization.AffineQuantizer.numericalSystem_represents_iff (q : AffineQuantizer) (code : ↑q.StoredCode) (x : ℚ) : q.numericalSystem.Represents code x ↔ q.dequantize ↑code = x

Representation in the affine system is equality with exact dequantization.

theorem FloatLib.Numerics.Quantization.AffineQuantizer.quantizeCode_quantizerOn_roundedValue (q : AffineQuantizer) : Operation.QuantizerOn q.numericalSystem q.quantizeCode q.roundedValue fun (x : q.numericalSystem.Scalar) => True

Executable quantization is a quantizer onto its own reconstructed value.

Since roundedValue is dequantize after quantize, this is the definitional contract used by generic QuantizerOn automation. The error bound when clipping is inactive is dequantize_quantize_error_le.

theorem FloatLib.Numerics.Quantization.AffineQuantizer.numericalSystem_quantize_error_le (q : AffineQuantizer) (x : ℚ) (hlo : q.qmin ≤ q.rawCode x) (hhi : q.rawCode x ≤ q.qmax) : ∃ (reconstructed : ℚ), q.numericalSystem.Represents (q.quantizeCode x) reconstructed ∧ |reconstructed - x| ≤ q.scale / 2

The numerical-system view inherits the inactive-saturation half-step guarantee.