Integer Digits, Scaling, and Slices

These definitions are the effective integer layer used by radix-based rounding algorithms. Signed division and remainder use Int.tdiv and Int.tmod, matching Flocq's quotient and remainder toward zero rather than Lean's Euclidean / and % operations.

def TorchLean.Floats.neuralIntPower (β : NeuralRadix) (e : ℤ) : ℤ

Integer radix power, with the Flocq convention that negative powers are zero.

@[simp]

theorem TorchLean.Floats.neuralIntPower_of_nonneg (β : NeuralRadix) {e : ℤ} (he : 0 ≤ e) : neuralIntPower β e = Int.ofNat (β.base ^ e.toNat)

@[simp]

theorem TorchLean.Floats.neuralIntPower_of_neg (β : NeuralRadix) {e : ℤ} (he : e < 0) : neuralIntPower β e = 0

@[simp]

theorem TorchLean.Floats.neuralIntPower_zero (β : NeuralRadix) : neuralIntPower β 0 = 1

def TorchLean.Floats.neuralDigit (β : NeuralRadix) (n k : ℤ) : ℤ

The signed radix digit at position k.

@[simp]

theorem TorchLean.Floats.neuralDigit_zero (β : NeuralRadix) (k : ℤ) : neuralDigit β 0 k = 0

@[simp]

theorem TorchLean.Floats.neuralDigit_neg (β : NeuralRadix) (n k : ℤ) : neuralDigit β (-n) k = -neuralDigit β n k

theorem TorchLean.Floats.neuralDigit_of_neg_index (β : NeuralRadix) (n : ℤ) {k : ℤ} (hk : k < 0) : neuralDigit β n k = 0

theorem TorchLean.Floats.neuralDigit_abs_lt_base (β : NeuralRadix) (n k : ℤ) : |neuralDigit β n k| < Int.ofNat β.base

Every signed digit has absolute value strictly smaller than the radix.

def TorchLean.Floats.neuralScale (β : NeuralRadix) (n k : ℤ) : ℤ

Shift an integer left for nonnegative k, and right with truncation for negative k.

theorem TorchLean.Floats.neuralScale_of_nonneg (β : NeuralRadix) (n : ℤ) {k : ℤ} (hk : 0 ≤ k) : neuralScale β n k = n * neuralIntPower β k

theorem TorchLean.Floats.neuralScale_of_neg (β : NeuralRadix) (n : ℤ) {k : ℤ} (hk : k < 0) : neuralScale β n k = n.tdiv (neuralIntPower β (-k))

@[simp]

theorem TorchLean.Floats.neuralScale_zero_value (β : NeuralRadix) (k : ℤ) : neuralScale β 0 k = 0

@[simp]

theorem TorchLean.Floats.neuralScale_zero_shift (β : NeuralRadix) (n : ℤ) : neuralScale β n 0 = n

@[simp]

theorem TorchLean.Floats.neuralScale_neg (β : NeuralRadix) (n k : ℤ) : neuralScale β (-n) k = -neuralScale β n k

def TorchLean.Floats.neuralSlice (β : NeuralRadix) (n start width : ℤ) : ℤ

Extract width radix digits beginning at start; negative widths produce zero.

@[simp]

theorem TorchLean.Floats.neuralSlice_zero_value (β : NeuralRadix) (start width : ℤ) : neuralSlice β 0 start width = 0

theorem TorchLean.Floats.neuralSlice_of_neg_width (β : NeuralRadix) (n start : ℤ) {width : ℤ} (hwidth : width < 0) : neuralSlice β n start width = 0

theorem TorchLean.Floats.neuralSlice_abs_lt_power (β : NeuralRadix) (n start : ℤ) {width : ℤ} (hwidth : 0 ≤ width) : |neuralSlice β n start width| < neuralIntPower β width

A nonnegative-width slice has absolute value below the corresponding radix power.

@[simp]

theorem TorchLean.Floats.neuralSlice_neg (β : NeuralRadix) (n start width : ℤ) : neuralSlice β (-n) start width = -neuralSlice β n start width

def TorchLean.Floats.neuralDigits (β : NeuralRadix) (n : ℤ) : ℕ

Number of base-β digits in the absolute value of an integer.

@[simp]

theorem TorchLean.Floats.neuralDigits_zero (β : NeuralRadix) : neuralDigits β 0 = 0

@[simp]

theorem TorchLean.Floats.neuralDigits_neg (β : NeuralRadix) (n : ℤ) : neuralDigits β (-n) = neuralDigits β n

theorem TorchLean.Floats.neuralDigits_pos {β : NeuralRadix} {n : ℤ} (hn : n ≠ 0) : 0 < neuralDigits β n

theorem TorchLean.Floats.neuralDigits_bounds (β : NeuralRadix) {n : ℤ} (hn : n ≠ 0) : β.base ^ (neuralDigits β n - 1) ≤ n.natAbs ∧ n.natAbs < β.base ^ neuralDigits β n

A nonzero integer lies between consecutive powers selected by its digit count.

theorem TorchLean.Floats.neuralMagnitude_intCast_of_pos (β : NeuralRadix) {n : ℤ} (hn : 0 < n) : neuralMagnitude β ↑n = ↑(neuralDigits β n)

The radix digit count of a positive integer is the magnitude of its real embedding.

theorem TorchLean.Floats.intCast_lt_neuralBpow_digits (β : NeuralRadix) {n : ℤ} (hn : 0 < n) : ↑n < neuralBpow β ↑(neuralDigits β n)

A positive integer is strictly below the radix power selected by its digit count.

theorem TorchLean.Floats.intCast_add_one_le_neuralBpow_digits (β : NeuralRadix) {n : ℤ} (hn : 0 < n) : ↑(n + 1) ≤ neuralBpow β ↑(neuralDigits β n)

The successor of a positive integer does not exceed its next radix-power boundary.

theorem TorchLean.Floats.neuralDigits_unique (β : NeuralRadix) {n : ℤ} (hn : n ≠ 0) {d : ℕ} (hd : 0 < d) (hlower : β.base ^ (d - 1) ≤ n.natAbs) (hupper : n.natAbs < β.base ^ d) : neuralDigits β n = d

The power bounds uniquely determine the digit count of a nonzero integer.

theorem TorchLean.Floats.neuralDigits_mono_abs (β : NeuralRadix) {n m : ℤ} (hn : n ≠ 0) (hnm : n.natAbs ≤ m.natAbs) : neuralDigits β n ≤ neuralDigits β m

Digit count is monotone with respect to integer absolute value away from zero.

theorem TorchLean.Floats.neuralDigits_mul_le (β : NeuralRadix) {n m : ℤ} (hn : n ≠ 0) (hm : m ≠ 0) : neuralDigits β (n * m) ≤ neuralDigits β n + neuralDigits β m

A nonzero product uses at most the sum of the operand digit counts.

theorem TorchLean.Floats.neuralDigits_power (β : NeuralRadix) (k : ℕ) : neuralDigits β (Int.ofNat (β.base ^ k)) = k + 1

A positive radix power has one more digit than its exponent.