Round to Odd

For an inexact real input, oddRound selects the odd member of the two adjacent integers. Exact integers are unchanged. Applied to a binary scaled mantissa, this is the usual round-to-odd or jamming rule: discarded information is recorded by setting the least-significant retained bit.

The double-rounding result below concerns a fixed binary grid. The corresponding theorem for floating-point formats also needs hypotheses relating their precision and minimum exponents.

References:

• S. Boldo and G. Melquiond, “Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd,” IEEE Transactions on Computers 57(4), 2008, pp. 462–471, §III-C, Theorem 3, DOI: 10.1109/TC.2007.70819. Author manuscript: https://guillaume.melquiond.fr/doc/08-tc.pdf.
• Flocq 4.2.2, src/Prop/Round_odd.v, definitions Zrnd_odd, Rnd_odd_pt, and the format-level theorem round_N_odd: https://flocq.gitlabpages.inria.fr/releases/flocq-4.2.2.tar.gz.

noncomputable def FloatLib.Floats.Formats.Flocq.oddRound (x : ℝ) : ℤ

Preserve integers; otherwise select the odd integer among floor x and floor x + 1.

theorem FloatLib.Floats.Formats.Flocq.oddRound_bounds (x : ℝ) : ⌊x⌋ ≤ oddRound x ∧ oddRound x ≤ ⌊x⌋ + 1

Round-to-odd always selects one of the two adjacent integers.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.oddRound_intCast (n : ℤ) : oddRound ↑n = n

Exact integers are fixed by round-to-odd.

theorem FloatLib.Floats.Formats.Flocq.oddRound_odd_of_inexact {x : ℝ} (hx : x ≠ ↑⌊x⌋) : Odd (oddRound x)

An inexact input receives an odd integer result.

instance FloatLib.Floats.Formats.Flocq.oddRoundValid : ValidRnd oddRound

Round-to-odd is monotone and fixes every integer.

theorem FloatLib.Floats.Formats.Flocq.oddRound_lt_even {x : ℝ} {n : ℤ} (hxn : x < ↑n) (hn : Even n) : oddRound x < n

An input below an even integer rounds to an integer strictly below it.

theorem FloatLib.Floats.Formats.Flocq.even_lt_oddRound {x : ℝ} {n : ℤ} (hnx : ↑n < x) (hn : Even n) : n < oddRound x

An input above an even integer rounds to an integer strictly above it.

theorem FloatLib.Floats.Formats.Flocq.nearestEven_roundOdd_binary_extra (extra : ℕ) (x : ℝ) : nearestEven (↑(oddRound (x * 2 ^ (extra + 2))) / 2 ^ (extra + 2)) = nearestEven x

Round-to-odd with at least two extra binary digits prevents nearest-even double rounding on the integer grid. roundAtScale_nearestEven_after_odd_binary_extra transports this to any fixed grid; no floating-point (exponent-dependent) version is proved in this library.

theorem FloatLib.Floats.Formats.Flocq.roundAtScale_nearestEven_after_odd_binary_extra (extra : ℕ) (step x : ℝ) (hstep : 0 < step) : roundAtScale nearestEven step hstep (roundAtScale oddRound (step / 2 ^ (extra + 2)) ⋯ x) = roundAtScale nearestEven step hstep x

Round-to-odd on a finer binary grid prevents nearest-even double rounding on a coarser grid.

The coarse grid has positive spacing step; the intermediate grid is finer by extra + 2 binary digits. Both grids are fixed, so the theorem applies to fixed-point and affine-quantization grids. It does not cover floating-point formats, whose spacing depends on the exponent of the value.

theorem FloatLib.Floats.Formats.Flocq.oddRound_scaled_mantissa_odd_of_not_generic {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] {x : ℝ} (hx : ¬genericFormat β fexp x) : Odd (oddRound (scaledMantissa β fexp x))

If x is not representable, round-to-odd selects an odd scaled integer mantissa.

theorem FloatLib.Floats.Formats.Flocq.generic_format_round_odd {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) : genericFormat β fexp (round oddRound x)

Round-to-odd produces a value in the selected generic format.

def FloatLib.Floats.Formats.Flocq.RoundOddPoint (β : Numerics.Radix) (F : ℝ → Prop) (exponent : ℤ) (x f : ℝ) : Prop

Semantic round-to-odd specification at the grid exponent selected for the input.

An exact input is unchanged. An inexact result is a directed neighbor whose integer mantissa is odd at exponent. Fixing this exponent matters: every nonzero binary dyadic has an odd mantissa at some exponent, which alone would not characterize round-to-odd.

theorem FloatLib.Floats.Formats.Flocq.round_odd_point {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) : RoundOddPoint β (genericFormat β fexp) (cexp β fexp x) x (round oddRound x)

Generic rounding with oddRound satisfies the round-to-odd point specification.

def FloatLib.Floats.Formats.Flocq.RoundOddCanonicalPoint (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] (x f : ℝ) : Prop

Flocq's round-to-odd point predicate, testing parity at the result's canonical exponent. Abrupt-underflow grids can give a different exponent to the input and output, so input-grid parity alone does not establish this predicate.

theorem FloatLib.Floats.Formats.Flocq.round_odd_canonical_point_of_cexp_eq {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) (hexponent : cexp β fexp (round oddRound x) = cexp β fexp x) : RoundOddCanonicalPoint β fexp x (round oddRound x)

Input-grid rounding satisfies canonical round-to-odd whenever the canonical exponent is preserved. Fixed-point grids always satisfy this condition.

theorem FloatLib.Floats.Formats.Flocq.round_odd_canonical_point_FIX (β : Numerics.Radix) (exponent : ℤ) (x : ℝ) : RoundOddCanonicalPoint β (fixExp exponent) x (round oddRound x)

Fixed-point round-to-odd meets Flocq's canonical parity convention for every input.