Ordered-representability capability

This proof-only capability states that every exact scalar has representable lower and upper neighbors. It provides the existence needed for total directed rounding without selecting an executable search algorithm or adding order fields to the universal numerical-system structure.

class FloatLib.Numerics.OrderedRepresentable (system : NumericalSystem) [Preorder system.Scalar] : Prop

Every scalar admits both a lower and an upper representable neighbor.

• lower_exists (input : system.Scalar) : ∃ (code : system.Code), Quantization.Ordered.LowerNeighbor system input code

  Existence of a greatest representable value below an input.

• upper_exists (input : system.Scalar) : ∃ (code : system.Code), Quantization.Ordered.UpperNeighbor system input code

  Existence of a least representable value above an input.

instance FloatLib.Numerics.exactOrderedRepresentable (α : Type) [Preorder α] : OrderedRepresentable (NumericalSystem.exact α)

In an exact numerical system, each input is its own lower and upper neighbor.

theorem FloatLib.Numerics.towardNegative_total (system : NumericalSystem) [Preorder system.Scalar] [OrderedRepresentable system] : (Quantization.Directed.towardNegative system).Total

Downward-directed quantization is total for an ordered-representable system.

theorem FloatLib.Numerics.towardPositive_total (system : NumericalSystem) [Preorder system.Scalar] [OrderedRepresentable system] : (Quantization.Directed.towardPositive system).Total

Upward-directed quantization is total for an ordered-representable system.