Executable affine quantization and real rounding

The rational nearest-even kernel and the real nearest-even specification choose exactly the same integer, including negative inputs and half-way ties. Consequently, executable affine quantization agrees with real affine quantization before and after saturation, and exact reconstruction commutes with the rational-to-real embedding.

The rounding-independent API lives in Numerics.Quantization.Affine.Real. This module also specializes its order, round-trip, and error theorems to the existing Flocq rounding contracts.

theorem FloatLib.Floats.Formats.Flocq.nearestEven_ratCast (x : ℚ) : nearestEven ↑x = Numerics.roundRatEven x

Rational nearest-even execution agrees exactly with real nearest-even rounding.

theorem FloatLib.Floats.Formats.Flocq.affine_quantize_monotone (q : Numerics.Quantization.RealAffineQuantizer) (rnd : ℝ → ℤ) [ValidRnd rnd] : Monotone (q.quantize rnd)

A Flocq-valid integer rounder gives monotone affine quantization.

theorem FloatLib.Floats.Formats.Flocq.affine_quantize_dequantize (q : Numerics.Quantization.RealAffineQuantizer) (rnd : ℝ → ℤ) [ValidRnd rnd] {code : ℤ} (hlo : q.qmin ≤ code) (hhi : code ≤ q.qmax) : q.quantize rnd (q.dequantize code) = code

Any Flocq-valid rounder preserves in-range stored codes under reconstruction and rounding.

theorem FloatLib.Floats.Formats.Flocq.affine_dequantize_quantize_error_le_half (q : Numerics.Quantization.RealAffineQuantizer) (rnd : ℝ → ℤ) [ValidRndToNearest rnd] (x : ℝ) (hlo : q.qmin ≤ q.rawCode rnd x) (hhi : q.rawCode rnd x ≤ q.qmax) : |q.roundedValue rnd x - x| ≤ q.scale / 2

Without saturation, every valid nearest rounder reconstructs within half a grid step.

theorem FloatLib.Floats.Formats.Flocq.affine_toReal_quantize (q : Numerics.Quantization.AffineQuantizer) (x : ℚ) : q.toReal.quantize nearestEven ↑x = q.quantize x

Saturated rational execution and real nearest-even affine quantization return the same code.

theorem FloatLib.Floats.Formats.Flocq.affine_toReal_roundedValue (q : Numerics.Quantization.AffineQuantizer) (x : ℚ) : q.toReal.roundedValue nearestEven ↑x = ↑(q.roundedValue x)

Exact reconstruction agrees after the complete nearest-even quantization operation.