Order Theory for Generic Rounding

Monotonicity is subtle because two inputs may be scaled with different canonical exponents. The proof separates equal-grid inputs from inputs in different magnitude bins and uses the bounds from GenericRound in the latter case.

theorem TorchLean.Floats.neuralRound_le_of_cexp_eq {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] {x y : ℝ} (hxy : x ≤ y) (he : neuralCexp β fexp x = neuralCexp β fexp y) : neuralRound rnd x ≤ neuralRound rnd y

Rounding is monotone when both inputs use the same canonical exponent.

theorem TorchLean.Floats.neuralRound_mono_pos {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] {x y : ℝ} (hx : 0 < x) (hxy : x ≤ y) : neuralRound rnd x ≤ neuralRound rnd y

Positive generic rounding is monotone.

theorem TorchLean.Floats.neuralRound_nonneg {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] {x : ℝ} (hx : 0 ≤ x) : 0 ≤ neuralRound rnd x

Rounding a nonnegative value with a valid mode produces a nonnegative value.

theorem TorchLean.Floats.neuralRound_nonpos {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] {x : ℝ} (hx : x ≤ 0) : neuralRound rnd x ≤ 0

Rounding a nonpositive value with a valid mode produces a nonpositive value.

theorem TorchLean.Floats.neuralRound_mono {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] {x y : ℝ} (hxy : x ≤ y) : neuralRound rnd x ≤ neuralRound rnd y

Generic rounding is monotone on all real inputs.

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

A representable lower value remains below rounding of any larger input.

theorem TorchLean.Floats.neural_round_le_generic {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] {x y : ℝ} (hy : neuralGenericFormat β fexp y) (hxy : x ≤ y) : neuralRound rnd x ≤ y

Rounding of a smaller input remains below a representable upper value.

theorem TorchLean.Floats.neuralRound_floor_point {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) : NeuralRoundDownPoint (neuralGenericFormat β fexp) x (neuralRound neuralFloorRound x)

Directed-down generic rounding selects the greatest representable value below its input.

theorem TorchLean.Floats.neuralRound_ceil_point {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) : NeuralRoundUpPoint (neuralGenericFormat β fexp) x (neuralRound neuralCeilRound x)

Directed-up generic rounding selects the least representable value above its input.

theorem TorchLean.Floats.neuralRound_trunc_point {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) : NeuralRoundTowardZeroPoint (neuralGenericFormat β fexp) x (neuralRound neuralTruncRound x)

Generic truncation satisfies the toward-zero rounding specification.

theorem TorchLean.Floats.neuralRound_nearestEven_error_le {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) (x : ℝ) : |neuralRound neuralNearestEven x - x| ≤ |neuralRound rnd x - x|

Nearest-even generic rounding is no farther from the input than any other integer rounding.

theorem TorchLean.Floats.neuralRound_nearestEven_point {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) : NeuralRoundNearestPoint (neuralGenericFormat β fexp) x (neuralRound neuralNearestEven x)

Nearest-even rounding selects a globally nearest representable value.