Configured binary helpers for approximation theorems

This module contains the backend-generic glue used by the executable universal-approximation theorems. We keep it independent of any one approximation construction (hinge sums, shallow ReLU MLPs, convolutional models, or transformer-style models) and record the common semantic operations:

• evaluating a two-layer ReLU MLP over a configured executable binary format,
• mapping executable binary values back to their real denotation, and
• interpreting executable linear-layer parameters as real parameters.

The mathematical role is the standard one in floating-point analysis: separate the exact real network from the concrete execution, then bridge the two by explicit rounding hypotheses or verified rounding lemmas. Useful references for this separation are IEEE Std 754-2019, Goldberg's survey on floating-point arithmetic, and Higham's treatment of numerical error analysis. The ReLU approximation side is connected through ReLUMlpBridge, which supplies the real-valued MLP semantics used by the universal-approximation files.

def NN.MLTheory.Proofs.UniversalApproximation.BinaryExecCore.mlpEval {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] {n hidDim : ℕ} (l1 : Spec.LinearSpec (FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) n hidDim) (l2 : Spec.LinearSpec (FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) hidDim 1) (x : TorchLean.Tensor (FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) [n]) : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)

Evaluate a two-layer ReLU MLP over a configured executable binary format.

The corresponding real-valued evaluator is mlpEval from ReLUMlpBridge. Approximation theorems compare the real denotation Model.toReal (toModel (mlpEval l1 l2 x)) with that real evaluator applied to tensorToReal x, isolating the floating-point execution error from the approximation and quantization errors.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.BinaryExecCore.tensorToReal {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] {s : Spec.Shape} (t : TorchLean.Tensor (FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) s) : TorchLean.Tensor ℝ s

Interpret a configured binary tensor entrywise using the model's total real denotation.

Exceptional values follow Model.toReal; this map does not assert that the entries are finite.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.BinaryExecCore.linearSpecToReal {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] {inDim outDim : ℕ} (m : Spec.LinearSpec (FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) inDim outDim) : Spec.LinearSpec ℝ inDim outDim

Interpret executable linear-layer parameters as real-valued parameters entrywise.

This helper is used in three-term bounds: real approximation error + parameter quantization error + concrete execution error.