Executable ReLU approximation for configured IEEE formats

hingeFunBinary evaluates a hinge network with a configured FloatFormat, storage plan, and ModelCodec. Refinement to RoundedReLUApprox requires format.isIEEE = true and finite intermediates. The result preserves the exact fold order and combines real approximation, parameter quantization, and arithmetic rounding error.

HingeSumFinite records the finite intermediates. HingeSumBounds supplies sufficient bounds on exact subtractions, products, and partial sums to establish that witness through FloatLib's range theorems. Dyadic quantization bounds use the selected format's rounding and half-ulp API.

Embedding configured binary values into the rounded-real model

@[inline]

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.embed {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] (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) : RoundedReLUApprox.Rounded format

Read an executable configured IEEE value as a point of the rounded-real model.

@[simp]

theorem NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.embed_val {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] (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) : (embed x).val = (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal

@[inline]

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.embedVec {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 : ℕ} (v : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) : Fin n → RoundedReLUApprox.Rounded format

Pointwise embedding of a vector of Value values into the rounded-real model.

Configured binary hinge network (same shape as RoundedReLUApprox.hingeFun format)

@[inline]

def NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.reluBinary {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] (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)

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.BinaryExecReLUApprox.hingeTermBinary {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 : ℕ} (c t : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (i : Fin n) : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)

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

@[inline]

def NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.hingeSumStepBinary {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 : ℕ} (c t : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan) → Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)

Fold step for summing hinge terms, used by hingeSumBinary.

def NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.hingeSumBinary {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 : ℕ} (c t : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)

Executable configured binary sum of hinge terms, in ascending index order.

def NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.hingeFunBinary {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 : ℕ} (t c : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (b x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)

Executable configured binary 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.BinaryExecReLUApprox.HingeSumFinite {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 : ℕ} (t c : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan) → 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 the instance instDecHingeSumFinite.

• nil {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 : ℕ} {t c : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)} {x acc : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)} (hacc : FloatLib.Floats.ExecFloat.Binary.isFinite acc = true) : HingeSumFinite t c x acc []
• cons {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 : ℕ} {t c : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)} {x acc : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)} {i : Fin n} {xs : List (Fin n)} (hsub : FloatLib.Floats.ExecFloat.Binary.isFinite (x.sub (t i)) = true) (hmax : (x.sub (t i) ⊔ 0).isFinite = true) (hmul : FloatLib.Floats.ExecFloat.Binary.isFinite (hingeTermBinary c t x i) = true) (hadd : FloatLib.Floats.ExecFloat.Binary.isFinite (acc.add (hingeTermBinary c t x i)) = true) (hrest : HingeSumFinite t c x (acc.add (hingeTermBinary 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 configured binary constants coming from a lowered model artifact. In that setting, the easiest way to satisfy the HingeSumFinite … hypotheses is to compute the configured binary kernel and check finiteness at every intermediate.

instDecHingeSumFinite is a Decidable instance for HingeSumFinite … that walks the fold, so a true concrete instance closes by computation:

  have hSum : HingeSumFinite t c x (0 : Value) (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.

@[instance_reducible]

instance NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.instDecHingeSumFinite {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 : ℕ} (t c : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (x acc : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (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.BinaryExecReLUApprox.HingeEvalFiniteProp {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 : ℕ} (t c : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (b x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) : Prop

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

Sufficient range bounds for finite intermediates

inductive NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.HingeSumBounds {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 : ℕ} (t c : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan) → List (Fin n) → Prop

Exact arithmetic bounds along the executable fold. Each bound compares the unrounded operation with the selected format's largest finite value.

• nil {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 : ℕ} {t c : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)} {x acc : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)} : HingeSumBounds t c x acc []
• cons {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 : ℕ} {t c : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)} {x acc : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)} {i : Fin n} {xs : List (Fin n)} (hsub : |(FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel (t i)).toReal| ≤ (FloatLib.Floats.Formats.BinaryInterchange.Model.posMaxFinite format).toReal) (hmul : |(FloatLib.Floats.ExecFloat.Binary.toModel (c i)).toReal| * |(FloatLib.Floats.ExecFloat.Binary.toModel (reluBinary (x.sub (t i)))).toReal| ≤ (FloatLib.Floats.Formats.BinaryInterchange.Model.posMaxFinite format).toReal) (hadd : |(FloatLib.Floats.ExecFloat.Binary.toModel acc).toReal + (FloatLib.Floats.ExecFloat.Binary.toModel (hingeTermBinary c t x i)).toReal| ≤ (FloatLib.Floats.Formats.BinaryInterchange.Model.posMaxFinite format).toReal) (hrest : HingeSumBounds t c x (acc.add (hingeTermBinary c t x i)) xs) : HingeSumBounds t c x acc (i :: xs)

theorem NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.hinge_sum_finite_of_bounds {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] (hformat : format.isIEEE = true) {n : ℕ} {t c : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)} {x acc : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)} {xs : List (Fin n)} (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) (hbound : HingeSumBounds t c x acc xs) : FloatLib.Floats.ExecFloat.Binary.isFinite acc = true → HingeSumFinite t c x acc xs

Bounds on each exact subtraction, product, and partial sum rule out exceptional intermediates, starting from finite inputs, parameters, and accumulator.

theorem NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.HingeSumFinite.isFinite_fold {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 : ℕ} {t c : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)} {x acc : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)} {xs : List (Fin n)} (h : HingeSumFinite t c x acc xs) : (List.foldl (hingeSumStepBinary c t x) acc xs).isFinite = true

