Affine quantization over the reals

RealAffineQuantizer describes a positive-scale integer grid with bounded storage. Its rounding function is supplied by the caller: order preservation, integer round trips, and error bounds each require only the corresponding property of that function. In particular, the error result is not restricted to nearest-even rounding.

AffineQuantizer.toReal embeds the executable rational quantizer's parameters without changing the code interval. toReal_quantize and toReal_roundedValue transport any agreement between rational and real integer rounding to the complete saturated operation. The Flocq rounding adapter specializes this agreement to nearest-even; executable clients can continue importing Affine alone without loading real-number theory.

structure FloatLib.Numerics.Quantization.RealAffineQuantizer : Type

A bounded affine grid with real-valued spacing and caller-supplied integer rounding.

• scale : ℝ

  Distance between adjacent reconstructed values.

• zeroPoint : ℤ

  Integer code whose reconstruction is zero. It need not be inside the storage interval.

• qmin : ℤ

  Smallest stored code.

• qmax : ℤ

  Largest stored code.

• scale_pos : 0 < self.scale

  The grid spacing is strictly positive.

• codeRange : self.qmin ≤ self.qmax

  The storage interval is nonempty.

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

Saturate an integer to the storage interval using the shared clamp.

noncomputable def FloatLib.Numerics.Quantization.RealAffineQuantizer.rawCode (q : RealAffineQuantizer) (rnd : ℝ → ℤ) (x : ℝ) : ℤ

Integer code before saturation.

noncomputable def FloatLib.Numerics.Quantization.RealAffineQuantizer.quantize (q : RealAffineQuantizer) (rnd : ℝ → ℤ) (x : ℝ) : ℤ

Round onto the affine grid and saturate to the storage interval.

noncomputable def FloatLib.Numerics.Quantization.RealAffineQuantizer.dequantize (q : RealAffineQuantizer) (code : ℤ) : ℝ

Reconstruct the real value denoted by an integer code.

noncomputable def FloatLib.Numerics.Quantization.RealAffineQuantizer.roundedValue (q : RealAffineQuantizer) (rnd : ℝ → ℤ) (x : ℝ) : ℝ

Reconstructed value after rounding and saturation.

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

Saturation always produces a code in the declared interval.

@[simp]

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

Saturation fixes every code already in the storage interval.

theorem FloatLib.Numerics.Quantization.RealAffineQuantizer.quantize_mem (q : RealAffineQuantizer) (rnd : ℝ → ℤ) (x : ℝ) : q.qmin ≤ q.quantize rnd x ∧ q.quantize rnd x ≤ q.qmax

Every quantized value lies in the storage interval, independently of the rounding rule.

@[simp]

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

The zero point reconstructs to zero, even if it lies outside the storage interval.

theorem FloatLib.Numerics.Quantization.RealAffineQuantizer.quantize_monotone (q : RealAffineQuantizer) {rnd : ℝ → ℤ} (hmono : Monotone rnd) : Monotone (q.quantize rnd)

A monotone integer rounder gives monotone saturated quantization.

theorem FloatLib.Numerics.Quantization.RealAffineQuantizer.dequantize_strictMono (q : RealAffineQuantizer) : StrictMono q.dequantize

Reconstruction preserves integer-code order because the scale is positive.

@[simp]

theorem FloatLib.Numerics.Quantization.RealAffineQuantizer.quantize_dequantize (q : RealAffineQuantizer) {rnd : ℝ → ℤ} (hfix : ∀ (n : ℤ), rnd ↑n = n) {code : ℤ} (hlo : q.qmin ≤ code) (hhi : code ≤ q.qmax) : q.quantize rnd (q.dequantize code) = code

A rounder that fixes integers preserves in-range codes under reconstruction and rounding.

theorem FloatLib.Numerics.Quantization.RealAffineQuantizer.dequantize_rawCode_error_le (q : RealAffineQuantizer) (rnd : ℝ → ℤ) (x ε : ℝ) (hround : |↑(rnd (x / q.scale)) - x / q.scale| ≤ ε) : |q.dequantize (q.rawCode rnd x) - x| ≤ q.scale * ε

An integer-rounding error bound scales by the spacing of the affine grid.

theorem FloatLib.Numerics.Quantization.RealAffineQuantizer.dequantize_quantize_error_le (q : RealAffineQuantizer) (rnd : ℝ → ℤ) (x ε : ℝ) (hround : |↑(rnd (x / q.scale)) - x / q.scale| ≤ ε) (hlo : q.qmin ≤ q.rawCode rnd x) (hhi : q.rawCode rnd x ≤ q.qmax) : |q.roundedValue rnd x - x| ≤ q.scale * ε

Without clipping, an integer-rounding error bound scales by the grid spacing.

theorem FloatLib.Numerics.Quantization.RealAffineQuantizer.dequantize_quantize_error_le_half (q : RealAffineQuantizer) (rnd : ℝ → ℤ) (x : ℝ) (hround : |↑(rnd (x / q.scale)) - x / q.scale| ≤ 1 / 2) (hlo : q.qmin ≤ q.rawCode rnd x) (hhi : q.rawCode rnd x ≤ q.qmax) : |q.roundedValue rnd x - x| ≤ q.scale / 2

Without clipping, nearest integer rounding reconstructs within half a grid step.

noncomputable def FloatLib.Numerics.Quantization.AffineQuantizer.toReal (q : AffineQuantizer) : RealAffineQuantizer

View an executable rational grid as a real grid with the same integer codes.

@[simp]

theorem FloatLib.Numerics.Quantization.AffineQuantizer.toReal_dequantize (q : AffineQuantizer) (code : ℤ) : q.toReal.dequantize code = ↑(q.dequantize code)

Reconstruction commutes with the exact rational-to-real embedding.

theorem FloatLib.Numerics.Quantization.AffineQuantizer.toReal_quantize (q : AffineQuantizer) (rnd : ℝ → ℤ) (hround : ∀ (x : ℚ), rnd ↑x = roundRatEven x) (x : ℚ) : q.toReal.quantize rnd ↑x = q.quantize x

Agreement of integer rounding lifts to affine quantization, including saturation.

theorem FloatLib.Numerics.Quantization.AffineQuantizer.toReal_roundedValue (q : AffineQuantizer) (rnd : ℝ → ℤ) (hround : ∀ (x : ℚ), rnd ↑x = roundRatEven x) (x : ℚ) : q.toReal.roundedValue rnd ↑x = ↑(q.roundedValue x)

Reconstruction commutes with exact embedding whenever integer rounding does.