Generic Rounding Properties

Order properties that follow directly from scaling by a positive radix power. These results do not assume a particular standard format.

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

Rounding toward negative infinity never exceeds the exact value.

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

Rounding toward positive infinity never falls below the exact value.

theorem TorchLean.Floats.neural_floor_le_valid_round (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) : neuralFloorRound x ≤ rnd x

Every valid integer rounding rule lies between floor and ceiling.

theorem TorchLean.Floats.neural_valid_round_le_ceil (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) : rnd x ≤ neuralCeilRound x

Every valid integer rounding rule lies between floor and ceiling.

theorem TorchLean.Floats.neural_valid_round_eq_floor_or_ceil (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) : rnd x = neuralFloorRound x ∨ rnd x = neuralCeilRound x

Every valid integer rounding chooses either floor or ceiling.

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

Every valid format rounding lies above directed-down rounding.

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

Every valid format rounding lies below directed-up rounding.

theorem TorchLean.Floats.neuralRound_eq_floor_or_ceil {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) : neuralRound rnd x = neuralRound neuralFloorRound x ∨ neuralRound rnd x = neuralRound neuralCeilRound x

Every valid generic rounding chooses either directed-down or directed-up rounding.