A finite-fold witness guarantees that its final accumulator is finite.

theorem NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.hinge_eval_finite_of_bounds {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] (hformat : format.isIEEE = true) {n : ℕ} {t c : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)} {b x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)} (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) (hb : FloatLib.Floats.ExecFloat.Binary.isFinite b = true) (hbound : HingeSumBounds t c x 0 (List.finRange n)) (hout : |(FloatLib.Floats.ExecFloat.Binary.toModel (hingeSumBinary c t x)).toReal + (FloatLib.Floats.ExecFloat.Binary.toModel b).toReal| ≤ (FloatLib.Floats.Formats.BinaryInterchange.Model.posMaxFinite format).toReal) : HingeEvalFiniteProp t c b x

Range bounds on the fold and final bias addition discharge the complete execution witness.

Refinement to rounded-real execution

theorem NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.toReal_hinge_sum_binary_eq_rounded_val {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] (hformat : format.isIEEE = true) {n : ℕ} (t c : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) {acc : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)} {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) : (List.foldl (hingeSumStepBinary c t x) acc xs).toModel.toReal = (List.foldl (fun (accRounded : RoundedReLUApprox.Rounded format) (i : Fin n) => accRounded + RoundedReLUApprox.hingeTerm format (embedVec c) (embedVec t) (embed x) i) (embed acc) xs).val

