Exact ReLU interpolation and rounded-real approximation

The real interpolation theorem constructs a two-layer ReLU MLP matching arbitrary values on a uniform grid. RoundedReLUApprox then bounds each rounded hinge term, its ordered sum, and the final bias addition for an explicit FloatFormat, using FloatLib's half-ULP error theorem.

The scalar carrier is FloatLib's NF: its stored real value need not be representable, while arithmetic operations round to the selected precision and gradual-underflow grid. There is no upper exponent bound. The approximation theorem embeds exact real parameters and inputs in this carrier; parameter quantization and finite executable arithmetic require separate bounds.

theorem NN.MLTheory.Proofs.UniversalApproximation.relu_mlp_exact_on_uniform_grid {a b : ℝ} (h_ab : a < b) {N : ℕ} : 0 < N → ∀ (y : Fin (N + 1) → ℝ), ∃ (l1 : Spec.LinearSpec ℝ 1 N) (l2 : Spec.LinearSpec ℝ N 1), ∀ (k : Fin (N + 1)), mlpEvalScalar N l1 l2 (a + ↑↑k * ((b - a) / ↑N)) = y k

Exact interpolation on a uniform grid by a two-layer ReLU MLP over $\mathbb{R}$ semantics.

Given arbitrary target values $y_0,\ldots,y_N$ at the uniform grid points $\operatorname{grid}(k)=a+k(b-a)/N$, this constructs a width-$N$ hinge network that matches them at the grid points.

@[reducible, inline]

abbrev NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.Rounded (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) : Type

Real-valued scalars whose arithmetic rounds to the selected format's nearest-even grid. The stored value is unrestricted; NF.ofReal additionally rounds a real input.

@[simp]

theorem NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.rounded_zero_val (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) : FloatLib.Floats.Formats.Flocq.NF.val 0 = 0

The Rounded format zero denotes the real 0: rounding 0 is exact.

@[simp]

theorem NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.relu_rounded_val (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) (x : Rounded format) : (Activation.Math.reluSpec x).val = relu x.val

The Rounded format ReLU agrees with the real ReLU on the underlying value.

The Boolean zero test compares real values. A zero-valued input therefore returns a scalar whose value is zero, and the remaining branch selects the input or zero according to the same real order. Both cases give $\max(x.\mathrm{val},0)$ exactly, with no rounding error.

theorem NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.relu_lipschitz (u v : ℝ) : |relu u - relu v| ≤ |u - v|

Real ReLU is 1-Lipschitz.

The subtraction rounding error passes through the nonlinearity without amplification.

Rounded hinge terms and a pointwise error bound

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.hingeTerm (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) {n : ℕ} (c t : Fin n → Rounded format) (x : Rounded format) (i : Fin n) : Rounded format

One rounded hinge term $c_i\operatorname{ReLU}(x-t_i)$ in the rounded-real model.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.hingeTermReal (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) {n : ℕ} (c t : Fin n → Rounded format) (x : Rounded format) (i : Fin n) : ℝ

Real reference for the same hinge term, using the parameters’ real values.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.hingeTermErrorBound (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) {n : ℕ} (c t : Fin n → Rounded format) (x : Rounded format) (i : Fin n) : ℝ

Certified error budget for one rounded hinge term: a half-ulp for the final multiplication plus the subtraction rounding error, propagated through the 1-Lipschitz ReLU and scaled by |cᵢ|.

theorem NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.hinge_term_abs_error (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) {n : ℕ} (c t : Fin n → Rounded format) (x : Rounded format) (i : Fin n) : |(hingeTerm format c t x i).val - hingeTermReal format c t x i| ≤ hingeTermErrorBound format c t x i

Per-neuron rounded hinge-term error bound.

The bound has two pieces: one half-ulp term for the final multiplication and one subtraction rounding term propagated through the $1$-Lipschitz ReLU and scaled by $|c_i|$.

Summation error propagation (rounded hinge network)

@[reducible, inline]

abbrev NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.HingeSumState (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) : Type

Fold state for summing hinge terms in Rounded format, while tracking:

• a real reference sum (computed from .val),
• and a provable error bound on the difference between them.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.hingeSumStateStep (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) {n : ℕ} (c t : Fin n → Rounded format) (x : Rounded format) : HingeSumState format → Fin n → HingeSumState format

One summation step: add a hinge term, and accumulate rounding+term error bounds.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.hingeSumState (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) {n : ℕ} (c t : Fin n → Rounded format) (x : Rounded format) : HingeSumState format

Compute the hinge-term sum state in ascending index order.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.hingeSum (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) {n : ℕ} (c t : Fin n → Rounded format) (x : Rounded format) : Rounded format

