NeuralFloat Conversion Helpers

This module contains small utilities for moving values between:

• real semantics (ℝ), and
• the Flocq-style mantissa/exponent payload NeuralFloat β.

Important scope note:

• The canonical rounding semantics in this folder is neural_round (see Rounding.lean), which models one “compute in ℝ, then round” step and comes with the key half-ULP theorem neural_error_bound_ulp (under round-to-nearest assumptions).
• The helpers in this file are conversion utilities and examples: packaging the rounded result into a NeuralFloat record and attaching a small amount of error/ULP metadata.

If you are doing proofs about rounding error, prefer theorems in:

• NN/Floats/NeuralFloat/Rounding.lean (core half-ULP bound), and
• NN/Floats/NeuralFloat/ErrorBounds.lean (small derived bounds).

structure TorchLean.Floats.Conversion.NeuralConversionResult (α : Type) : Type

Conversion result with error tracking.

• value : α

  Converted value.

• error_bound : ℝ

  Absolute error bound for the conversion step.

  For conversions that only repackage an already-rounded value, this may be a metadata field rather than a proved bound.

• is_exact : Bool

  Whether the conversion was exact (error_bound = 0).

• ulp_error : Option ℝ

  Optional ULP-scale metadata at the input point.

  This is not itself an error bound. For round-to-nearest, a typical one-step error bound is ulp(x)/2, proved separately (see neural_error_bound_ulp).

• target_phase : TrainingPhase

  Training phase used when interpreting ULP scaling hooks.

noncomputable def TorchLean.Floats.Conversion.neuralFloatToReal {β : NeuralRadix} (f : NeuralFloat β) : NeuralConversionResult ℝ

Convert a NeuralFloat β payload to its real semantics, returning lightweight metadata.

In words: the returned value is exactly neural_to_real f. The error_bound field is the metadata stored in the input record (it is not recomputed here).

noncomputable def TorchLean.Floats.Conversion.realToNeuralFloat {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) (phase : TrainingPhase := TrainingPhase.forward) : NeuralConversionResult (NeuralFloat β)

Round a real number x onto the (β,fexp,rnd) grid and package it as a NeuralFloat β.

In words: The returned payload is the same one used by neural_round (it uses mantissa := rnd (scaled_mantissa x) and exponent := cexp x), and error_bound = |neural_to_real(value) - x| is the actual absolute error for this rounding step.

If you additionally assume round-to-nearest (NeuralValidRndToNearest), the theorem neural_error_bound_ulp bounds this error by ulp(x)/2.

noncomputable def TorchLean.Floats.Conversion.listToNeuralFloats {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (values : List ℝ) (phase : TrainingPhase := TrainingPhase.forward) : NeuralConversionResult (List (NeuralFloat β))

Convert list of reals to neural floats

noncomputable def TorchLean.Floats.Conversion.neuralFloatsToList {β : NeuralRadix} (neural_floats : List (NeuralFloat β)) : NeuralConversionResult (List ℝ)

Convert neural floats back to reals

noncomputable def TorchLean.Floats.Conversion.testRoundTripAccuracy {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (original : ℝ) (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (phase : TrainingPhase := TrainingPhase.forward) : ℝ

Test conversion round-trip accuracy

noncomputable def TorchLean.Floats.Conversion.validateNeuralConversion (original : ℝ) (converted : NeuralConversionResult ℝ) (tolerance : ℝ) : Bool

Validate conversion preserves essential properties