Radix Magnitude

The magnitude of a nonzero real $x$ is the unique integer $e$ for which $\beta^{e-1}\le|x|<\beta^e$. These bounds are the basic bridge between logarithmic magnitude, canonical exponents, and generic-format rounding.

theorem TorchLean.Floats.neuralMagnitude_spec (β : NeuralRadix) (x : ℝ) (hx : x ≠ 0) : neuralBpow β (neuralMagnitude β x - 1) ≤ |x| ∧ |x| < neuralBpow β (neuralMagnitude β x)

The logarithmic definition of neuralMagnitude satisfies the standard Flocq magnitude bounds.

theorem TorchLean.Floats.neuralBpow_magnitude_sub_one_le (β : NeuralRadix) (x : ℝ) (hx : x ≠ 0) : neuralBpow β (neuralMagnitude β x - 1) ≤ |x|

Lower magnitude bound for a nonzero real.

theorem TorchLean.Floats.abs_lt_neuralBpow_magnitude (β : NeuralRadix) (x : ℝ) (hx : x ≠ 0) : |x| < neuralBpow β (neuralMagnitude β x)

Strict upper magnitude bound for a nonzero real.

@[simp]

theorem TorchLean.Floats.neuralMagnitude_bpow (β : NeuralRadix) (e : ℤ) : neuralMagnitude β (neuralBpow β e) = e + 1

The magnitude of $\beta^e$ is $e+1$.

@[simp]

theorem TorchLean.Floats.neuralBpow_le_neuralBpow_iff (β : NeuralRadix) (e₁ e₂ : ℤ) : neuralBpow β e₁ ≤ neuralBpow β e₂ ↔ e₁ ≤ e₂

Radix powers preserve and reflect exponent order.

@[simp]

theorem TorchLean.Floats.neuralBpow_lt_neuralBpow_iff (β : NeuralRadix) (e₁ e₂ : ℤ) : neuralBpow β e₁ < neuralBpow β e₂ ↔ e₁ < e₂

Radix powers preserve and reflect strict exponent order.

theorem TorchLean.Floats.neuralMagnitude_eq_of_bpow_bounds (β : NeuralRadix) (x : ℝ) (e : ℤ) (hx : x ≠ 0) (hlower : neuralBpow β (e - 1) ≤ |x|) (hupper : |x| < neuralBpow β e) : neuralMagnitude β x = e

Radix-power bounds uniquely determine magnitude.

theorem TorchLean.Floats.neuralMagnitude_le_of_abs_lt_bpow (β : NeuralRadix) (x : ℝ) (e : ℤ) (hx : x ≠ 0) (hupper : |x| < neuralBpow β e) : neuralMagnitude β x ≤ e

Any strict radix-power upper bound is also an upper bound on magnitude.

theorem TorchLean.Floats.neuralMagnitude_mono_pos (β : NeuralRadix) {x y : ℝ} (hx : 0 < x) (hxy : x ≤ y) : neuralMagnitude β x ≤ neuralMagnitude β y

Magnitude is monotone on positive real inputs.

theorem TorchLean.Floats.neuralMagnitude_mono_abs (β : NeuralRadix) {x y : ℝ} (hx : x ≠ 0) (hxy : |x| ≤ |y|) : neuralMagnitude β x ≤ neuralMagnitude β y

Magnitude is monotone with respect to absolute value.

theorem TorchLean.Floats.neuralCexp_mono_abs (β : NeuralRadix) {fexp : ℤ → ℤ} [NeuralValidExp fexp] [NeuralMonotoneExp fexp] {x y : ℝ} (hx : x ≠ 0) (hxy : |x| ≤ |y|) : neuralCexp β fexp x ≤ neuralCexp β fexp y

A monotone exponent format preserves absolute-value order at canonical exponents.

theorem TorchLean.Floats.neuralMagnitude_mul_le_add (β : NeuralRadix) {x y : ℝ} (hx : x ≠ 0) (hy : y ≠ 0) : neuralMagnitude β (x * y) ≤ neuralMagnitude β x + neuralMagnitude β y

The magnitude of a nonzero product is at most the sum of operand magnitudes.

theorem TorchLean.Floats.neuralMagnitude_mul_bpow (β : NeuralRadix) (x : ℝ) (e : ℤ) (hx : x ≠ 0) : neuralMagnitude β (x * neuralBpow β e) = neuralMagnitude β x + e

Multiplication by a radix power shifts magnitude by its exponent.

theorem TorchLean.Floats.neuralBpow_eq_natCast_of_nonneg (β : NeuralRadix) (e : ℤ) (he : 0 ≤ e) : ∃ (n : ℕ), neuralBpow β e = ↑n

A radix power with nonnegative exponent is the cast of a natural number.