Rounding Away from Zero

Away-from-zero rounding uses ceiling on nonnegative inputs and floor on negative inputs. Together with toward-zero rounding, it supplies the second endpoint decomposition for arbitrary valid integer rounding modes.

noncomputable def TorchLean.Floats.neuralAwayRound (x : ℝ) : ℤ

Integer rounding away from zero.

theorem TorchLean.Floats.neuralAwayRound_eq_floor {x : ℝ} (hx : x < 0) : neuralAwayRound x = neuralFloorRound x

Away-from-zero agrees with floor on negative inputs.

theorem TorchLean.Floats.neuralAwayRound_eq_ceil {x : ℝ} (hx : 0 ≤ x) : neuralAwayRound x = neuralCeilRound x

Away-from-zero agrees with ceiling on nonnegative inputs.

theorem TorchLean.Floats.neuralAwayRound_eq_floor_of_nonpos {x : ℝ} (hx : x ≤ 0) : neuralAwayRound x = neuralFloorRound x

On nonpositive inputs, away-from-zero agrees with floor, including at zero.

instance TorchLean.Floats.neuralAwayRoundValid : NeuralValidRnd neuralAwayRound

Away-from-zero rounding is monotone and fixes integers.

theorem TorchLean.Floats.neural_valid_round_eq_trunc_or_away (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) : rnd x = neuralTruncRound x ∨ rnd x = neuralAwayRound x

Arbitrary valid integer rounding chooses toward-zero or away-from-zero.

def TorchLean.Floats.NeuralRoundAwayFromZeroPoint (F : ℝ → Prop) (x f : ℝ) : Prop

Away-from-zero uses upward rounding for nonnegative values and downward rounding otherwise.

theorem TorchLean.Floats.neuralRound_away_point {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) : NeuralRoundAwayFromZeroPoint (neuralGenericFormat β fexp) x (neuralRound neuralAwayRound x)

Generic away-from-zero rounding satisfies its semantic point specification.