Rounding Predicates

Semantic specifications for directed, toward-zero, and nearest rounding. They are independent of any radix or concrete format: a predicate F : ℝ → Prop identifies the representable values, and the point predicates characterize the required output among those values.

These definitions correspond to Flocq's Rnd_DN_pt, Rnd_UP_pt, Rnd_ZR_pt, and Rnd_N_pt.

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

f is the greatest F-value no larger than x.

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

f is the least F-value no smaller than x.

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

Toward-zero rounding uses directed down on nonnegative inputs and directed up on negative ones.

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

f is an F-value at least as close to x as every other representable value.

def TorchLean.Floats.NeuralRoundDown (F : ℝ → Prop) (round : ℝ → ℝ) : Prop

A rounding function rounds downward with respect to F at every input.

def TorchLean.Floats.NeuralRoundUp (F : ℝ → Prop) (round : ℝ → ℝ) : Prop

A rounding function rounds upward with respect to F at every input.

def TorchLean.Floats.NeuralRoundTowardZero (F : ℝ → Prop) (round : ℝ → ℝ) : Prop

A rounding function rounds toward zero with respect to F at every input.

def TorchLean.Floats.NeuralRoundNearest (F : ℝ → Prop) (round : ℝ → ℝ) : Prop

A rounding function rounds to a nearest F-value at every input.

theorem TorchLean.Floats.neuralRoundDownPoint_unique {F : ℝ → Prop} {x f g : ℝ} (hf : NeuralRoundDownPoint F x f) (hg : NeuralRoundDownPoint F x g) : f = g

A downward rounding point is unique.

theorem TorchLean.Floats.neuralRoundUpPoint_unique {F : ℝ → Prop} {x f g : ℝ} (hf : NeuralRoundUpPoint F x f) (hg : NeuralRoundUpPoint F x g) : f = g

An upward rounding point is unique.

theorem TorchLean.Floats.neuralRoundDownPoint_refl {F : ℝ → Prop} {x : ℝ} (hx : F x) : NeuralRoundDownPoint F x x

A representable value is its own downward rounding point.

theorem TorchLean.Floats.neuralRoundUpPoint_refl {F : ℝ → Prop} {x : ℝ} (hx : F x) : NeuralRoundUpPoint F x x

A representable value is its own upward rounding point.

theorem TorchLean.Floats.neuralRoundUpPoint_neg {F : ℝ → Prop} (hneg : ∀ (x : ℝ), F x → F (-x)) {x f : ℝ} (hf : NeuralRoundDownPoint F x f) : NeuralRoundUpPoint F (-x) (-f)

Negation turns a downward point into an upward point for a symmetric format.

theorem TorchLean.Floats.neuralRoundDownPoint_neg {F : ℝ → Prop} (hneg : ∀ (x : ℝ), F x → F (-x)) {x f : ℝ} (hf : NeuralRoundUpPoint F x f) : NeuralRoundDownPoint F (-x) (-f)

Negation turns an upward point into a downward point for a symmetric format.

theorem TorchLean.Floats.neuralRoundDownUpPoint_split {F : ℝ → Prop} {x d u f : ℝ} (hd : NeuralRoundDownPoint F x d) (hu : NeuralRoundUpPoint F x u) (hf : F f) : f ≤ d ∨ u ≤ f

Any representable value lies below the downward point or above the upward point.

theorem TorchLean.Floats.neuralRoundNearestPoint_of_down_up {F : ℝ → Prop} {x d u f : ℝ} (hd : NeuralRoundDownPoint F x d) (hu : NeuralRoundUpPoint F x u) (hf : F f) (hfd : |f - x| ≤ |d - x|) (hfu : |f - x| ≤ |u - x|) : NeuralRoundNearestPoint F x f

A representable value no farther than both directed neighbors is globally nearest. Every other representable value lies outside the interval between those neighbors.