Exact ReLU interpolation and FP32 error lifting

This file has two jobs.

First, it proves an exact interpolation lemma on a uniform grid: given arbitrary target values at the grid points, we construct a two-layer ReLU MLP that matches those values exactly under the ideal $\mathbb{R}$ semantics. This is the familiar hinge-basis construction behind one-dimensional piecewise-linear approximation; see Pinkus for the approximation-theory background and Yarotsky for quantitative ReLU-network rates.

Second, it states the FP32 lifting layer: once a real construction is fixed, explicit rounding-error bounds turn it into an FP32 approximation theorem. Real approximation, parameter rounding, and executable IEEE semantics are proved in separate modules, matching the numerical-analysis separation used in Goldberg and Higham.

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.

FP32 (rounding-on-ℝ) error propagation for the hinge construction

The theorem below does not claim that FP32 is equivalent to hardware float32. It proves a pointwise bound for evaluating the same hinge network with rounded operations (TorchLean.Floats.FP32) versus exact real arithmetic on the rounded inputs/weights.

def NN.MLTheory.Proofs.UniversalApproximation.extractScalarOutputFp32 (t : TorchLean.Tensor TorchLean.Floats.FP32 [1]) : TorchLean.Floats.FP32

Extract scalar from a length-1 tensor (FP32).

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.mlpEvalScalarFP32 (hidDim : ℕ) (l1 : Spec.LinearSpec TorchLean.Floats.FP32 1 hidDim) (l2 : Spec.LinearSpec TorchLean.Floats.FP32 hidDim 1) (x : TorchLean.Floats.FP32) : TorchLean.Floats.FP32

Evaluate a 2-layer ReLU MLP on a scalar FP32 input (returns an FP32 scalar).

@[inline]

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.reluFp32 (x : TorchLean.Floats.FP32) : TorchLean.Floats.FP32

Scalar ReLU on the rounded-real FP32 model.

The zero branch returns scalar zero; otherwise the maximum selects the input or scalar zero. Neither branch performs an additional rounding operation.

@[simp]

theorem NN.MLTheory.Proofs.UniversalApproximation.fp32_zero_val : FloatLib.Floats.Formats.Flocq.NF.val 0 = 0

@[simp]

theorem NN.MLTheory.Proofs.UniversalApproximation.relu_fp32_val (x : TorchLean.Floats.FP32) : (reluFp32 x).val = relu x.val

The FP32 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.relu_lipschitz (u v : ℝ) : |relu u - relu v| ≤ |u - v|

Real ReLU is 1-Lipschitz.

This elementary analytic fact is what lets the FP32 error analysis pass a subtraction-rounding error through the ReLU nonlinearity without amplifying it.

FP32 hinge layers and a pointwise error bound

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.hingeLayer1Fp32 (n : ℕ) (t : Fin n → TorchLean.Floats.FP32) : Spec.LinearSpec TorchLean.Floats.FP32 1 n

First FP32 hinge layer: hidden unit $i$ computes $x-t_i$ before ReLU.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.hingeLayer2Fp32 (n : ℕ) (c : Fin n → TorchLean.Floats.FP32) (b : TorchLean.Floats.FP32) : Spec.LinearSpec TorchLean.Floats.FP32 n 1

Second FP32 hinge layer: sum hidden activations with coefficients $c_i$ and bias $b$.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.hingeTermFp32 {n : ℕ} (c t : Fin n → TorchLean.Floats.FP32) (x : TorchLean.Floats.FP32) (i : Fin n) : TorchLean.Floats.FP32

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

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.hingeTermReal {n : ℕ} (c t : Fin n → TorchLean.Floats.FP32) (x : TorchLean.Floats.FP32) (i : Fin n) : ℝ

Real reference for the same hinge term, using the .val denotation of FP32 parameters.

theorem NN.MLTheory.Proofs.UniversalApproximation.hinge_term_abs_error {n : ℕ} (c t : Fin n → TorchLean.Floats.FP32) (x : TorchLean.Floats.FP32) (i : Fin n) : have term32 := hingeTermFp32 c t x i; have termR := hingeTermReal c t x i; |term32.val - termR| ≤ FloatLib.Floats.Formats.Flocq.ulp FloatLib.Numerics.binaryRadix TorchLean.Floats.fexp32 ((c i).val * (reluFp32 (x - t i)).val) / 2 + |(c i).val| * (FloatLib.Floats.Formats.Flocq.ulp FloatLib.Numerics.binaryRadix TorchLean.Floats.fexp32 (x.val - (t i).val) / 2)

Per-neuron FP32 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|$.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.hingeTermErrorBound {n : ℕ} (c t : Fin n → TorchLean.Floats.FP32) (x : TorchLean.Floats.FP32) (i : Fin n) : ℝ

The per-hinge error bound used by hinge_term_abs_error.

@[simp]

theorem NN.MLTheory.Proofs.UniversalApproximation.hinge_term_abs_error' {n : ℕ} (c t : Fin n → TorchLean.Floats.FP32) (x : TorchLean.Floats.FP32) (i : Fin n) : |(hingeTermFp32 c t x i).val - hingeTermReal c t x i| ≤ hingeTermErrorBound c t x i

Named version of hinge_term_abs_error using hingeTermErrorBound.

