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).

source

noncomputable def TorchLean.Floats.neuralFloorRound :

ℝ → ℤ

Round toward negative infinity (floor)

Instances For

source

noncomputable def TorchLean.Floats.neuralCeilRound :

ℝ → ℤ

Round toward positive infinity (ceiling)

Instances For

source

noncomputable def TorchLean.Floats.neuralTruncRound :

ℝ → ℤ

Round toward zero (truncation)

Instances For

source

theorem TorchLean.Floats.neuralTruncRound_eq_floor {x : ℝ} (hx : 0 ≤ x) :

neuralTruncRound x = neuralFloorRound x

Toward-zero integer rounding agrees with floor on nonnegative inputs.

source

theorem TorchLean.Floats.neuralTruncRound_eq_ceil {x : ℝ} (hx : x ≤ 0) :

neuralTruncRound x = neuralCeilRound x

Toward-zero integer rounding agrees with ceiling on nonpositive inputs.

source

noncomputable def TorchLean.Floats.neuralNearestEven :

ℝ → ℤ

Round to nearest, ties to even

Instances For

source

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

Prop

Valid rounding mode predicate.

monotone (x y : ℝ) : x ≤ y → rnd x ≤ rnd y
The rounding rule preserves the order of its real inputs.
id (n : ℤ) : rnd ↑n = n
Every integer is fixed by the rounding rule.

Instances

source

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⁻¹
Rounding changes a real input by at most one half on the integer grid.

Instances

source

noncomputable def TorchLean.Floats.neuralRoundAtScale (rnd : ℝ → ℤ) (step : ℝ) (_hstep : 0 < step) (x : ℝ) :

ℝ

Round x to the integer grid with spacing step.

This fixed-scale operation is the common core of fixed-point arithmetic and affine quantization. Unlike neuralRound, the scale is supplied explicitly rather than chosen from the magnitude of x by an exponent format. Requiring positivity prevents a zero scale from silently turning the operation into the constant-zero map through totalized real division.

Instances For

source

instance TorchLean.Floats.instNeuralValidRndNeuralFloorRound :

NeuralValidRnd neuralFloorRound

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

source

instance TorchLean.Floats.instNeuralValidRndNeuralCeilRound :

NeuralValidRnd neuralCeilRound

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

source

instance TorchLean.Floats.instNeuralValidRndNeuralTruncRound :

NeuralValidRnd neuralTruncRound

Toward-zero integer rounding is monotone and fixes integers.

source

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.

source

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⌋.

source

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.

source

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.

source

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.

source

instance TorchLean.Floats.instNeuralValidRndNeuralNearestEven :

NeuralValidRnd neuralNearestEven

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

source

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.

source

theorem TorchLean.Floats.neuralNearestEven_abs_eq_round (x : ℝ) :

|↑(neuralNearestEven x) - x| = |↑(round x) - x|

Nearest-even has the same distance from the input as Mathlib's ties-up nearest integer.

source

theorem TorchLean.Floats.neuralNearestEven_is_nearest_integer (x : ℝ) (n : ℤ) :

|↑(neuralNearestEven x) - x| ≤ |↑n - x|

Nearest-even minimizes distance to the input among all integers.

source

instance TorchLean.Floats.instNeuralValidRndToNearestNeuralNearestEven :

NeuralValidRndToNearest neuralNearestEven

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

source

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 pure NeuralFloat mantissa/exponent pair and interpret it with neuralToReal.

Instances For

source

theorem TorchLean.Floats.neuralScaledMantissa_eq_div {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) :

neuralScaledMantissa β fexp x = x / neuralBpow β (neuralCexp β fexp x)

The scaled mantissa is the input divided by its canonical radix power.

source

theorem TorchLean.Floats.neural_scaled_mantissa_int_of_generic {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) (hx : neuralGenericFormat β fexp x) :

∃ (n : ℤ), neuralScaledMantissa β fexp x = ↑n

If x is already in the generic format grid, then neural_scaled_mantissa β fexp x is an integer.

In words: exact representability means “no fractional bits at the chosen exponent scale”.

source

@[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.

source

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.

source

theorem TorchLean.Floats.neural_generic_format_of_scaled_mantissa_int {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) (n : ℤ) (h : neuralScaledMantissa β fexp x = ↑n) :

neuralGenericFormat β fexp x

An integral canonical scaled mantissa is sufficient for exact representability.

source

theorem TorchLean.Floats.neural_generic_format_iff_scaled_mantissa_int {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) :

neuralGenericFormat β fexp x ↔ ∃ (n : ℤ), neuralScaledMantissa β fexp x = ↑n

Exact representability is equivalent to integrality of the canonical scaled mantissa.

source

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.

Named standard modes #

source

inductive TorchLean.Floats.NeuralRoundingMode :

Type

The four standard rounding-direction attributes used by the generic float model.

nearestEven : NeuralRoundingMode
Round to the nearest value, resolving a tie toward an even integer at the selected scale.
Under the usual Flocq conditions (in particular, excluding the precision-one even-radix corner case), this agrees with the familiar even canonical-significand description.
towardZero : NeuralRoundingMode
Round toward zero.
towardPositive : NeuralRoundingMode
Round toward positive infinity.
towardNegative : NeuralRoundingMode
Round toward negative infinity.

Instances For

source

@[implicit_reducible]

instance TorchLean.Floats.instDecidableEqNeuralRoundingMode :

DecidableEq NeuralRoundingMode

source

@[implicit_reducible]

instance TorchLean.Floats.instReprNeuralRoundingMode :

Repr NeuralRoundingMode

source

def TorchLean.Floats.instReprNeuralRoundingMode.repr :

NeuralRoundingMode → ℕ → Std.Format