Exact Operations on Mantissa/Exponent Values

These operations manipulate NeuralFloat representations without rounding. Addition aligns both operands to their smaller exponent; multiplication adds exponents. Their correctness theorems are radix-parametric counterparts of Flocq's Calc.Operations results.

theorem TorchLean.Floats.neuralIntPower_cast_eq_bpow (β : NeuralRadix) {e : ℤ} (he : 0 ≤ e) : ↑(neuralIntPower β e) = neuralBpow β e

Integer radix powers agree with real radix powers at nonnegative exponents.

structure TorchLean.Floats.NeuralFloatAlignment : Type

Two integer mantissas expressed on a common exponent grid.

• leftMantissa : ℤ

  First aligned mantissa.

• rightMantissa : ℤ

  Second aligned mantissa.

• exponent : ℤ

  Common exponent, equal to the smaller input exponent.

def TorchLean.Floats.NeuralFloat.align {β : NeuralRadix} (f g : NeuralFloat β) : NeuralFloatAlignment

Align two representations to the smaller exponent without changing their real values.

theorem TorchLean.Floats.NeuralFloat.align_toReal {β : NeuralRadix} (f g : NeuralFloat β) : neuralToReal f = neuralToReal { mantissa := (f.align g).leftMantissa, exponent := (f.align g).exponent } ∧ neuralToReal g = neuralToReal { mantissa := (f.align g).rightMantissa, exponent := (f.align g).exponent }

Alignment preserves both represented real values.

theorem TorchLean.Floats.NeuralFloat.align_exponent {β : NeuralRadix} (f g : NeuralFloat β) : (f.align g).exponent = min f.exponent g.exponent

Alignment selects the minimum input exponent.

def TorchLean.Floats.NeuralFloat.negExact {β : NeuralRadix} (f : NeuralFloat β) : NeuralFloat β

Exact negation of a mantissa/exponent representation.

def TorchLean.Floats.NeuralFloat.absExact {β : NeuralRadix} (f : NeuralFloat β) : NeuralFloat β

Exact absolute value of a mantissa/exponent representation.

def TorchLean.Floats.NeuralFloat.addExact {β : NeuralRadix} (f g : NeuralFloat β) : NeuralFloat β

Exact addition after exponent alignment.

def TorchLean.Floats.NeuralFloat.subExact {β : NeuralRadix} (f g : NeuralFloat β) : NeuralFloat β

Exact subtraction after exponent alignment.

def TorchLean.Floats.NeuralFloat.mulExact {β : NeuralRadix} (f g : NeuralFloat β) : NeuralFloat β

Exact multiplication of mantissas with exponent addition.

@[simp]

theorem TorchLean.Floats.NeuralFloat.toReal_negExact {β : NeuralRadix} (f : NeuralFloat β) : neuralToReal f.negExact = -neuralToReal f

@[simp]

theorem TorchLean.Floats.NeuralFloat.toReal_absExact {β : NeuralRadix} (f : NeuralFloat β) : neuralToReal f.absExact = |neuralToReal f|

@[simp]

theorem TorchLean.Floats.NeuralFloat.toReal_addExact {β : NeuralRadix} (f g : NeuralFloat β) : neuralToReal (f.addExact g) = neuralToReal f + neuralToReal g

@[simp]

theorem TorchLean.Floats.NeuralFloat.toReal_subExact {β : NeuralRadix} (f g : NeuralFloat β) : neuralToReal (f.subExact g) = neuralToReal f - neuralToReal g

@[simp]

theorem TorchLean.Floats.NeuralFloat.toReal_mulExact {β : NeuralRadix} (f g : NeuralFloat β) : neuralToReal (f.mulExact g) = neuralToReal f * neuralToReal g