Nearest Rounding with a Tie Choice

neuralNearestChoice chooseUp rounds to a nearest integer. At an exact midpoint, chooseUp f decides whether the lower integer f or the upper integer f + 1 is selected. This is the native Lean counterpart of Flocq's Znearest choice.

noncomputable def TorchLean.Floats.neuralNearestChoice (chooseUp : ℤ → Bool) (x : ℝ) : ℤ

Round to a nearest integer, resolving a midpoint according to its lower integer.

theorem TorchLean.Floats.neuralNearestChoice_eq_floor_or_ceil (chooseUp : ℤ → Bool) (x : ℝ) : neuralNearestChoice chooseUp x = ⌊x⌋ ∨ neuralNearestChoice chooseUp x = ⌈x⌉

Choice-based nearest rounding always selects floor or ceiling.

theorem TorchLean.Floats.neuralNearestChoice_bounds (chooseUp : ℤ → Bool) (x : ℝ) : ⌊x⌋ ≤ neuralNearestChoice chooseUp x ∧ neuralNearestChoice chooseUp x ≤ ⌊x⌋ + 1

Choice-based nearest rounding lies between floor and floor plus one.

@[simp]

theorem TorchLean.Floats.neuralNearestChoice_intCast (chooseUp : ℤ → Bool) (n : ℤ) : neuralNearestChoice chooseUp ↑n = n

Choice-based nearest rounding fixes integers.

theorem TorchLean.Floats.neuralNearestChoice_abs_sub_le_half (chooseUp : ℤ → Bool) (x : ℝ) : |↑(neuralNearestChoice chooseUp x) - x| ≤ 1 / 2

Every tie choice has absolute error at most one half.

theorem TorchLean.Floats.neuralNearestChoice_mono (chooseUp : ℤ → Bool) {x y : ℝ} (hxy : x ≤ y) : neuralNearestChoice chooseUp x ≤ neuralNearestChoice chooseUp y

Choice-based nearest rounding is monotone.

instance TorchLean.Floats.neuralNearestChoiceValid (chooseUp : ℤ → Bool) : NeuralValidRndToNearest (neuralNearestChoice chooseUp)

Every tie-choice nearest mode is a valid nearest rounding mode.