Summation error propagation (FP32 hinge network)

@[reducible, inline]

abbrev NN.MLTheory.Proofs.UniversalApproximation.HingeSumState : Type

Fold state for summing hinge terms in FP32, 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.hingeSumStateStep {n : ℕ} (c t : Fin n → TorchLean.Floats.FP32) (x : TorchLean.Floats.FP32) : HingeSumState → Fin n → HingeSumState

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

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.hingeSumState {n : ℕ} (c t : Fin n → TorchLean.Floats.FP32) (x : TorchLean.Floats.FP32) : HingeSumState

Compute the hinge-term sum state over all Fin n in a fixed order (List.finRange).

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.hingeSumFp32 {n : ℕ} (c t : Fin n → TorchLean.Floats.FP32) (x : TorchLean.Floats.FP32) : TorchLean.Floats.FP32

FP32 value produced by folding all hinge terms in the fixed List.finRange order.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.hingeSumReal {n : ℕ} (c t : Fin n → TorchLean.Floats.FP32) (x : TorchLean.Floats.FP32) : ℝ

Real reference sum accumulated alongside hingeSumFp32.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.hingeSumErrorBound {n : ℕ} (c t : Fin n → TorchLean.Floats.FP32) (x : TorchLean.Floats.FP32) : ℝ

Accumulated certified absolute-error budget for hingeSumFp32.

theorem NN.MLTheory.Proofs.UniversalApproximation.hinge_sum_state_invariant_aux {n : ℕ} (c t : Fin n → TorchLean.Floats.FP32) (x : TorchLean.Floats.FP32) (xs : List (Fin n)) (acc32 : TorchLean.Floats.FP32) (accR err : ℝ) : |acc32.val - accR| ≤ err → have st := List.foldl (hingeSumStateStep c t x) (acc32, accR, err) xs; |st.1.val - st.2.1| ≤ st.2.2

Fold invariant for FP32 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.hinge_sum_abs_error {n : ℕ} (c t : Fin n → TorchLean.Floats.FP32) (x : TorchLean.Floats.FP32) : |(hingeSumFp32 c t x).val - hingeSumReal c t x| ≤ hingeSumErrorBound c t x

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

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.hingeFunFp32 {n : ℕ} (t c : Fin n → TorchLean.Floats.FP32) (b x : TorchLean.Floats.FP32) : TorchLean.Floats.FP32

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

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.hingeFunReal {n : ℕ} (t c : Fin n → TorchLean.Floats.FP32) (b x : TorchLean.Floats.FP32) : ℝ

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

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.hingeFunErrorBound {n : ℕ} (t c : Fin n → TorchLean.Floats.FP32) (b x : TorchLean.Floats.FP32) : ℝ

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

theorem NN.MLTheory.Proofs.UniversalApproximation.hinge_fun_abs_error {n : ℕ} (t c : Fin n → TorchLean.Floats.FP32) (b x : TorchLean.Floats.FP32) : |(hingeFunFp32 t c b x).val - hingeFunReal t c b x| ≤ hingeFunErrorBound t c b x

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

This composes the fold invariant with the final rounded + b, giving the main FP32 rounding term used by the executable approximation theorems.

Real approximation + rounding combination (pointwise)

theorem NN.MLTheory.Proofs.UniversalApproximation.hinge_fun_total_abs_error_le {n : ℕ} (f : ℝ → ℝ) (t c : Fin n → TorchLean.Floats.FP32) (b x : TorchLean.Floats.FP32) : |f x.val - (hingeFunFp32 t c b x).val| ≤ |f x.val - hingeFunReal t c b x| + hingeFunErrorBound t c b x

Triangle bound combining real approximation error with FP32 rounding error.

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

theorem NN.MLTheory.Proofs.UniversalApproximation.hinge_fun_total_abs_error_lt {n : ℕ} (f : ℝ → ℝ) (t c : Fin n → TorchLean.Floats.FP32) (b x : TorchLean.Floats.FP32) {ε : ℝ} (hε : |f x.val - hingeFunReal t c b x| < ε) : |f x.val - (hingeFunFp32 t c b x).val| < ε + hingeFunErrorBound t c b x

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

theorem NN.MLTheory.Proofs.UniversalApproximation.hinge_sum_real_eq_sum {n : ℕ} (c t : Fin n → TorchLean.Floats.FP32) (x : TorchLean.Floats.FP32) : hingeSumReal c t x = ∑ i : Fin n, hingeTermReal c t x i

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

theorem NN.MLTheory.Proofs.UniversalApproximation.relu_universal_approximation_Icc_fp32 {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 → TorchLean.Floats.FP32) (c : Fin hidDim → TorchLean.Floats.FP32) (b0 : TorchLean.Floats.FP32), ∀ x ∈ Set.Icc a b, |f x - (hingeFunFp32 t c b0 { val := x }).val| < ε + hingeFunErrorBound t c b0 { val := x }

1D ReLU approximation with a pointwise FP32 rounding bound.

This combines:

• the constructive real-valued hinge-network approximation theorem (relu_universal_approximation_Icc_hinge), and
• the FP32 hinge-network rounding bound (hinge_fun_total_abs_error_lt).

The output network is evaluated on the FP32 model (NF rounding-on-ℝ); the additional rounding error is given by hingeFunErrorBound.