IEEE32 executable ReLU approximation

IEEE32Exec-facing theorems for combining:

• real-valued hinge-network approximation results, and
• a proved rounding/error bound for executing that hinge network with IEEE binary32 rounding.

The file is organized as a refinement chain:

• hingeFunIeee defines the executable network using IEEE-754 binary32 operations;
• HingeSumFinite records the exact finiteness obligations needed to rule out NaN/Inf paths;
• bridge lemmas connect the executable values, via ExecFloat.Binary.toModel followed by Model.toReal, to the rounded-ℝ FP32 semantics; and
• the final theorem packages real approximation, FP32 rounding, and IEEE execution into one certified error bound.

The construction exposes the finite-execution hypotheses at theorem boundaries: they are the precise trust boundary between mathematical approximation and concrete floating-point execution. The floating-point viewpoint follows IEEE Std 754-2019 and the standard analyses of Goldberg and Higham; the approximation side reuses the constructive hinge-network development in UniversalApproximation and UniversalApproximationFP32.

Embedding IEEE32Exec values into the FP32 (rounded-ℝ) model

@[inline]

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.embed (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) : TorchLean.Floats.FP32

Read an executable binary32 value as a point of the rounded-ℝ FP32 model.

@[simp]

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.embed_val (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) : (embed x).val = (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal

@[inline]

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.embedVec {n : ℕ} (v : Fin n → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) : Fin n → TorchLean.Floats.FP32

Pointwise embedding of a vector of ExecFloat.Binary 8 23 values into the FP32 model.

IEEE32Exec hinge network (same shape as hingeFunFp32)

@[inline]

def NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.reluIeee (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4

ReLU in the executable backend, as maximum x 0 rather than a branch, so that the IEEE 754 treatment of signed zeros and NaN comes from maximum itself.

@[inline]

def NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.hingeTermIeee {n : ℕ} (c t : Fin n → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (i : Fin n) : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4

One hinge term cᵢ * ReLU(x - tᵢ) evaluated in the executable IEEE32Exec backend.

@[inline]

def NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.hingeSumStepIeee {n : ℕ} (c t : Fin n → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4 → Fin n → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4

Fold step for summing hinge terms, used by hingeSumIeee.

def NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.hingeSumIeee {n : ℕ} (c t : Fin n → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4

Executable IEEE32Exec sum of hinge terms, in the fixed List.finRange order.

def NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.hingeFunIeee {n : ℕ} (t c : Fin n → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (b x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4

Executable IEEE32Exec hinge network: sum hinge terms, then add the executable bias.

A finiteness witness for IEEE evaluation (no NaN/Inf intermediates)

inductive NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.HingeSumFinite {n : ℕ} (t c : Fin n → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4 → List (Fin n) → Prop

Every intermediate of the hinge fold is finite: no subtraction, ReLU, product, or partial sum overflows to an infinity or produces a NaN.

Stating it as an inductive over the remaining index list rather than as a conjunction is what makes it checkable by decide on a concrete input, via instDecHingeSumFinite.

• nil {n : ℕ} {t c : Fin n → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4} {x acc : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4} (hacc : FloatLib.Floats.ExecFloat.Binary.isFinite acc = true) : HingeSumFinite t c x acc []
• cons {n : ℕ} {t c : Fin n → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4} {x acc : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4} {i : Fin n} {xs : List (Fin n)} (hsub : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.sub x (t i)) = true) (hmax : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.sub x (t i) ⊔ 0) = true) (hmul : FloatLib.Floats.ExecFloat.Binary.isFinite (hingeTermIeee c t x i) = true) (hadd : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.add acc (hingeTermIeee c t x i)) = true) (hrest : HingeSumFinite t c x (FloatLib.Floats.ExecFloat.add acc (hingeTermIeee c t x i)) xs) : HingeSumFinite t c x acc (i :: xs)

Discharging HingeSumFinite for concrete networks by computation

For typical verification workflows, t, c, and x are concrete IEEE32Exec constants coming from a lowered model artifact. In that setting, the easiest way to satisfy the HingeSumFinite … hypotheses is to compute the IEEE32Exec kernel and check finiteness at every intermediate.

instDecHingeSumFinite provides a Decidable instance generator for HingeSumFinite …. This enables proofs like:

  classical
  haveI := IEEE32ExecReLUApprox.instDecHingeSumFinite (t := t) (c := c) (x := x)
    (acc := (0 : IEEE32Exec)) (xs := List.finRange n)
  have hSum : HingeSumFinite t c x (0 : IEEE32Exec) (List.finRange n) := by
    decide

This does not solve the symbolic “no overflow for all x” problem, but it makes the pointwise theorems in this file directly usable for concrete executions.

def NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.instDecHingeSumFinite {n : ℕ} (t c : Fin n → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (x acc : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (xs : List (Fin n)) : Decidable (HingeSumFinite t c x acc xs)

Decide HingeSumFinite by walking the fold, which is what lets concrete runs use decide.

A compact finiteness hypothesis bundle (pointwise)

def NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.HingeEvalFiniteProp {n : ℕ} (t c : Fin n → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (b x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) : Prop

The finiteness hypotheses the pointwise theorems need, bundled into one conjunction.

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.hingeEvalFiniteProp_to_witness {n : ℕ} {t c : Fin n → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4} {b x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4} : HingeEvalFiniteProp t c b x → FloatLib.Floats.ExecFloat.Binary.isFinite x = true ∧ (∀ (i : Fin n), FloatLib.Floats.ExecFloat.Binary.isFinite (t i) = true) ∧ (∀ (i : Fin n), FloatLib.Floats.ExecFloat.Binary.isFinite (c i) = true) ∧ HingeSumFinite t c x 0 (List.finRange n) ∧ FloatLib.Floats.ExecFloat.Binary.isFinite (hingeFunIeee t c b x) = true

Unpack the compact pointwise finiteness bundle.

The executable bridge lemmas need separate finiteness facts for the input, parameters, fold state, and final output. Keeping the bundled form at theorem boundaries makes user-facing statements shorter, while this projection feeds the stepwise IEEE-754 refinement proofs.

Refinement: IEEE32Exec execution equals FP32 rounded-ℝ execution (as reals)

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.toReal_hinge_sum_ieee_eq_fp32_val {n : ℕ} (t c : Fin n → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) {acc : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4} {xs : List (Fin n)} (hfin : HingeSumFinite t c x acc xs) (hx : FloatLib.Floats.ExecFloat.Binary.isFinite x = true) (ht : ∀ (i : Fin n), FloatLib.Floats.ExecFloat.Binary.isFinite (t i) = true) (_hc : ∀ (i : Fin n), FloatLib.Floats.ExecFloat.Binary.isFinite (c i) = true) : (FloatLib.Floats.ExecFloat.Binary.toModel (List.foldl (hingeSumStepIeee c t x) acc xs)).toReal = (List.foldl (fun (acc32 : TorchLean.Floats.FP32) (i : Fin n) => acc32 + hingeTermFp32 (embedVec c) (embedVec t) (embed x) i) (embed acc) xs).val

Refine an executable IEEE hinge-term fold to the FP32 rounded-ℝ fold with the same order.

Floating-point addition is not associative, so the theorem preserves the exact List.finRange evaluation order. This is why the proof is fold-based rather than rewriting directly to an unordered finite sum.

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.toReal_hinge_fun_ieee_eq_fp32_val {n : ℕ} (t c : Fin n → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (b x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (hx : FloatLib.Floats.ExecFloat.Binary.isFinite x = true) (ht : ∀ (i : Fin n), FloatLib.Floats.ExecFloat.Binary.isFinite (t i) = true) (hc : ∀ (i : Fin n), FloatLib.Floats.ExecFloat.Binary.isFinite (c i) = true) (hSum : HingeSumFinite t c x 0 (List.finRange n)) (hOut : FloatLib.Floats.ExecFloat.Binary.isFinite (hingeFunIeee t c b x) = true) : (FloatLib.Floats.ExecFloat.Binary.toModel (hingeFunIeee t c b x)).toReal = (hingeFunFp32 (embedVec t) (embedVec c) (embed b) (embed x)).val

Refine the whole executable hinge network to the FP32 rounded-ℝ network.

The theorem composes the fold refinement with the final rounded bias addition. Its hypotheses are exactly the finiteness obligations needed by the IEEE-754 bridge lemmas.

IEEE32Exec error bound inherited from the FP32 bound

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.hinge_fun_ieee_abs_error_le {n : ℕ} (t c : Fin n → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (b x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (hx : FloatLib.Floats.ExecFloat.Binary.isFinite x = true) (ht : ∀ (i : Fin n), FloatLib.Floats.ExecFloat.Binary.isFinite (t i) = true) (hc : ∀ (i : Fin n), FloatLib.Floats.ExecFloat.Binary.isFinite (c i) = true) (hSum : HingeSumFinite t c x 0 (List.finRange n)) (hOut : FloatLib.Floats.ExecFloat.Binary.isFinite (hingeFunIeee t c b x) = true) : |(FloatLib.Floats.ExecFloat.Binary.toModel (hingeFunIeee t c b x)).toReal - hingeFunReal (embedVec t) (embedVec c) (embed b) (embed x)| ≤ hingeFunErrorBound (embedVec t) (embedVec c) (embed b) (embed x)

Lift the FP32 hinge-network rounding error bound to executable IEEE32Exec evaluation.

Once toReal_hinge_fun_ieee_eq_fp32_val identifies the executable result with the FP32 model, the already-proved FP32 error bound transfers directly.

“Approximation error + rounding error” (pointwise)

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.hinge_fun_total_abs_error_ieee_le {n : ℕ} (f : ℝ → ℝ) (t c : Fin n → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (b x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (hx : FloatLib.Floats.ExecFloat.Binary.isFinite x = true) (ht : ∀ (i : Fin n), FloatLib.Floats.ExecFloat.Binary.isFinite (t i) = true) (hc : ∀ (i : Fin n), FloatLib.Floats.ExecFloat.Binary.isFinite (c i) = true) (hSum : HingeSumFinite t c x 0 (List.finRange n)) (hOut : FloatLib.Floats.ExecFloat.Binary.isFinite (hingeFunIeee t c b x) = true) : |f (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel (hingeFunIeee t c b x)).toReal| ≤ |f (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - hingeFunReal (embedVec t) (embedVec c) (embed b) (embed x)| + hingeFunErrorBound (embedVec t) (embedVec c) (embed b) (embed x)

Pointwise triangle bound: target error to executable output is bounded by real approximation error plus the certified FP32/IEEE rounding error.

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.hinge_fun_total_abs_error_ieee_lt {n : ℕ} (f : ℝ → ℝ) (t c : Fin n → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (b x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (hx : FloatLib.Floats.ExecFloat.Binary.isFinite x = true) (ht : ∀ (i : Fin n), FloatLib.Floats.ExecFloat.Binary.isFinite (t i) = true) (hc : ∀ (i : Fin n), FloatLib.Floats.ExecFloat.Binary.isFinite (c i) = true) (hSum : HingeSumFinite t c x 0 (List.finRange n)) (hOut : FloatLib.Floats.ExecFloat.Binary.isFinite (hingeFunIeee t c b x) = true) {ε : ℝ} (hε : |f (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - hingeFunReal (embedVec t) (embedVec c) (embed b) (embed x)| < ε) : |f (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel (hingeFunIeee t c b x)).toReal| < ε + hingeFunErrorBound (embedVec t) (embedVec c) (embed b) (embed x)

Strict version of hinge_fun_total_abs_error_ieee_le, useful for approximation theorems.

IEEE32Exec pointwise ReLU approximation packaging (1D)

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.reluApproximationIccIEEE32Exec_fromHinge {f : ℝ → ℝ} {a b : ℝ} (ε : ℝ) : ε > 0 → (∃ (hidDim : ℕ) (t : Fin hidDim → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (c : Fin hidDim → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (b0 : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4), (∀ (i : Fin hidDim), FloatLib.Floats.ExecFloat.Binary.isFinite (t i) = true) ∧ (∀ (i : Fin hidDim), FloatLib.Floats.ExecFloat.Binary.isFinite (c i) = true) ∧ (∀ (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4), FloatLib.Floats.ExecFloat.Binary.isFinite x = true → (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b → HingeSumFinite t c x 0 (List.finRange hidDim) ∧ FloatLib.Floats.ExecFloat.Binary.isFinite (hingeFunIeee t c b0 x) = true) ∧ ∀ (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4), FloatLib.Floats.ExecFloat.Binary.isFinite x = true → (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b → |f (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - hingeFunReal (embedVec t) (embedVec c) (embed b0) (embed x)| < ε) → ∃ (hidDim : ℕ) (t : Fin hidDim → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (c : Fin hidDim → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (b0 : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4), ∀ (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4), FloatLib.Floats.ExecFloat.Binary.isFinite x = true → (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b → |f (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel (hingeFunIeee t c b0 x)).toReal| < ε + hingeFunErrorBound (embedVec t) (embedVec c) (embed b0) (embed x)

1D ReLU approximation statement over IEEE32Exec values.

This is not a full universal approximation theorem, because it does not construct IEEE weights from a real target. Instead it packages the already-proved pointwise inequality hinge_fun_total_abs_error_ieee_lt into an existence/for-all form:

• assume there exist IEEE32Exec hinge parameters (t,c,b0) that approximate f at the real level (via hingeFunReal on the embedded reals),
• and assume a finiteness/no-NaN/no-Inf witness for IEEE32Exec evaluation,
• then IEEE32Exec evaluation approximates f with an explicit extra rounding term hingeFunErrorBound.

Real approximation + quantization + IEEE rounding (1D, pointwise)

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.reluApproximationIccIEEE32Exec_threeTerm {f : ℝ → ℝ} {a b : ℝ} {hidDim : ℕ} (tR cR : Fin hidDim → ℝ) (t c : Fin hidDim → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (b0 : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (ht : ∀ (i : Fin hidDim), FloatLib.Floats.ExecFloat.Binary.isFinite (t i) = true) (hc : ∀ (i : Fin hidDim), FloatLib.Floats.ExecFloat.Binary.isFinite (c i) = true) (εApprox εQ : ℝ) : (∀ (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4), FloatLib.Floats.ExecFloat.Binary.isFinite x = true → (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b → HingeSumFinite t c x 0 (List.finRange hidDim) ∧ FloatLib.Floats.ExecFloat.Binary.isFinite (hingeFunIeee t c b0 x) = true) → (∀ (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4), FloatLib.Floats.ExecFloat.Binary.isFinite x = true → (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b → |f (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - hingeFun hidDim tR cR (f a) (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal| < εApprox) → (∀ (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4), FloatLib.Floats.ExecFloat.Binary.isFinite x = true → (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b → |hingeFun hidDim tR cR (f a) (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - hingeFunReal (embedVec t) (embedVec c) (embed b0) (embed x)| ≤ εQ) → ∀ (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4), FloatLib.Floats.ExecFloat.Binary.isFinite x = true → (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b → |f (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel (hingeFunIeee t c b0 x)).toReal| < εApprox + εQ + hingeFunErrorBound (embedVec t) (embedVec c) (embed b0) (embed x)

1D IEEE32Exec ReLU approximation with an explicit 3-term error decomposition:

1. Real approximation error: $|f(r)-\operatorname{hinge\_fun}(\ldots,r)|<\varepsilon_{\mathrm{approx}}$.
2. Quantization/reference error: $|\operatorname{hinge\_fun}(\ldots,r) -\operatorname{hinge\_fun}_{\mathbb R}(\operatorname{embed}(\text{IEEE parameters}), \operatorname{embed}(r))|\leq\varepsilon_Q$.
3. IEEE rounding error (proved): hingeFunErrorBound.

To obtain a fully synthesized IEEE32Exec approximation theorem, callers must additionally:

• construct IEEE32Exec parameters (t,c,b0) from the real hinge parameters, and
• prove the finiteness/no-NaN/no-Inf witnesses (HingeSumFinite + finite output), and
• prove a uniform bound εQ for the parameter-quantization step.

Pointwise wrappers that take HingeEvalFiniteProp

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.hinge_fun_total_abs_error_ieee_lt_of_finiteProp {n : ℕ} {f : ℝ → ℝ} (t c : Fin n → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (b x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) {ε : ℝ} (hFin : HingeEvalFiniteProp t c b x) (hε : |f (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - hingeFunReal (embedVec t) (embedVec c) (embed b) (embed x)| < ε) : |f (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel (hingeFunIeee t c b x)).toReal| < ε + hingeFunErrorBound (embedVec t) (embedVec c) (embed b) (embed x)

Pointwise strict error theorem using the compact finiteness bundle.

Use this form when a checker or proof generator has produced one HingeEvalFiniteProp certificate instead of separate hypotheses for input, parameter, fold, and output finiteness.

Same 3-term theorem, but with an explicit real bias parameter

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.reluApproximationIccIEEE32Exec_threeTerm_bias {f : ℝ → ℝ} {a b : ℝ} {hidDim : ℕ} (bR : ℝ) (tR cR : Fin hidDim → ℝ) (t c : Fin hidDim → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (b0 : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (ht : ∀ (i : Fin hidDim), FloatLib.Floats.ExecFloat.Binary.isFinite (t i) = true) (hc : ∀ (i : Fin hidDim), FloatLib.Floats.ExecFloat.Binary.isFinite (c i) = true) (εApprox εQ : ℝ) : (∀ (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4), FloatLib.Floats.ExecFloat.Binary.isFinite x = true → (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b → HingeSumFinite t c x 0 (List.finRange hidDim) ∧ FloatLib.Floats.ExecFloat.Binary.isFinite (hingeFunIeee t c b0 x) = true) → (∀ (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4), FloatLib.Floats.ExecFloat.Binary.isFinite x = true → (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b → |f (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - hingeFun hidDim tR cR bR (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal| < εApprox) → (∀ (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4), FloatLib.Floats.ExecFloat.Binary.isFinite x = true → (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b → |hingeFun hidDim tR cR bR (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - hingeFunReal (embedVec t) (embedVec c) (embed b0) (embed x)| ≤ εQ) → ∀ (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4), FloatLib.Floats.ExecFloat.Binary.isFinite x = true → (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b → |f (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel (hingeFunIeee t c b0 x)).toReal| < εApprox + εQ + hingeFunErrorBound (embedVec t) (embedVec c) (embed b0) (embed x)

Three-term IEEE32Exec approximation theorem with a caller-supplied real bias.

reluApproximationIccIEEE32Exec_threeTerm uses f a as the real hinge-network bias because that is what the constructive one-dimensional interpolation theorem emits. This variant is the more general numerical-analysis statement: any real reference bias bR may be compared with the executable bias b0.

Dyadic (roundDyadicToIEEE32) quantization helpers

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.fp32Round_abs_error_bound (x : ℝ) : |TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round x - x| ≤ FloatLib.Floats.Formats.Flocq.ulp FloatLib.Numerics.binaryRadix TorchLean.Floats.fexp32 x / 2

Generic half-ulp absolute-error bound for the rounded-ℝ binary32 model.

This is the standard floating-point local rounding statement specialized to TorchLean's FP32 format parameters. It is the bridge from abstract approximation coefficients to explicit quantization budgets.

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.toReal_roundDyadicToIEEE32_abs_error_bound (d : FloatLib.Numerics.Dyadic) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 d)) = true) : |(FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 d))).toReal - TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal d| ≤ FloatLib.Floats.Formats.Flocq.ulp FloatLib.Numerics.binaryRadix TorchLean.Floats.fexp32 (TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal d) / 2

Half-ulp error bound for dyadic values rounded into executable IEEE32Exec values.

The finiteness hypothesis excludes overflow/NaN paths, after which roundDyadicToIEEE32 agrees with the same real fp32Round operation used by the FP32 model.

Real hinge network sensitivity to parameter rounding (for a compact input domain)

This is the “εQ quantization” step for reluApproximationIccIEEE32Exec_threeTerm. The lemma below uses the compact-domain assumption that the reference knot locations tR lie in the input interval [a,b], then bounds the output perturbation using:

• a width term |b-a| to bound relu(x - tR i) on the interval, and
• relu_lipschitz to control the sensitivity to perturbing t.

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.hinge_fun_abs_error_le_of_params_Icc {n : ℕ} {a b x : ℝ} (tR cR tI cI : Fin n → ℝ) (bR bI : ℝ) (hx : x ∈ Set.Icc a b) (htR : ∀ (i : Fin n), tR i ∈ Set.Icc a b) : |hingeFun n tR cR bR x - hingeFun n tI cI bI x| ≤ |bR - bI| + ∑ i : Fin n, (|cR i - cI i| * |b - a| + |cI i| * |tR i - tI i|)

Sensitivity of a real hinge network to perturbing all parameters on a compact interval.

The bound decomposes into a bias perturbation, a coefficient perturbation weighted by the interval width, and a knot perturbation weighted by the absolute executable coefficients. This is the real analysis step that supplies the quantization term εQ.

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.hinge_fun_abs_error_le_of_params_Icc_uniform {n : ℕ} {a b x : ℝ} (tR cR tI cI : Fin n → ℝ) (bR bI : ℝ) (hx : x ∈ Set.Icc a b) (htR : ∀ (i : Fin n), tR i ∈ Set.Icc a b) {Δc C Δt : ℝ} (hC0 : 0 ≤ C) (hΔc : ∀ (i : Fin n), |cR i - cI i| ≤ Δc) (hC : ∀ (i : Fin n), |cI i| ≤ C) (hΔt : ∀ (i : Fin n), |tR i - tI i| ≤ Δt) : |hingeFun n tR cR bR x - hingeFun n tI cI bI x| ≤ |bR - bI| + ↑n * (Δc * |b - a| + C * Δt)

Uniform version of hinge_fun_abs_error_le_of_params_Icc.

Instead of summing per-neuron perturbation bounds, this theorem uses uniform coefficient and knot budgets Δc, C, and Δt, producing the simpler expression |bR-bI| + n * (Δc * |b-a| + C * Δt).

Removing the quantization term when reals are exactly representable

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.hinge_fun_real_embed_eq_hinge_fun_toReal {n : ℕ} (t c : Fin n → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (b x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) : hingeFunReal (embedVec t) (embedVec c) (embed b) (embed x) = hingeFun n (fun (i : Fin n) => (FloatLib.Floats.ExecFloat.Binary.toModel (t i)).toReal) (fun (i : Fin n) => (FloatLib.Floats.ExecFloat.Binary.toModel (c i)).toReal) (FloatLib.Floats.ExecFloat.Binary.toModel b).toReal (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal

The embedded FP32/IEEE real reference is exactly the ordinary real hinge network evaluated on entrywise ExecFloat.Binary.toModel followed by Model.toReal parameters.

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.hinge_fun_quantization_error_le_Icc_uniform {n : ℕ} {a b : ℝ} (tR cR : Fin n → ℝ) (bR : ℝ) (t c : Fin n → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (b0 x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (hxIn : (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b) (htR : ∀ (i : Fin n), tR i ∈ Set.Icc a b) {Δc C Δt : ℝ} (hC0 : 0 ≤ C) (hΔc : ∀ (i : Fin n), |cR i - (FloatLib.Floats.ExecFloat.Binary.toModel (c i)).toReal| ≤ Δc) (hC : ∀ (i : Fin n), |(FloatLib.Floats.ExecFloat.Binary.toModel (c i)).toReal| ≤ C) (hΔt : ∀ (i : Fin n), |tR i - (FloatLib.Floats.ExecFloat.Binary.toModel (t i)).toReal| ≤ Δt) : |hingeFun n tR cR bR (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - hingeFunReal (embedVec t) (embedVec c) (embed b0) (embed x)| ≤ |bR - (FloatLib.Floats.ExecFloat.Binary.toModel b0).toReal| + ↑n * (Δc * |b - a| + C * Δt)

Uniform quantization-error bound between a real hinge network and executable IEEE parameters.

This is the user-facing εQ discharge lemma when callers can bound coefficient and knot rounding errors uniformly.

Dyadic-to-IEEE32Exec quantization bound (εQ)

This lemma is a drop-in way to discharge the εQ premise of reluApproximationIccIEEE32Exec_threeTerm when IEEE parameters are obtained by rounding dyadic rationals via roundDyadicToIEEE32.

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.hinge_fun_dyadic_quantization_error_le_Icc {n : ℕ} {a b : ℝ} (tD cD : Fin n → FloatLib.Numerics.Dyadic) (bD : FloatLib.Numerics.Dyadic) (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (hxIn : (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b) (htIn : ∀ (i : Fin n), TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal (tD i) ∈ Set.Icc a b) : |hingeFun n (fun (i : Fin n) => TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal (tD i)) (fun (i : Fin n) => TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal (cD i)) (TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal bD) (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - hingeFunReal (embedVec fun (i : Fin n) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (tD i))) (embedVec fun (i : Fin n) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (cD i))) (embed (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 bD))) (embed x)| ≤ |TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal bD - (FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 bD))).toReal| + ∑ i : Fin n, (|TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal (cD i) - (FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (cD i)))).toReal| * |b - a| + |(FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (cD i)))).toReal| * |TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal (tD i) - (FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (tD i)))).toReal|)

Dyadic quantization error for a hinge network on [a,b].

The real reference uses exact dyadic parameters, while the executable reference uses those dyadics rounded to IEEE32Exec values. The result is still expressed as a sum of concrete per-parameter rounding errors.

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.hinge_fun_dyadic_quantization_error_le_Icc_halfUlp {n : ℕ} {a b : ℝ} (tD cD : Fin n → FloatLib.Numerics.Dyadic) (bD : FloatLib.Numerics.Dyadic) (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (hxIn : (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b) (htIn : ∀ (i : Fin n), TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal (tD i) ∈ Set.Icc a b) (htfin : ∀ (i : Fin n), FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (tD i))) = true) (hcfin : ∀ (i : Fin n), FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (cD i))) = true) (hbfin : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 bD)) = true) : |hingeFun n (fun (i : Fin n) => TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal (tD i)) (fun (i : Fin n) => TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal (cD i)) (TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal bD) (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - hingeFunReal (embedVec fun (i : Fin n) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (tD i))) (embedVec fun (i : Fin n) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (cD i))) (embed (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 bD))) (embed x)| ≤ FloatLib.Floats.Formats.Flocq.ulp FloatLib.Numerics.binaryRadix TorchLean.Floats.fexp32 (TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal bD) / 2 + ∑ i : Fin n, (FloatLib.Floats.Formats.Flocq.ulp FloatLib.Numerics.binaryRadix TorchLean.Floats.fexp32 (TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal (cD i)) / 2 * |b - a| + |(FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (cD i)))).toReal| * (FloatLib.Floats.Formats.Flocq.ulp FloatLib.Numerics.binaryRadix TorchLean.Floats.fexp32 (TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal (tD i)) / 2))

Dyadic quantization error with each per-parameter rounding error bounded by a half-ulp term.

This is the more automated version of hinge_fun_dyadic_quantization_error_le_Icc: callers provide finiteness of every rounded dyadic value, and the theorem substitutes the standard half-ulp bounds.

Packaged “dyadic quantization + IEEE rounding” theorem (1D, pointwise)

This is the “dyadic next step”: it replaces the abstract εQ premise of reluApproximationIccIEEE32Exec_threeTerm_bias with a concrete bound coming from:

• dyadic→FP32 rounding (≤ 1/2 ulp), and
• a Lipschitz-style sensitivity bound for the real hinge network on x ∈ [a,b].

It still assumes the IEEE finiteness witnesses for evaluation (HingeSumFinite + finite output).

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.reluApproximationIccIEEE32Exec_dyadicHalfUlp {f : ℝ → ℝ} {a b : ℝ} {hidDim : ℕ} (tD cD : Fin hidDim → FloatLib.Numerics.Dyadic) (bD : FloatLib.Numerics.Dyadic) (htIn : ∀ (i : Fin hidDim), TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal (tD i) ∈ Set.Icc a b) (htfin : ∀ (i : Fin hidDim), FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (tD i))) = true) (hcfin : ∀ (i : Fin hidDim), FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (cD i))) = true) (hbfin : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 bD)) = true) (εApprox : ℝ) : (∀ (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4), FloatLib.Floats.ExecFloat.Binary.isFinite x = true → (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b → HingeSumFinite (fun (i : Fin hidDim) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (tD i))) (fun (i : Fin hidDim) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (cD i))) x 0 (List.finRange hidDim) ∧ FloatLib.Floats.ExecFloat.Binary.isFinite (hingeFunIeee (fun (i : Fin hidDim) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (tD i))) (fun (i : Fin hidDim) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (cD i))) (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 bD)) x) = true) → (∀ (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4), FloatLib.Floats.ExecFloat.Binary.isFinite x = true → (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b → |f (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - hingeFun hidDim (fun (i : Fin hidDim) => TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal (tD i)) (fun (i : Fin hidDim) => TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal (cD i)) (TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal bD) (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal| < εApprox) → ∀ (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4), FloatLib.Floats.ExecFloat.Binary.isFinite x = true → (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b → |f (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel (hingeFunIeee (fun (i : Fin hidDim) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (tD i))) (fun (i : Fin hidDim) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (cD i))) (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 bD)) x)).toReal| < εApprox + (FloatLib.Floats.Formats.Flocq.ulp FloatLib.Numerics.binaryRadix TorchLean.Floats.fexp32 (TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal bD) / 2 + ∑ i : Fin hidDim, (FloatLib.Floats.Formats.Flocq.ulp FloatLib.Numerics.binaryRadix TorchLean.Floats.fexp32 (TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal (cD i)) / 2 * |b - a| + |(FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (cD i)))).toReal| * (FloatLib.Floats.Formats.Flocq.ulp FloatLib.Numerics.binaryRadix TorchLean.Floats.fexp32 (TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal (tD i)) / 2))) + hingeFunErrorBound (embedVec fun (i : Fin hidDim) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (tD i))) (embedVec fun (i : Fin hidDim) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (cD i))) (embed (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 bD))) (embed x)

theorem NN.MLTheory.Proofs.UniversalApproximation.IEEE32ExecReLUApprox.reluApproximationIccIEEE32Exec_twoTerm {f : ℝ → ℝ} {a b : ℝ} {hidDim : ℕ} (t c : Fin hidDim → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (b0 : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4) (ht : ∀ (i : Fin hidDim), FloatLib.Floats.ExecFloat.Binary.isFinite (t i) = true) (hc : ∀ (i : Fin hidDim), FloatLib.Floats.ExecFloat.Binary.isFinite (c i) = true) (εApprox : ℝ) : (∀ (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4), FloatLib.Floats.ExecFloat.Binary.isFinite x = true → (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b → HingeSumFinite t c x 0 (List.finRange hidDim) ∧ FloatLib.Floats.ExecFloat.Binary.isFinite (hingeFunIeee t c b0 x) = true) → (∀ (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4), FloatLib.Floats.ExecFloat.Binary.isFinite x = true → (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b → |f (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - hingeFun hidDim (fun (i : Fin hidDim) => (FloatLib.Floats.ExecFloat.Binary.toModel (t i)).toReal) (fun (i : Fin hidDim) => (FloatLib.Floats.ExecFloat.Binary.toModel (c i)).toReal) (FloatLib.Floats.ExecFloat.Binary.toModel b0).toReal (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal| < εApprox) → ∀ (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) embed._proof_1 embed._proof_2 embed._proof_3 embed._proof_4), FloatLib.Floats.ExecFloat.Binary.isFinite x = true → (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b → |f (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel (hingeFunIeee t c b0 x)).toReal| < εApprox + hingeFunErrorBound (embedVec t) (embedVec c) (embed b0) (embed x)

Two-term 1D IEEE32Exec ReLU approximation statement:

• assume the real hinge network built from the IEEE parameters’ toReal values already approximates f on toReal inputs in [a,b],
• and assume finiteness/no-NaN/no-Inf witnesses,
• then IEEE execution approximates f with an explicit IEEE rounding term.

This is a specialization of the 3-term theorem with εQ = 0.