Constant rounded targets over Interval32

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

This file packages the finite-float base case for the concrete IEEE32Exec.Interval32 interval type: 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. We keep this file separate because it is the direct Interval32 statement used at the low-level rounded-target boundary, while FloatInterval.Semantics is the reusable abstract-domain semantics.

@[reducible, inline]

abbrev NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.I : Type

Shorthand for the float32 interval type IEEE32Exec.Interval32.

@[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 : I) : 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.BoxInCube {d : ℕ} (B : Box d) : Prop

B is a box contained in [-1,1]^d.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.ExactIntervalImage {d : ℕ} (g _ν : (Fin d → F) → F) (nuInt : Box d → I) : 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.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.RoundedTargetExactIntervalImageStatement (d : ℕ) : Prop

Generic exact-interval-image statement shape for ExecFloat.Binary 8 23 rounded targets.

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.le_refl_of_isFinite (x : F) (hx : FloatLib.Floats.ExecFloat.Binary.isFinite x = true) : x ≤ x

Float comparison is reflexive on finite values. Not a Preorder instance, because NaN is not comparable to itself and IEEE 754 order is genuinely partial.

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 : 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].