Round to Odd

For an inexact real input, neuralOddRound 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 TorchLean.Floats.neuralOddRound (x : ℝ) : ℤ

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

theorem TorchLean.Floats.neuralOddRound_bounds (x : ℝ) : ⌊x⌋ ≤ neuralOddRound x ∧ neuralOddRound x ≤ ⌊x⌋ + 1

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

@[simp]

theorem TorchLean.Floats.neuralOddRound_intCast (n : ℤ) : neuralOddRound ↑n = n

Exact integers are fixed by round-to-odd.

theorem TorchLean.Floats.neuralOddRound_odd_of_inexact {x : ℝ} (hx : x ≠ ↑⌊x⌋) : Odd (neuralOddRound x)

An inexact input receives an odd integer result.

instance TorchLean.Floats.neuralOddRoundValid : NeuralValidRnd neuralOddRound

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

theorem TorchLean.Floats.neuralOddRound_lt_even {x : ℝ} {n : ℤ} (hxn : x < ↑n) (hn : Even n) : neuralOddRound x < n

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

theorem TorchLean.Floats.even_lt_neuralOddRound {x : ℝ} {n : ℤ} (hnx : ↑n < x) (hn : Even n) : n < neuralOddRound x

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

theorem TorchLean.Floats.neuralNearestEven_roundOdd_binary_extra (extra : ℕ) (x : ℝ) : neuralNearestEven (↑(neuralOddRound (x * 2 ^ (extra + 2))) / 2 ^ (extra + 2)) = neuralNearestEven x

Round-to-odd with at least two extra binary digits prevents nearest-even double rounding. This is the integer-scale core of the format-level theorem.

theorem TorchLean.Floats.neuralRoundAtScale_nearestEven_after_odd_binary_extra (extra : ℕ) (step x : ℝ) (hstep : 0 < step) : neuralRoundAtScale neuralNearestEven step hstep (neuralRoundAtScale neuralOddRound (step / 2 ^ (extra + 2)) ⋯ x) = neuralRoundAtScale neuralNearestEven 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. The theorem is independent of any particular floating-point exponent format, so it also applies to fixed-point and affine-quantization grids.

theorem TorchLean.Floats.neuralOddRound_scaled_mantissa_odd_of_not_generic {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] {x : ℝ} (hx : ¬neuralGenericFormat β fexp x) : Odd (neuralOddRound (neuralScaledMantissa β fexp x))

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

theorem TorchLean.Floats.neural_generic_format_round_odd {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) : neuralGenericFormat β fexp (neuralRound neuralOddRound x)

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

def TorchLean.Floats.NeuralRoundOddPoint (β : NeuralRadix) (F : ℝ → Prop) (x f : ℝ) : Prop

Semantic round-to-odd specification. An exact input is unchanged. An inexact result is a directed neighbor and has an odd integer mantissa at an explicit radix exponent.

theorem TorchLean.Floats.neuralRound_odd_point {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) : NeuralRoundOddPoint β (neuralGenericFormat β fexp) x (neuralRound neuralOddRound x)

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