6.8. Approximation Theory
Suppose we want a ReLU network to represent a function f on an interval. An approximation
theorem may tell us that suitable weights exist. Once we choose weights, a verifier can try to
enclose that particular network's values on an input box. To say what its binary32 execution
does, we also need to account for rounding. The quantifiers show why these are separate claims:
\begin{aligned}
\text{representation:}\quad&
\forall f\,\forall\varepsilon>0\,\exists\theta\,
\sup_{x\in K}|N_\theta(x)-f(x)|<\varepsilon,\\
\text{verification:}\quad&
\forall x\in B,\quad N_\theta(x)\in\mathcal A_\theta(B),\\
\text{execution:}\quad&
\forall x\in B,\quad
|N_{\theta,\mathrm{run}}(x)-N_{\theta,\mathbb R}(x)|\leq\delta(x).
\end{aligned}
Only the first line is universal approximation. It does not certify a trained checkpoint, choose the parameters for an optimizer, or prove that floating-point evaluation is close to the real network. TorchLean keeps these statements near one another because they eventually need to be composed, but it does not identify them.
The position of \exists\theta is doing real work. We choose the target and tolerance first,
then obtain one parameter vector that works for every input in the domain. Moving the existential
inside the final input quantifier would permit a different network at every point, which would
say very little about representation. For a trained model, by contrast, the parameters have
already been fixed. The useful question becomes whether those parameters satisfy an approximation
bound, or whether their outputs stay in an acceptable range. This is why a theorem about the
network family and a certificate for one checkpoint can both be useful without answering the
same question.
ReLU Hinge Approximation
The one-dimensional construction is easier to understand in hinge notation. Let
H(x)=b_0+\sum_{i=0}^{N-1} c_i\,\operatorname{ReLU}(x-t_i).
Each term changes the slope at one knot t_i. By choosing knots on a sufficiently fine mesh and
choosing c_i from changes in the piecewise-linear slope, H interpolates a Lipschitz target.
The same expression is a one-hidden-layer network: the first linear layer computes x-t_i, ReLU
applies the hinges, and the second linear layer forms their weighted sum.
For an exact example, take two hinges at the same knot t_0=0, one reading
x and one reading -x, both with coefficient one. Their sum is the absolute value:
-- Split at zero, where the active hinge changes; either
-- branch leaves one copy of the magnitude.
example (x : ℝ) : |x| = max x 0 + max (-x) 0 := x:ℝ⊢ |x| = max x 0 + max (-x) 0
x:ℝh:0 ≤ x⊢ |x| = max x 0 + max (-x) 0x:ℝh:x ≤ 0⊢ |x| = max x 0 + max (-x) 0
x:ℝh:0 ≤ x⊢ |x| = max x 0 + max (-x) 0 All goals completed! 🐙
x:ℝh:x ≤ 0⊢ |x| = max x 0 + max (-x) 0 All goals completed! 🐙
Here max y 0 is ReLU, so the right-hand side is a width-two ReLU network with first-layer weights
+1 and -1, zero biases, and second-layer weights both 1. This example allows a hinge
facing each direction; the interpolation formula above uses hinges facing right. In either case,
the proof splits at the knot: on one side of t_i the hinge is inert, on the other it contributes
its slope. The general theorem also uses the Lipschitz bound to choose a mesh and control the
interpolation error uniformly.
The theorem
relu_universal_approximation_Icc makes precisely that conversion. Its current signature is:
-- Expose the interval and Lipschitz premises before the
-- existential choice of network layers.
#check @relu_universal_approximation_Icc
Here a<b gives an interval with positive length.
L>0 and h_lip provide a quantitative continuity bound. \varepsilon>0 is needed before a
finite mesh can be chosen. The conclusion supplies two TorchLean LinearSpec values: the
input-to-hidden layer and the hidden-to-output layer used by mlpEvalScalar.
The printed ∀ x ∈ Set.Icc a b abbreviates two arguments: an input x and a proof that
a\leq x\leq b. Likewise, each arrow before the existential introduces a premise the caller
must supply. The braces around {f : ℝ → ℝ} mark an implicit parameter that Lean can infer from
those premises. After obtaining hidDim, the types of l1 and l2 depend on that dimension;
their hidden coordinates must agree. This ties the analytic construction to a well-shaped model.
Strict positivity of L is harmless for a constant target: any positive upper bound is also a
Lipschitz bound for that target, even though its smallest Lipschitz constant is zero.
The rate theorem chooses the width
N(L,a,b,\varepsilon)
= \left\lceil\frac{2L(b-a)}{\varepsilon}\right\rceil+1.
In Lean this is
reluApproximationWidth. The qualitative theorem uses it as its witness, and
relu_universal_approximation_Icc_rate states the same hidden dimension explicitly. The
arithmetic lemma underneath it proves
\frac{2L(b-a)}{N}<\varepsilon.
This bound is conservative. It establishes a construction with a stated size; it does not claim that the width is minimal, nor that gradient descent will discover these hinge parameters.
Approximation Rate And Network Width
The following #check commands display the declarations behind the width formula and are checked
when the page builds. The width takes four real arguments and returns a natural number:
-- The width is a natural count computed from four
-- real-valued specification parameters.
#check @reluApproximationWidth
The arithmetic lemma shows that this choice of width makes the mesh error smaller than the requested tolerance:
-- Inspect the strict mesh estimate obtained by adding one
-- after the ceiling.
#check @two_mul_mul_sub_div_relu_approximation_width_lt
The rate theorem then has the same hypotheses as before, with the existential over hidDim
discharged by that formula:
-- The hidden dimension is now fixed; only the two layer
-- parameter records remain existential.
#check @relu_universal_approximation_Icc_rate
The same definition cannot be evaluated with #eval:
-- This deliberately asks the compiler to execute a width
-- defined using mathematical reals.
#eval reluApproximationWidth 1 0 1 (1 / 10)
The width uses Nat.ceil on mathematical real numbers, so it is a proof-level construction rather
than a compiled numerical routine. That error marks the boundary between an existence proof over
exact reals and an executable parameter-selection program. A runtime tool could compute the same
formula from rational inputs, but that would be a separate executable definition with a refinement
theorem.
Lean can still prove the value for specific inputs. For a
1-Lipschitz target on [0,1] at \varepsilon=1/10, the width is twenty-one hidden units:
-- Prove the real ceiling calculation for this tolerance
-- without compiling it as a numerical
-- routine.
example :
reluApproximationWidth 1 0 1 (1 / 10) = 21 := ⊢ reluApproximationWidth 1 0 1 (1 / 10) = 21
All goals completed! 🐙
That is \lceil 2\cdot 1\cdot 1/(1/10)\rceil+1=21; norm_num proves the arithmetic, including the
ceiling. Halving \varepsilon approximately doubles the width, so this construction is
linear in 1/\varepsilon.
The extra one after the ceiling turns a weak inequality into a strict one. If the ratio inside
the ceiling is already an integer, choosing that integer alone would only give the mesh estimate
at the requested tolerance; adding one leaves room for the final < ε. The proof also knows the
width is positive, so division by its real-valued cast is legitimate. In the displayed type,
↑(reluApproximationWidth L a b ε) is exactly that cast from a natural count to a real denominator.
norm_num establishes an equality about this definition inside Lean's logic. It does not require
an executable implementation of arbitrary real inputs, which is why the proof succeeds even
though the preceding compilation attempt fails.
Quadratic Approximation In Binary32
To construct parameters explicitly, use four hinges on [0,1] for the target f(x)=x^2.
The following code computes the knots and chord slopes in Float, converts the knots and slope
increments to FloatLib binary32, and prints the resulting parameters. The next example evaluates
their
hinge sum in binary32 arithmetic.
-- Each coefficient records a slope increment, so active
-- hinges reconstruct the chord slope.
def meshN : Nat := 4
def meshStep : Float := 1.0 / 4.0
def target (x : Float) : Float := x * x
def knot (i : Fin meshN) : (ExecFloat.Binary 8 23) :=
(ExecFloat.Binary.ofFloat32 ∘ Float.toFloat32)
(Nat.toFloat i.val * meshStep)
-- Slope of the chord of `target` over subinterval `i`.
def chordSlope (i : Nat) : Float :=
(target (Nat.toFloat (i + 1) * meshStep)
- target (Nat.toFloat i * meshStep)) / meshStep
def coeff (i : Fin meshN) : (ExecFloat.Binary 8 23) :=
(ExecFloat.Binary.ofFloat32 ∘ Float.toFloat32)
(if i.val = 0 then chordSlope 0
else chordSlope i.val - chordSlope (i.val - 1))
#eval do
let ts := (List.finRange meshN).map
(knot · |> ExecFloat.Binary.toFloat32 |>.toFloat)
let cs := (List.finRange meshN).map
(coeff · |> ExecFloat.Binary.toFloat32 |>.toFloat)
let ss := (List.range meshN).map chordSlope
IO.println s!"knots {ts}"
IO.println s!"slopes {ss}"
IO.println s!"coeffs {cs}"
A hinge
c_i\operatorname{ReLU}(x-t_i) is inert to the left of its knot and contributes slope c_i to
the right, so between knots the sum has slope \sum_{t_i\leq x} c_i. For that running total to
match the chord slopes s_0,\dots,s_{N-1} printed above, the coefficients have to be the
increments: c_0=s_0 and c_i=s_i-s_{i-1}. Slopes 0.25,0.75,1.25,1.75 therefore give
coefficients 0.25,0.5,0.5,0.5. For example, after the second knot the first two hinges are
active: their coefficients add to the second chord's slope. This cumulative addition is why
coeff stores differences of slopes.
At x=3/8, only the knots at zero and one quarter contribute. Their terms are
(1/4)(3/8)=3/32 and (1/2)(1/8)=1/16, giving H(x)=5/32.
The target is 9/64, so the difference is 1/64, the 0.015625 in the table below.
This also explains the tensor layout in the PyTorch transcription below: each hidden coordinate
stores one distance from a knot, and the output weight on that coordinate stores a slope change.
The four coefficients are not four independent chord slopes. Copying the printed slope list into
the output layer would change the function, even though all layer dimensions would still match.
Now evaluate the network on a grid twice as fine as its own mesh, so that both the knots and the points between them appear:
-- Sample both knots and midpoints to distinguish
-- interpolation agreement from between-knot error.
#eval do
for k in [0, 1, 2, 3, 4, 5, 6, 7, 8] do
let x := Nat.toFloat k * 0.125
let xe :=
(ExecFloat.Binary.ofFloat32 ∘ Float.toFloat32) x
let hv :=
(ExecFloat.Binary.toFloat32
(hingeFunBinary knot coeff 0 xe)).toFloat
IO.println s!"x={x} f={target x} H={hv}"
The hinge sum agrees with x^2 at every knot because its slopes match the chords. Between knots
the real chord interpolant lies above the curve, since the target is convex. In the displayed
calculation, the overshoot is
0.015625 at every midpoint: the midpoint error of a
chord interpolant of this quadratic is \tfrac18 f''h^2=\tfrac18\cdot 2\cdot(1/4)^2.
Compare that with what the rate theorem certifies at this width. Since x^2 is 2-Lipschitz on
[0,1], the formula reaches four or fewer hidden units only once \varepsilon is at least
4/3:
-- Compare the prescribed widths for the same Lipschitz
-- bound at three tolerances.
example :
reluApproximationWidth 2 0 1 (4 / 3) = 4 := ⊢ reluApproximationWidth 2 0 1 (4 / 3) = 4
All goals completed! 🐙
example :
reluApproximationWidth 2 0 1 (1 / 10) = 41 := ⊢ reluApproximationWidth 2 0 1 (1 / 10) = 41
All goals completed! 🐙
example :
reluApproximationWidth 2 0 1 (1 / 20) = 81 := ⊢ reluApproximationWidth 2 0 1 (1 / 20) = 81
All goals completed! 🐙
The rate theorem supplies a real network with error below 4/3; the displayed binary32
mesh has sampled error 0.015625. Applying the theorem to these particular parameters requires
identifying its real construction with this mesh, then bounding conversion and execution error.
The width calculation alone does not discharge those obligations. A sharper interpolation bound
can also use the second derivative of this smooth target, information absent from the Lipschitz
hypotheses. The sampled error and the existence guarantee therefore describe different claims.
The last two examples make the size cost concrete: halving \varepsilon changes the prescribed
width from 41 to 81. This is an upper bound on the width needed by the construction. Proving
minimality would also require a lower bound that rules out smaller networks.
Sine Approximation
Convexity explains the one-sided interpolation error for x^2 and the increasing chord slopes.
The hinge construction itself only needs the slopes and their differences. Apply it to eight
hinges on [0,1] for f(x)=\sin(2\pi x):
-- Allow signed slope increments so the interpolant can
-- follow both halves of the wave.
def waveN : Nat := 8
def waveStep : Float := 1.0 / 8.0
def wave (x : Float) : Float :=
Float.sin (2.0 * 3.141592653589793 * x)
def waveKnot (i : Fin waveN) : (ExecFloat.Binary 8 23) :=
(ExecFloat.Binary.ofFloat32 ∘ Float.toFloat32)
(Nat.toFloat i.val * waveStep)
def waveChord (i : Nat) : Float :=
(wave (Nat.toFloat (i + 1) * waveStep)
- wave (Nat.toFloat i * waveStep)) / waveStep
def waveCoeff (i : Fin waveN) : (ExecFloat.Binary 8 23) :=
(ExecFloat.Binary.ofFloat32 ∘ Float.toFloat32)
(if i.val = 0 then waveChord 0
else waveChord i.val - waveChord (i.val - 1))
def waveHinge (x : Float) : Float :=
(ExecFloat.Binary.toFloat32
(hingeFunBinary waveKnot waveCoeff 0
((ExecFloat.Binary.ofFloat32 ∘ Float.toFloat32)
x))).toFloat
#eval do
let cs :=
(List.finRange waveN).map
(waveCoeff · |> ExecFloat.Binary.toFloat32 |>.toFloat)
IO.println s!"coeffs {cs}"
-- Signed error at four midpoints, two per half.
for k in [1, 3, 9, 11] do
let x := Nat.toFloat k * 0.0625
IO.println
s!"x={x} f={wave x} H-f={waveHinge x - wave x}"
let mut worst := 0.0
for k in [0:17] do
let x := Nat.toFloat k * 0.0625
worst := max worst (waveHinge x - wave x).abs
IO.println s!"worst on this grid = {worst}"
The coefficients change sign because the chord
slopes now decrease as well as increase, so a hinge can cancel the slope its predecessors added
rather than only steepening the curve. And the midpoint errors have both signs: the interpolant sits
below f where f is concave and above it where f is convex, so no one-sided statement of the
kind that held for x^2 is available. The Lipschitz error bound controls the absolute error in
both cases.
The rate formula reacts to this target the way a worst-case bound has to. Since
\sin(2\pi x) is 2\pi-Lipschitz, take L=7 as a rational upper bound and ask what eight
hidden units certify:
-- Use the rational Lipschitz upper bound seven in the same
-- width formula.
example : reluApproximationWidth 7 0 1 2 = 8 := ⊢ reluApproximationWidth 7 0 1 2 = 8
All goals completed! 🐙
The formula assigns width eight to \varepsilon=2. For this particular f, whose range is
[-1,1], that tolerance is loose: even the constant zero function has error at most one.
The measured error of the displayed mesh is about 0.07 on the sampled grid. The rate theorem
uses only the supplied Lipschitz constant, so it covers every
7-Lipschitz target with the same width. It does not use the sine function's curvature, and the
grid measurement does not establish a uniform bound between samples.
The two signs in H-f are useful here. A positive number means the approximation lies above the
target; taking an absolute value too early would hide the change in curvature between the two
halves of the wave. The final worst is a maximum over seventeen evaluated inputs, whereas the
analytic error statement quantifies over an interval. To turn such a grid into a regional bound,
one would also need to control how the error varies between adjacent inputs. The Lipschitz
construction supplies that control through its hypotheses and mesh argument. The printed table
instead helps inspect whether the chosen slope increments behave as intended.
ReLU Approximation In PyTorch
We can place the same knots and slope increments in two torch.nn linear layers. The first
layer uses all-ones weights and biases -t_i; the second weights the resulting hinges:
# Place each knot in the first-layer bias and each slope
# increment in the output weight.
import torch, torch.nn as nn
knots = torch.tensor([0.0, 0.25, 0.50, 0.75])
coeff = torch.tensor([[0.25, 0.5, 0.5, 0.5]])
net = nn.Sequential(nn.Linear(1, 4), nn.ReLU(), nn.Linear(4, 1))
with torch.no_grad():
net[0].weight.copy_(torch.ones(4, 1))
net[0].bias.copy_(-knots)
net[2].weight.copy_(coeff)
net[2].bias.zero_()
xs = torch.arange(0, 9, dtype=torch.float32).mul(0.125).unsqueeze(1)
with torch.no_grad():
ys = net(xs).squeeze(1)
The transcription is intended to produce the nine H values printed above. The inputs,
parameters, intermediate products, and partial sums of the displayed hinge computation are all
exactly representable in binary32. This explains why that computation has no rounding error;
checking the PyTorch execution remains a separate runtime comparison
((Paszke et al., 2019)).
The Lean table evaluates hingeFunBinary, the function used in the three-term executable
approximation theorem below. Applying that theorem still requires proofs of its
approximation, quantization, and finiteness premises for these parameters. A
transcription into another framework is a claim that has to be checked separately, which is exactly
what the roundtrip chapter is for.
Rounding Error
In the quadratic example, the hinge sum agrees with the target at the knots down to the last bit.
The knots and chord slopes are multiples of 1/4; on this small grid, the products and partial
sums are also exactly representable in binary32. The following comparison subtracts the bit
patterns of the two positive outputs, exposing differences hidden by decimal formatting:
-- Compare stored encodings at interior dyadic knots, where
-- decimal output could hide a difference.
#eval do
for k in [1, 2, 3] do
let x := Nat.toFloat k * meshStep
let xe :=
(ExecFloat.Binary.ofFloat32 ∘ Float.toFloat32) x
let hx := hingeFunBinary knot coeff 0 xe
let fx := (ExecFloat.Binary.ofFloat32 ∘ Float.toFloat32)
(target x)
let distance :=
ExecFloat.Binary.toBits32 hx -
ExecFloat.Binary.toBits32 fx
IO.println s!"knot {k}: {distance} ulp"
Move the same construction onto a mesh of three and the knots become multiples of 1/3, which
binary32 cannot represent:
-- Convert the thirds-based construction to binary32 before
-- comparing its interior-knot outputs.
def thirds : Float := 1.0 / 3.0
def knot3 (i : Fin 3) : (ExecFloat.Binary 8 23) :=
(ExecFloat.Binary.ofFloat32 ∘ Float.toFloat32)
(Nat.toFloat i.val * thirds)
def chord3 (i : Nat) : Float :=
(target (Nat.toFloat (i + 1) * thirds)
- target (Nat.toFloat i * thirds)) / thirds
def coeff3 (i : Fin 3) : (ExecFloat.Binary 8 23) :=
(ExecFloat.Binary.ofFloat32 ∘ Float.toFloat32)
(if i.val = 0 then chord3 0
else chord3 i.val - chord3 (i.val - 1))
#eval do
for k in [1, 2] do
let x := Nat.toFloat k * thirds
let xe :=
(ExecFloat.Binary.ofFloat32 ∘ Float.toFloat32) x
let hx := hingeFunBinary knot3 coeff3 0 xe
let fx := (ExecFloat.Binary.ofFloat32 ∘ Float.toFloat32)
(target x)
let distance :=
ExecFloat.Binary.toBits32 hx -
ExecFloat.Binary.toBits32 fx
IO.println s!"knot {k}: {distance} ulp"
At each interior knot the outputs are adjacent positive binary32 values, one ULP apart.
Float's six-digit rendering shows 0.111111 for both outputs at the first knot and 0.444444
for both at the second, hiding the discrepancy. This is an example of the distinction between a
stored value and its decimal display discussed by Goldberg ((Goldberg, 1991)).
This comparison includes several rounding steps: conversion of the input and coefficients, evaluation of the hinge sum, and conversion of the reference target value. The theorems below separate parameter conversion from evaluation error. They also require finite executable intermediates so that each arithmetic step can be related to a real-valued expression.
From Real Parameters To A Floating-Point Format
The worked examples use binary32, but the proof takes the format as a parameter. An executable
value also specifies its storage plan and a FloatLib codec relating stored values to the model.
The arithmetic refinement assumes format.isIEEE = true; binary16, binary32, binary64, and
binary128 can use the same theorem. Once knots, coefficients, and the bias are stored in the chosen
format, the total error naturally splits into
\begin{aligned}
|f(x)-H_{\mathrm{IEEE}}(x)|
\leq{}&
|f(x)-H_{\mathbb R}(x)|\\
&+|H_{\mathbb R}(x)-H_{\mathrm{embedded}}(x)|\\
&+|H_{\mathrm{embedded}}(x)-H_{\mathrm{IEEE}}(x)|.
\end{aligned}
These are, respectively:
-
approximation error of the real hinge network;
-
parameter-quantization or reference error;
-
rounded evaluation error.
The distinction is visible in
the three-term approximation theorem. It takes real hinge parameters tR and cR,
executable parameters t, c, and b0 in that format, and separate assumptions for the real
approximation and quantization terms. It also requires finiteness witnesses for the intermediate
hinge sum and output. Its conclusion adds hingeFunErrorBound to the two supplied tolerances.
To use this theorem, conversion and evaluation must satisfy its finiteness assumptions. Its dyadic specialization starts from dyadic parameters and uses a half-ULP rounding bound, but it still asks for finite evaluation witnesses.
The full signature exposes the obligations needed to connect the real approximant to executable arithmetic:
-- Inspect the separate approximation,
-- parameter-quantization, and finite-execution obligations.
#check @relu_approximation_Icc_binary_three_term
Read it from the top. The two parameter vectors come in pairs, tR cR over the reals and t c over
the configured format, because the theorem has to talk about both to relate them. The two isFinite
hypotheses on t and c rule out NaN and infinite parameters, which is a condition a real-valued
statement could not even express. The HingeSumFinite conjunct is the one to notice: it demands
that every intermediate of the fold stay finite, not merely the result. The proof uses finite
real embeddings at each arithmetic step; an overflowing intermediate breaks that argument. The next
two hypotheses are the
\varepsilon_{\mathrm{Approx}} and \varepsilon_Q budgets from the three-term split, supplied
rather than derived. And the conclusion adds hingeFunErrorBound to their sum, which is the
rounding of the evaluation itself.
For a particular checkpoint, each premise must be proved for its stored parameters and the stated
input domain. instDecHingeSumFinite makes the HingeSumFinite predicate decidable for a fixed
input and concrete parameters. After installing it with haveI, decide can prove a true concrete
instance. A premise
quantified over all inputs in an interval still needs an argument covering that whole domain.
Notice that the final input is a stored value in the chosen format, and interval membership is
tested on its decoded
real value Model.toReal (ExecFloat.Binary.toModel x). The target is therefore evaluated at the
real number represented by that
stored input. If an application starts with an ideal real measurement and rounds it before model
evaluation, its input-conversion error is an additional question. A Lipschitz bound on the target
can help relate those two inputs, but that step is not hidden inside εQ: the quantization premise
shown here compares two parameterizations at the same embedded input. Keeping that input fixed
makes the three terms correspond to three identifiable functions.
A companion theorem for dyadic parameters replaces the supplied
\varepsilon_Q with a half-ULP bound derived from dyadic parameters. It is the more usable form
when reference parameters are given as dyadics. It assumes knots in [a,b] and finite rounded
parameters; the per-parameter half-ULP errors are propagated through the hinge sensitivities,
including the interval length |b-a|. The finite-evaluation witnesses remain necessary
because finite stored parameters can still produce an overflowing intermediate.
For example, the output accumulation can overflow even if every weight, bias, and input was converted successfully. The witness follows the intermediate operations of the hinge evaluation, which is why it appears separately from the parameter-conversion estimate. Checking only the stored parameter bits would leave that part of the theorem's hypothesis unaddressed. The dyadic specialization exposes those witnesses in its signature:
-- Dyadic reference parameters supply the quantization
-- estimate; finite evaluation is still
-- required.
#check @relu_approximation_Icc_binary_dyadic_half_ulp
TorchLean also has an intermediate
rounded-real theorem.
RoundedReLUApprox.relu_universal_approximation_Icc format evaluates the hinge construction with
rounding at each operation and proves a pointwise bound of the form
|f(x)-H_{\mathrm{rounded}}(x)|
< \varepsilon+\operatorname{hingeFunErrorBound}(x).
-- This bound concerns the rounded-real carrier and reads
-- its result through the val field.
#check @RoundedReLUApprox.relu_universal_approximation_Icc
Compare that conclusion with the real one printed earlier. The hypotheses are identical, the
existential now produces hinge parameters rather than a LinearSpec pair, and the bound has grown a
second summand. That summand bounds evaluation in this model. It does not include a separate
conversion of
arbitrary real parameters into finite storage.
Rounded format values carry arbitrary reals; each primitive operation rounds its result to the
format's precision and underflow grid, with no upper exponent cutoff. This carrier is FloatLib's
NF, specialized by the format descriptor. The executable bridge connects it to stored values
under the IEEE-format and finite-intermediate hypotheses. Changing format changes the grid and
the error bounds without selecting a different proof file.
Exact Finite Interval Images
Approximation theory also appears in a finite semantic form. The module
FloatInterval.Semantics
defines intervals of FloatLib binary32 values. Its exact abstract operations take the hull of
the finite concrete image; these are noncomputable specifications. For addition, the central
theorem is:
-- The conclusion is enclosure of the executable sum for
-- every pair of interval members.
#check @OpsExact.add_sound
For any members x of A and y of B, their executable sum belongs to addSharp A B.
No separate rounding hypothesis appears, because the
abstract operator was built by enumerating the concrete image rather than by an interval formula
that would need one.
The multiplication and ReLU theorems have the same shape. They are then composed through an affine layer and a two-layer ReLU network. Hover the two signatures to read the hypotheses in full:
-- Follow scalar enclosure through an affine layer and then
-- the two-layer network.
#check @aff_sound
#check @eval_sound
The four explicit hypotheses on eval_sound are the isNaN ... = false conditions on the two
weight matrices and two bias vectors. They are stated per entry rather than as one predicate on the
network, which is slightly more verbose to supply and considerably easier to discharge from a
concrete checkpoint. The implicit OpsExact.Sound argument is supplied by the soundness
instance proved in the same file.
The weight and bias hypotheses rule out NaN parameters. The conclusion concerns executable FloatLib binary32 evaluation. The finite carrier lets the exact operators describe every concrete pair in an interval using classical finite sets. This gives a reference semantics for enclosure proofs; it does not supply an efficient interval evaluator.
There is also a difference between an exact concrete image and its interval hull. For a set of
executable results with gaps, the smallest containing interval can include values the operation
never returns. add_sound promises membership in that containing interval; it does not assert
that every member is attained. This is the right direction for verification: excluding an unsafe
value from the enclosure excludes it from the concrete image as well. It is less useful for proving
that a value is attainable. The constant-target result later in the chapter has a particularly
simple image because every allowed input returns the same finite constant.
Run the proof modules directly:
# Check the scalar interval semantics and its finite-image # theorem as separate modules. scripts/lake.sh env lean \ NN/MLTheory/Proofs/Approximation/FloatInterval/Semantics.lean scripts/lake.sh env lean \ NN/MLTheory/Proofs/Approximation/FloatInterval/ExactImageTheorem.lean
A successful run is silent and exits with status zero. If you want the same three signatures in a scratch file rather than on this page, the imports and namespaces are:
-- Open the scalar and composed-network namespaces to -- inspect their enclosure interfaces. import NN.MLTheory.Proofs.Approximation.FloatInterval.Semantics open NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox open NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.TwoLayerMLPExact #check OpsExact.add_sound #check aff_sound #check eval_sound
Note that add_sound lives in OpsExact while aff_sound and eval_sound live in
TwoLayerMLPExact; the split follows the file's own layering of scalar operators under composed
network semantics.
An application of aff_sound must discharge each isNaN ... = false premise.
A point interval containing NaN cannot be treated as an ordinary ordered singleton. Omitting
one of these premises leaves that part of the enclosure argument unproved.
Higher-Dimensional Domains
The one-dimensional hinge proof is constructive and quantitative. The higher-dimensional
development uses a different route. In
StoneWeierstrass,
Tensor ℝ [n] is identified with Fin n → ℝ by a homeomorphism. Coordinate functions generate a
subalgebra of continuous functions, and the proof establishes that this subalgebra separates
points: distinct tensors differ in at least one coordinate, and the corresponding coordinate
function distinguishes them. Mathlib's Stone-Weierstrass theorem (Community, 2020)
then supplies density on compact domains. The TorchLean-specific work establishes the
homeomorphism and checks the subalgebra hypotheses needed by that theorem.
Here the approximating objects are coordinate-polynomial expressions. A subalgebra contains
constants and is closed under addition, multiplication, and scalar multiplication, so starting
from coordinate projections permits expressions such as a coordinate squared or a product of two
coordinates. Point separation says this class can distinguish any two different tensor inputs.
Compactness is what lets density be stated using uniform error over the whole domain. The source
conclusion ∃ g : coordSubalg, ‖(g : C(K, ℝ)) - f‖ < ε chooses one such continuous function;
C(K, ℝ) bundles continuity with the function, and its norm measures the largest absolute error.
A later neural construction still has to represent or approximate that polynomial expression.
That topological argument answers a broad representation question, but it does not produce the same explicit width formula as the one-dimensional Lipschitz construction. The two proofs are complementary:
-
the hinge mesh exposes parameters and a rate on
[a,b]; -
the coordinate-subalgebra proof handles compact multidimensional domains at a more abstract level.
Approximation And Enclosure Guarantees
The scalar hinge construction also has a theorem for the corresponding two-layer network. The
two-layer configured binary approximation API packages representation, parameter-rounding, and
executable-rounding error in relu_mlp_approximation_three_term. Unlike the hinge theorem,
this theorem takes all three budgets, including the execution bound, as hypotheses and composes
them by the triangle inequality.
For finite interval semantics, the
constant-target API
proves exactIntervalImage_constant: a finite constant has the exact singleton interval image.
This gives a base case for reasoning about interval images.
Both results are checked as this page builds; hover to read their hypotheses:
-- Compare the three-budget network theorem with the exact
-- constant-image base case.
#check @relu_mlp_approximation_three_term
#check @ConstantTarget.exactIntervalImage_constant
The original binary32 interval theorem packages the remaining construction obligations explicitly.
roundedTargetExactIntervalImage_of_correctRounding takes a correct-rounding bridge, real
activation conditions, a threshold-network construction, and an exact interval-semantics
construction. Supplying those premises gives the exact-image conclusion for rounded targets.
#check @roundedTargetExactIntervalImage_of_correctRounding
For the quantitative two-layer approximation theorem introduced earlier, the error budgets give:
\text{target error}
\leq
\text{representation error}
+\text{parameter rounding error}
+\text{execution error}.
The three terms come from representation, parameter conversion, and executable arithmetic. Writing the sum explicitly lets an application decide where to spend its error budget. A CROWN or interval certificate can separately supply a sound enclosure over an input region for the chosen network. That enclosure is a regional property, not automatically another additive error term in this inequality.
The constructions follow the classical universal-approximation tradition. Cybenko (1989) proved density for superpositions of a sigmoidal function, and Hornik (1991) removed the sigmoid-specific hypothesis for multilayer feedforward networks. Both are density results: they say an approximant exists and are silent about its size. The explicit ReLU construction obtains a width formula by choosing a mesh and computing its slope increments. The finite interval development proves enclosure for executable binary32 networks and states the construction premises needed for its rounded-target exact-image theorem.