Refine an executable hinge-term fold to the rounded-real 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.BinaryExecReLUApprox.toReal_hinge_fun_binary_eq_rounded_val {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] (hformat : format.isIEEE = true) {n : ℕ} (t c : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (b x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (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 (hingeFunBinary t c b x) = true) : (FloatLib.Floats.ExecFloat.Binary.toModel (hingeFunBinary t c b x)).toReal = (RoundedReLUApprox.hingeFun format (embedVec t) (embedVec c) (embed b) (embed x)).val

Refine the whole executable hinge network to the rounded-real 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.

Configured binary error bound inherited from the rounded-real bound

theorem NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.hinge_fun_binary_abs_error_le {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] (hformat : format.isIEEE = true) {n : ℕ} (t c : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (b x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (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 (hingeFunBinary t c b x) = true) : |(FloatLib.Floats.ExecFloat.Binary.toModel (hingeFunBinary t c b x)).toReal - RoundedReLUApprox.hingeFunReal format (embedVec t) (embedVec c) (embed b) (embed x)| ≤ RoundedReLUApprox.hingeFunErrorBound format (embedVec t) (embedVec c) (embed b) (embed x)

Lift the rounded-real hinge-network error bound to executable evaluation.

The refinement toReal_hinge_fun_binary_eq_rounded_val identifies the executable result with the rounded-real model, so its error bound transfers directly.

“Approximation error + rounding error” (pointwise)

theorem NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.hinge_fun_total_abs_error_binary_le {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] (hformat : format.isIEEE = true) {n : ℕ} (f : ℝ → ℝ) (t c : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (b x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (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 (hingeFunBinary t c b x) = true) : |f (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel (hingeFunBinary t c b x)).toReal| ≤ |f (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - RoundedReLUApprox.hingeFunReal format (embedVec t) (embedVec c) (embed b) (embed x)| + RoundedReLUApprox.hingeFunErrorBound format (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 IEEE arithmetic rounding error.

theorem NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.hinge_fun_total_abs_error_binary_lt {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] (hformat : format.isIEEE = true) {n : ℕ} (f : ℝ → ℝ) (t c : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (b x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (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 (hingeFunBinary t c b x) = true) {ε : ℝ} (hε : |f (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - RoundedReLUApprox.hingeFunReal format (embedVec t) (embedVec c) (embed b) (embed x)| < ε) : |f (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel (hingeFunBinary t c b x)).toReal| < ε + RoundedReLUApprox.hingeFunErrorBound format (embedVec t) (embedVec c) (embed b) (embed x)

Strict version of hinge_fun_total_abs_error_binary_le, useful for approximation theorems.

Configured binary pointwise ReLU approximation packaging (1D)

theorem NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.relu_approximation_Icc_binary_of_hinge {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] (hformat : format.isIEEE = true) {f : ℝ → ℝ} {a b : ℝ} (ε : ℝ) : ε > 0 → (∃ (hidDim : ℕ) (t : Fin hidDim → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (c : Fin hidDim → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (b0 : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)), (∀ (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 (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)), 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 (hingeFunBinary t c b0 x) = true) ∧ ∀ (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)), 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 - RoundedReLUApprox.hingeFunReal format (embedVec t) (embedVec c) (embed b0) (embed x)| < ε) → ∃ (hidDim : ℕ) (t : Fin hidDim → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (c : Fin hidDim → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (b0 : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)), ∀ (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)), 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 (hingeFunBinary t c b0 x)).toReal| < ε + RoundedReLUApprox.hingeFunErrorBound format (embedVec t) (embedVec c) (embed b0) (embed x)

1D ReLU approximation statement over configured binary 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_binary_lt into an existence/for-all form:

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

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

theorem NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.relu_approximation_Icc_binary_three_term_bias {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] (hformat : format.isIEEE = true) {f : ℝ → ℝ} {a b : ℝ} {hidDim : ℕ} (bR : ℝ) (tR cR : Fin hidDim → ℝ) (t c : Fin hidDim → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (b0 : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (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 (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)), 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 (hingeFunBinary t c b0 x) = true) → (∀ (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)), 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 (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)), 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 - RoundedReLUApprox.hingeFunReal format (embedVec t) (embedVec c) (embed b0) (embed x)| ≤ εQ) → ∀ (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)), 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 (hingeFunBinary t c b0 x)).toReal| < εApprox + εQ + RoundedReLUApprox.hingeFunErrorBound format (embedVec t) (embedVec c) (embed b0) (embed x)

1D configured binary ReLU approximation with an explicit 3-term error decomposition, relative to a caller-supplied real reference bias bR:

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 format.

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

• construct configured binary 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.

theorem NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.relu_approximation_Icc_binary_three_term {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] (hformat : format.isIEEE = true) {f : ℝ → ℝ} {a b : ℝ} {hidDim : ℕ} (tR cR : Fin hidDim → ℝ) (t c : Fin hidDim → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (b0 : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (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 (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)), 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 (hingeFunBinary t c b0 x) = true) → (∀ (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)), 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 (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)), 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 - RoundedReLUApprox.hingeFunReal format (embedVec t) (embedVec c) (embed b0) (embed x)| ≤ εQ) → ∀ (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)), 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 (hingeFunBinary t c b0 x)).toReal| < εApprox + εQ + RoundedReLUApprox.hingeFunErrorBound format (embedVec t) (embedVec c) (embed b0) (embed x)

Specialization of relu_approximation_Icc_binary_three_term_bias to the real bias f a, which is the bias the constructive one-dimensional interpolation theorem emits.

Dyadic quantization helpers

theorem NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.abs_toReal_roundDyadic_sub_le_half_ulp {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] (hformat : format.isIEEE = true) (d : FloatLib.Numerics.Dyadic) (hfin : (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format d)).isFinite = true) : |(FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format d)).toModel.toReal - d.toReal| ≤ FloatLib.Floats.Formats.Flocq.ulp FloatLib.Numerics.binaryRadix (FloatLib.Floats.Formats.BinaryInterchange.Model.fexpOf format) d.toReal / 2

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

The finiteness hypothesis excludes overflow/NaN paths, after which the executable rounding of a dyadic agrees with the real Model.roundAt format operation used by the rounded-real model, and FloatLib's local rounding bound Model.abs_roundAt_sub_le applies.

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

This is the “εQ quantization” step for relu_approximation_Icc_binary_three_term. 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.BinaryExecReLUApprox.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.BinaryExecReLUApprox.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.BinaryExecReLUApprox.hinge_fun_real_embed_eq_hinge_fun_toReal {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 : ℕ} (t c : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (b x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) : RoundedReLUApprox.hingeFunReal format (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 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.BinaryExecReLUApprox.hinge_fun_quantization_error_le_Icc_uniform {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 : ℕ} {a b : ℝ} (tR cR : Fin n → ℝ) (bR : ℝ) (t c : Fin n → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (b0 x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (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 - RoundedReLUApprox.hingeFunReal format (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-configured binary quantization bound (εQ)

This lemma is a drop-in way to discharge the εQ premise of relu_approximation_Icc_binary_three_term when IEEE parameters are obtained by rounding dyadic rationals with Model.roundDyadic format.

theorem NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.hinge_fun_dyadic_quantization_error_le_Icc {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 : ℕ} {a b : ℝ} (tD cD : Fin n → FloatLib.Numerics.Dyadic) (bD : FloatLib.Numerics.Dyadic) (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (hxIn : (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b) (htIn : ∀ (i : Fin n), (tD i).toReal ∈ Set.Icc a b) : |hingeFun n (fun (i : Fin n) => (tD i).toReal) (fun (i : Fin n) => (cD i).toReal) bD.toReal (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - RoundedReLUApprox.hingeFunReal format (embedVec fun (i : Fin n) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format (tD i))) (embedVec fun (i : Fin n) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format (cD i))) (embed (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format bD))) (embed x)| ≤ |bD.toReal - (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format bD)).toModel.toReal| + ∑ i : Fin n, (|(cD i).toReal - (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format (cD i))).toModel.toReal| * |b - a| + |(FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format (cD i))).toModel.toReal| * |(tD i).toReal - (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format (tD i))).toModel.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 configured binary values. The result is still expressed as a sum of concrete per-parameter rounding errors.

theorem NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.hinge_fun_dyadic_quantization_error_le_Icc_half_ulp {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] (hformat : format.isIEEE = true) {n : ℕ} {a b : ℝ} (tD cD : Fin n → FloatLib.Numerics.Dyadic) (bD : FloatLib.Numerics.Dyadic) (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (hxIn : (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal ∈ Set.Icc a b) (htIn : ∀ (i : Fin n), (tD i).toReal ∈ Set.Icc a b) (htfin : ∀ (i : Fin n), (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format (tD i))).isFinite = true) (hcfin : ∀ (i : Fin n), (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format (cD i))).isFinite = true) (hbfin : (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format bD)).isFinite = true) : |hingeFun n (fun (i : Fin n) => (tD i).toReal) (fun (i : Fin n) => (cD i).toReal) bD.toReal (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - RoundedReLUApprox.hingeFunReal format (embedVec fun (i : Fin n) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format (tD i))) (embedVec fun (i : Fin n) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format (cD i))) (embed (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format bD))) (embed x)| ≤ FloatLib.Floats.Formats.Flocq.ulp FloatLib.Numerics.binaryRadix (FloatLib.Floats.Formats.BinaryInterchange.Model.fexpOf format) bD.toReal / 2 + ∑ i : Fin n, (FloatLib.Floats.Formats.Flocq.ulp FloatLib.Numerics.binaryRadix (FloatLib.Floats.Formats.BinaryInterchange.Model.fexpOf format) (cD i).toReal / 2 * |b - a| + |(FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format (cD i))).toModel.toReal| * (FloatLib.Floats.Formats.Flocq.ulp FloatLib.Numerics.binaryRadix (FloatLib.Floats.Formats.BinaryInterchange.Model.fexpOf format) (tD i).toReal / 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 relu_approximation_Icc_binary_three_term_bias with a concrete bound coming from:

• dyadic→arithmetic 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.BinaryExecReLUApprox.relu_approximation_Icc_binary_dyadic_half_ulp {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] (hformat : format.isIEEE = true) {f : ℝ → ℝ} {a b : ℝ} {hidDim : ℕ} (tD cD : Fin hidDim → FloatLib.Numerics.Dyadic) (bD : FloatLib.Numerics.Dyadic) (htIn : ∀ (i : Fin hidDim), (tD i).toReal ∈ Set.Icc a b) (htfin : ∀ (i : Fin hidDim), (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format (tD i))).isFinite = true) (hcfin : ∀ (i : Fin hidDim), (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format (cD i))).isFinite = true) (hbfin : (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format bD)).isFinite = true) (εApprox : ℝ) : (∀ (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)), 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 format (tD i))) (fun (i : Fin hidDim) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format (cD i))) x 0 (List.finRange hidDim) ∧ FloatLib.Floats.ExecFloat.Binary.isFinite (hingeFunBinary (fun (i : Fin hidDim) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format (tD i))) (fun (i : Fin hidDim) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format (cD i))) (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format bD)) x) = true) → (∀ (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)), 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) => (tD i).toReal) (fun (i : Fin hidDim) => (cD i).toReal) bD.toReal (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal| < εApprox) → ∀ (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)), 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 (hingeFunBinary (fun (i : Fin hidDim) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format (tD i))) (fun (i : Fin hidDim) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format (cD i))) (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format bD)) x)).toReal| < εApprox + (FloatLib.Floats.Formats.Flocq.ulp FloatLib.Numerics.binaryRadix (FloatLib.Floats.Formats.BinaryInterchange.Model.fexpOf format) bD.toReal / 2 + ∑ i : Fin hidDim, (FloatLib.Floats.Formats.Flocq.ulp FloatLib.Numerics.binaryRadix (FloatLib.Floats.Formats.BinaryInterchange.Model.fexpOf format) (cD i).toReal / 2 * |b - a| + |(FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format (cD i))).toModel.toReal| * (FloatLib.Floats.Formats.Flocq.ulp FloatLib.Numerics.binaryRadix (FloatLib.Floats.Formats.BinaryInterchange.Model.fexpOf format) (tD i).toReal / 2))) + RoundedReLUApprox.hingeFunErrorBound format (embedVec fun (i : Fin hidDim) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format (tD i))) (embedVec fun (i : Fin hidDim) => FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format (cD i))) (embed (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format bD))) (embed x)

Three-term configured binary approximation bound with the quantization term instantiated by the half-ulp dyadic rounding budget of hinge_fun_dyadic_quantization_error_le_Icc_half_ulp.

theorem NN.MLTheory.Proofs.UniversalApproximation.BinaryExecReLUApprox.relu_approximation_Icc_binary_two_term {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] (hformat : format.isIEEE = true) {f : ℝ → ℝ} {a b : ℝ} {hidDim : ℕ} (t c : Fin hidDim → FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (b0 : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (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 (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)), 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 (hingeFunBinary t c b0 x) = true) → (∀ (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)), 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 (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)), 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 (hingeFunBinary t c b0 x)).toReal| < εApprox + RoundedReLUApprox.hingeFunErrorBound format (embedVec t) (embedVec c) (embed b0) (embed x)

Two-term 1D configured binary 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.