Constant rounded targets over binary32 intervals

Exact interval-image theorem for constant rounded targets over Binary 8 23.

This file packages the finite-float base case for FloatLib's binary32 intervals: a constant rounded target has exact interval semantics given by the point interval [c,c] on every valid input box.

The companion file FloatInterval.Semantics develops the same idea for the abstract interval domain I used by the MLP interval evaluator. This file states the result directly for binary32 endpoints at the rounded-target boundary.

@[reducible, inline]

abbrev NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.Box (d : ℕ) : Type

Product box of float32 intervals.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.γI (J : FloatLib.Numerics.Interval F) : Set F

Concretization of a float32 interval to a set of float32 values.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.γ {d : ℕ} (B : Box d) : Set (Fin d → F)

Concretization of a product box to a set of float32 vectors.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.BoxValid {d : ℕ} (B : Box d) : Prop

Basic “well-formedness” predicate for product boxes.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.ExactIntervalImage {d : ℕ} (g : (Fin d → F) → F) (nuInt : Box d → FloatLib.Numerics.Interval F) : Prop

Exact interval-image property, phrased as: for every valid input box B, the interval semantics nuInt(B)’s concretization is exactly the float interval between the min/max of the target’s direct image on γ(B).

We phrase extrema relationally, rather than through a chosen float min/max operator, because NaN-aware binary32 orders need their edge cases stated explicitly.

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.gamma_nonempty_of_BoxValid {d : ℕ} {B : Box d} (hB : BoxValid B) : (γ B).Nonempty

A valid box is nonempty, witnessed by its own lower corner.

The exact-image statements quantify over nonempty concretizations, so this is what discharges that hypothesis for any box the checker actually produces.

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.exactIntervalImage_constant {d : ℕ} (c : F) (hc : FloatLib.Floats.ExecFloat.Binary.isFinite c = true) : ExactIntervalImage (fun (x : Fin d → F) => c) fun (x : Box d) => FloatLib.Floats.ExecFloat.Binary.Interval.point c

Base case: a constant target g(x) = c has an exact interval-image witness given by the constant network and the point interval [c,c].