Rounding modes and a half-ULP error bound

We use this file as the “rounding” half of the Flocq-style rounding-on-ℝ model:

• rounding modes rnd : ℝ → ℤ (floor/ceil/trunc/nearest-even),
• the validity typeclasses NeuralValidRnd and NeuralValidRndToNearest,
• the core rounding operator neural_round,
• the standard bound abs(neural_round … x - x) ≤ ulp(x)/2 for round-to-nearest.

These definitions are used by NF (the rounded scalar type), by the FP32 model, and by the bridge layer that connects proofs to executable IEEE-754 behavior.

References

• IEEE Std 754-2019, "IEEE Standard for Floating-Point Arithmetic".
• D. Goldberg, "What Every Computer Scientist Should Know About Floating-Point Arithmetic", ACM Computing Surveys, 1991.
• N. J. Higham, "Accuracy and Stability of Numerical Algorithms", SIAM, 2nd ed., 2002.
• The Flocq Coq library is a classic example of axiomatizing "rounding on R"; TorchLean's NeuralFloat layer is inspired by that style (but is implemented natively in Lean).

noncomputable def TorchLean.Floats.neuralFloorRound : ℝ → ℤ

Round toward negative infinity (floor)

noncomputable def TorchLean.Floats.neuralCeilRound : ℝ → ℤ

Round toward positive infinity (ceiling)

noncomputable def TorchLean.Floats.neuralTruncRound : ℝ → ℤ

Round toward zero (truncation)

noncomputable def TorchLean.Floats.neuralNearestEven : ℝ → ℤ

Round to nearest, ties to even

class TorchLean.Floats.NeuralValidRnd (rnd : ℝ → ℤ) : Prop

Valid rounding mode predicate.

• monotone (x y : ℝ) : x ≤ y → rnd x ≤ rnd y
• id (n : ℤ) : rnd ↑n = n

class TorchLean.Floats.NeuralValidRndToNearest (rnd : ℝ → ℤ) extends TorchLean.Floats.NeuralValidRnd rnd : Prop

Rounding modes with a half-unit error bound on the rounded integer.

This matches "round-to-nearest" style roundings (ties can be resolved arbitrarily): |rnd x - x| ≤ 1/2 for all x.

• monotone (x y : ℝ) : x ≤ y → rnd x ≤ rnd y
• id (n : ℤ) : rnd ↑n = n
• abs_sub_le_half (x : ℝ) : |↑(rnd x) - x| ≤ 2⁻¹

instance TorchLean.Floats.instNeuralValidRndNeuralFloorRound : NeuralValidRnd neuralFloorRound

neural_floor_round is a valid rounding mode (monotone and fixes integers).

instance TorchLean.Floats.instNeuralValidRndNeuralCeilRound : NeuralValidRnd neuralCeilRound

neural_ceil_round is a valid rounding mode (monotone and fixes integers).

theorem TorchLean.Floats.neural_nearest_even_bounds (x : ℝ) : ⌊x⌋ ≤ neuralNearestEven x ∧ neuralNearestEven x ≤ ⌊x⌋ + 1

Basic bounds for nearest-even rounding.

In words: neural_nearest_even x always lands in {⌊x⌋, ⌊x⌋ + 1}. This is the key fact used in the monotonicity proof and in IEEE-style interval bounds.

theorem TorchLean.Floats.neural_nearest_even_eq_floor_of_frac_lt_half (x : ℝ) (h : x - ↑⌊x⌋ < 1 / 2) : neuralNearestEven x = ⌊x⌋

Nearest-even rounds down when the fractional part is strictly less than 1/2.

In words: if x is closer to ⌊x⌋ than to ⌊x⌋+1, then it rounds to ⌊x⌋.

theorem TorchLean.Floats.neural_nearest_even_eq_ceil_of_frac_gt_half (x : ℝ) (h : x - ↑⌊x⌋ > 1 / 2) : neuralNearestEven x = ⌊x⌋ + 1

Nearest-even rounds up when the fractional part is strictly greater than 1/2.

In words: if x is closer to ⌊x⌋+1 than to ⌊x⌋, then it rounds to ⌊x⌋+1.

theorem TorchLean.Floats.neural_nearest_even_eq_floor_of_frac_half_even (x : ℝ) (h1 : x - ↑⌊x⌋ = 1 / 2) (h2 : Even ⌊x⌋) : neuralNearestEven x = ⌊x⌋

Nearest-even tie-breaking: when the fractional part is exactly 1/2 and the floor is even, round down to the even integer.

theorem TorchLean.Floats.neural_nearest_even_eq_ceil_of_frac_half_odd (x : ℝ) (h1 : x - ↑⌊x⌋ = 1 / 2) (h2 : ¬Even ⌊x⌋) : neuralNearestEven x = ⌊x⌋ + 1

Nearest-even tie-breaking: when the fractional part is exactly 1/2 and the floor is odd, round up to the even integer.

instance TorchLean.Floats.instNeuralValidRndNeuralNearestEven : NeuralValidRnd neuralNearestEven

neural_nearest_even is a valid rounding mode (monotone and fixes integers).

theorem TorchLean.Floats.neural_nearest_even_abs_sub_le_half (x : ℝ) : |↑(neuralNearestEven x) - x| ≤ 2⁻¹

Nearest-even is a “round-to-nearest” mode in the integer sense: |rnd(x) - x| ≤ 1/2.

This is the key property required by NeuralValidRndToNearest.

instance TorchLean.Floats.instNeuralValidRndToNearestNeuralNearestEven : NeuralValidRndToNearest neuralNearestEven

neural_nearest_even satisfies the half-unit error bound |rnd x - x| ≤ 1/2.

noncomputable def TorchLean.Floats.neuralRound {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) (x : ℝ) : ℝ

Core rounding operator (“compute in ℝ, then round back to the grid”).

We build a NeuralFloat record and then interpret it via neural_to_real. Only mantissa/exponent affect the value; the metadata fields are set to conventional defaults.

@[simp]

theorem TorchLean.Floats.neural_round_preserves_generic {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) (hx : neuralGenericFormat β fexp x) : neuralRound rnd x = x

Rounding preserves exactly-representable numbers.

In words: if x lies on the grid described by (β,fexp) (neural_generic_format), then rounding it with any valid rnd is a no-op.

This is the Flocq-style “round_generic” lemma.

theorem TorchLean.Floats.neural_scaled_mantissa_mul_bpow {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) : neuralScaledMantissa β fexp x * neuralBpow β (neuralCexp β fexp x) = x

Scaled mantissa times base power equals the original value.

In words: scaled_mantissa(x) * β^{cexp(x)} = x. This is the algebraic identity that justifies the scaling used before rounding.

theorem TorchLean.Floats.neural_error_bound_ulp {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRndToNearest rnd] (x : ℝ) : |neuralRound rnd x - x| ≤ neuralUlp β fexp x / 2

Half-ULP error bound for neural_round under round-to-nearest.

This is the basic “one-step” bound used by most error propagation arguments: neural_round deviates from x by at most half an ulp at the chosen exponent scale.