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.

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.