Floating-Point Adapters For Tensor Specifications

The numerical types in NN.Floats are independent of TorchLean's tensor and model interfaces. This module supplies the one-way adapters that let those types instantiate the broader Context expected by scalar-polymorphic specifications.

@[implicit_reducible]

noncomputable instance TorchLean.Floats.NF.instContext {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] : Context (NF β fexp rnd)

Use rounded-real NF arithmetic as a TorchLean specification scalar.

The general scalar interface requires a total α ^ α. Its adapter uses NF.checkedRealPow, which handles arbitrary exponents on positive bases, integer exponents on negative bases, and positive exponents at zero. The adapter selects its rounded-zero fallback only when checkedRealPow rejects the domain, such as a negative base with a noninteger exponent or zero with a negative exponent; an accepted computation can independently round to zero. Direct numerical code should inspect the checked result, or use the unambiguous NF.powNat, rather than relying on that compatibility fallback.

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instContext : Context IEEE32Exec

Use executable binary32 arithmetic as a TorchLean specification scalar.