Rounded value produced by folding all hinge terms in ascending index order.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.hingeSumReal (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) {n : ℕ} (c t : Fin n → Rounded format) (x : Rounded format) : ℝ

Real reference sum accumulated alongside hingeSum.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.hingeSumErrorBound (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) {n : ℕ} (c t : Fin n → Rounded format) (x : Rounded format) : ℝ

Accumulated certified absolute-error budget for hingeSum.

theorem NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.hinge_sum_state_invariant (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) {n : ℕ} (c t : Fin n → Rounded format) (x : Rounded format) (xs : List (Fin n)) (accQ : Rounded format) (accR err : ℝ) : |accQ.val - accR| ≤ err → have st := List.foldl (hingeSumStateStep format c t x) (accQ, accR, err) xs; |st.1.val - st.2.1| ≤ st.2.2

Fold invariant for rounded hinge summation.

At every prefix of the fold, the rounded accumulator is within the tracked error budget of the real accumulator. The proof is deliberately order-sensitive because floating-point addition is not associative.

theorem NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.hinge_sum_abs_error (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) {n : ℕ} (c t : Fin n → Rounded format) (x : Rounded format) : |(hingeSum format c t x).val - hingeSumReal format c t x| ≤ hingeSumErrorBound format c t x

Certified absolute-error bound for the whole rounded hinge-term sum.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.hingeFun (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) {n : ℕ} (t c : Fin n → Rounded format) (b x : Rounded format) : Rounded format

Rounded hinge-network output: sum of hinge terms, then add the bias.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.hingeFunReal (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) {n : ℕ} (t c : Fin n → Rounded format) (b x : Rounded format) : ℝ

Real reference for hingeFun: evaluate over $\mathbb{R}$ on the .val parameters and inputs.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.hingeFunErrorBound (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) {n : ℕ} (t c : Fin n → Rounded format) (b x : Rounded format) : ℝ

Total rounded hinge-network error budget, including the final rounded bias addition.

theorem NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.hinge_fun_abs_error (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) {n : ℕ} (t c : Fin n → Rounded format) (b x : Rounded format) : |(hingeFun format t c b x).val - hingeFunReal format t c b x| ≤ hingeFunErrorBound format t c b x

Certified absolute-error bound for the complete rounded hinge network.

This composes the fold invariant with the final rounded bias addition.

Real approximation + rounding combination (pointwise)

theorem NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.hinge_fun_total_abs_error_le (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) {n : ℕ} (f : ℝ → ℝ) (t c : Fin n → Rounded format) (b x : Rounded format) : |f x.val - (hingeFun format t c b x).val| ≤ |f x.val - hingeFunReal format t c b x| + hingeFunErrorBound format t c b x

Triangle bound combining real approximation error with arithmetic rounding error.

The theorem is pointwise. Given a real hinge network close to f, it bounds the rounded-real network by the real approximation error plus the certified rounding budget; it does not construct the hinge parameters.

theorem NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.hinge_fun_total_abs_error_lt (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) {n : ℕ} (f : ℝ → ℝ) (t c : Fin n → Rounded format) (b x : Rounded format) {ε : ℝ} (hε : |f x.val - hingeFunReal format t c b x| < ε) : |f x.val - (hingeFun format t c b x).val| < ε + hingeFunErrorBound format t c b x

Strict version of hinge_fun_total_abs_error_le for use with < ε approximation statements.

theorem NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.hinge_sum_real_eq_sum (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) {n : ℕ} (c t : Fin n → Rounded format) (x : Rounded format) : hingeSumReal format c t x = ∑ i : Fin n, hingeTermReal format c t x i

The real reference accumulator is the ordinary finite sum of real hinge terms.

theorem NN.MLTheory.Proofs.UniversalApproximation.RoundedReLUApprox.relu_universal_approximation_Icc (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) {f : ℝ → ℝ} {a b L : ℝ} (h_ab : a < b) (hL : 0 < L) (h_lip : ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc a b, |f x - f y| ≤ L * |x - y|) (ε : ℝ) : ε > 0 → ∃ (hidDim : ℕ) (t : Fin hidDim → Rounded format) (c : Fin hidDim → Rounded format) (b0 : Rounded format), ∀ x ∈ Set.Icc a b, |f x - (hingeFun format t c b0 { val := x }).val| < ε + hingeFunErrorBound format t c b0 { val := x }

One-dimensional ReLU approximation with a pointwise rounding budget for any FloatFormat.

The real hinge construction supplies exact real parameters, embedded in Rounded format without quantization. Each arithmetic operation rounds to the chosen grid. Thus the bound combines the real approximation error with hingeFunErrorBound; it does not assert representability of the parameters or inputs, or finiteness of a corresponding executable computation.