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 ℝ 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. This keeps the architecture clean: 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)), mlpEval1d N l1 l2 (a + ↑↑k * ((b - a) / ↑N)) = y k

Exact interpolation on a uniform grid by a 2-layer ReLU MLP (over ℝ semantics).

Given arbitrary target values y₀,…,y_N at the uniform grid points 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

This section 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.

@[reducible, inline]

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

Alias for the “round-after-each-primitive” real-valued FP32 model (TorchLean.Floats.FP32).

def NN.MLTheory.Proofs.UniversalApproximation.extractScalarOutputFp32 (t : Spec.Tensor FP32 (Spec.Shape.dim 1 Spec.Shape.scalar)) : FP32

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

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.mlpEval1dFp32 (hidDim : ℕ) (l1 : Spec.LinearSpec FP32 1 hidDim) (l2 : Spec.LinearSpec FP32 hidDim 1) (x : FP32) : 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 : FP32) : FP32

Scalar ReLU on FP32. (No rounding: it is max x 0 at the FP32 level.)

@[simp]

theorem NN.MLTheory.Proofs.UniversalApproximation.fp32_zero_val : TorchLean.Floats.NF.val 0 = 0

@[simp]

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

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 → FP32) : Spec.LinearSpec FP32 1 n

First FP32 hinge layer: hidden unit i computes x - tᵢ before ReLU.

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

Second FP32 hinge layer: sum hidden activations with coefficients cᵢ and bias b.

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

One rounded hinge term cᵢ * reluFp32 (x - tᵢ) in the FP32 model.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.hingeTermReal {n : ℕ} (c t : Fin n → FP32) (x : 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 → FP32) (x : FP32) (i : Fin n) : have term32 := hingeTermFp32 c t x i; have termR := hingeTermReal c t x i; |term32.val - termR| ≤ TorchLean.Floats.neuralUlp TorchLean.Floats.binaryRadix TorchLean.Floats.fexp32 ((c i).val * (reluFp32 (x - t i)).val) / 2 + |(c i).val| * (TorchLean.Floats.neuralUlp TorchLean.Floats.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ᵢ|.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.hingeTermErrorBound {n : ℕ} (c t : Fin n → FP32) (x : 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 → FP32) (x : 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 → FP32) (x : 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 → FP32) (x : 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 → FP32) (x : FP32) : 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 → FP32) (x : FP32) : ℝ

Real reference sum accumulated alongside hingeSumFp32.

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

Accumulated certified absolute-error budget for hingeSumFp32.

theorem NN.MLTheory.Proofs.UniversalApproximation.hinge_sum_state_invariant_aux {n : ℕ} (c t : Fin n → FP32) (x : FP32) (xs : List (Fin n)) (acc32 : 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 → FP32) (x : 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 → FP32) (b x : FP32) : 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 → FP32) (b x : FP32) : ℝ

Real reference for hinge_fun_fp32: evaluate over ℝ on the .val parameters/inputs.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.hingeFunErrorBound {n : ℕ} (t c : Fin n → FP32) (b x : 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 → FP32) (b x : 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 → FP32) (b x : 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: it does not construct the approximating hinge parameters, it simply says that once a real hinge network is close to f, the rounded FP32 network is close up to the certified rounding budget.

theorem NN.MLTheory.Proofs.UniversalApproximation.hinge_fun_total_abs_error_lt {n : ℕ} (f : ℝ → ℝ) (t c : Fin n → FP32) (b x : 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 → FP32) (x : 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 → FP32) (c : Fin hidDim → FP32) (b0 : 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 hinge_fun_error_bound.