Exact Interval Images for Rounded Targets

Structured theorem statements for exact interval images of rounded floating-point targets, specialized to IEEE32Exec.

This file defines correctly-rounded activation assumptions, separating-activation assumptions, finite σ-networks, exact interval semantics, and the pipeline theorem:

correctly rounded activation + separating construction + exact semantics construction implies exact interval images for every finite rounded target on [-1,1]^d.

Separating activation condition, specialized to IEEE32Exec

Source: Hwang et al. (arXiv:2506.16065), Condition 1 and its correctly-rounded sufficient conditions.

@[reducible, inline]

abbrev NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.Condition1.F : Type

Alias for the executable float format used throughout this file (IEEE32Exec).

Float-format constants for IEEE binary32

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.Condition1.M : ℕ

Mantissa bitwidth M for IEEE binary32 (excluding the hidden leading bit).

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.Condition1.emin : ℤ

Minimum normal exponent emin for IEEE binary32.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.Condition1.emax : ℤ

Maximum normal exponent emax for IEEE binary32.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.Condition1.ε : ℝ

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.Condition1.ω : ℝ

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.Condition1.pow2 (k : ℤ) : ℝ

Basic helpers

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.Condition1.finite (x : F) : Prop

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.Condition1.rabs (x : F) : ℝ

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.Condition1.between (a b x : F) : Prop

Separating activation condition

structure NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.Condition1.Witness (σ : F → F) : Type

• c1 : F

  First finite input witnessing the zero anchor in the separating condition.

• c2 : F

  Second finite input used to create a nonzero separated activation value.

• c1_finite : finite self.c1

  The first witness input is finite.

• c2_finite : finite self.c2

  The second witness input is finite.

• sigma_c1_eq_zero : σ self.c1 = Numbers.zero

  The activation sends the first witness to zero.

• sigma_c2_finite : finite (σ self.c2)

  The activation value at the second witness is finite.

• sigma_c2_abs_mem : rabs (σ self.c2) ∈ Set.Icc (ε / 2 + 2 * ε ^ 2) (5 / 4 - 2 * ε)

  The second activation value has the magnitude required by the binary32 separation bound.

• max_abs_c1_c2_ge : max (rabs self.c1) (rabs self.c2) ≥ pow2 (emin + 1)

  At least one witness input is not too close to underflow.

• sigma_between_on_Icc (x : F) : self.c1 ≤ x → x ≤ self.c2 → between (σ self.c1) (σ self.c2) (σ x)

  Between c1 and c2, activation values stay between the endpoint activation values.

• η : F

  Threshold witness for the local binary32 separation step.

• η_finite : finite self.η

  The threshold witness is finite.

• η_abs_mem : rabs self.η ∈ Set.Icc (pow2 (emin + 5)) (4 - 8 * ε)

  The threshold witness lies in the binary32 magnitude window required by the theorem.

• sigma_eta_finite : finite (σ self.η)

  The activation value at the threshold is finite.

• sigma_etaPlus_finite : finite (σ (TorchLean.Floats.IEEE754.IEEE32Exec.nextUp self.η))

  The activation value at the next float above the threshold is finite.

• sigma_eta_abs_mem : rabs (σ self.η) ∈ Set.Icc (pow2 (emin + 5)) (pow2 (emax - 6) * rabs self.η)

  The threshold activation magnitude is bounded in the required binary32 window.

• sigma_etaPlus_abs_mem : rabs (σ (TorchLean.Floats.IEEE754.IEEE32Exec.nextUp self.η)) ∈ Set.Icc (pow2 (emin + 5)) (pow2 (emax - 6) * rabs self.η)

  The next-up activation magnitude is bounded in the required binary32 window.

• threshold_separates (x y : F) : x ≤ self.η → self.η < TorchLean.Floats.IEEE754.IEEE32Exec.nextUp self.η → TorchLean.Floats.IEEE754.IEEE32Exec.nextUp self.η ≤ y → σ x ≤ σ self.η ∧ σ self.η < σ (TorchLean.Floats.IEEE754.IEEE32Exec.nextUp self.η) ∧ σ (TorchLean.Floats.IEEE754.IEEE32Exec.nextUp self.η) ≤ σ y ∨ σ x ≥ σ self.η ∧ σ self.η > σ (TorchLean.Floats.IEEE754.IEEE32Exec.nextUp self.η) ∧ σ (TorchLean.Floats.IEEE754.IEEE32Exec.nextUp self.η) ≥ σ y

  The activation separates values below and above the threshold interval.

• lam : ℝ

  Real Lipschitz envelope around the threshold.

• lam_mem : self.lam ∈ Set.Icc 0 (pow2 (emax - 7) * min (rabs (σ self.η)) (pow2 (Int.ofNat (M + 3))))

  The envelope constant is in the paper's binary32-safe range.

• lipschitz_around_threshold (x y : F) : x ≤ self.η → self.η < TorchLean.Floats.IEEE754.IEEE32Exec.nextUp self.η → TorchLean.Floats.IEEE754.IEEE32Exec.nextUp self.η ≤ y → |TorchLean.Floats.IEEE754.IEEE32Exec.toReal (σ x) - TorchLean.Floats.IEEE754.IEEE32Exec.toReal (σ self.η)| ≤ self.lam * |TorchLean.Floats.IEEE754.IEEE32Exec.toReal x - TorchLean.Floats.IEEE754.IEEE32Exec.toReal self.η| ∧ |TorchLean.Floats.IEEE754.IEEE32Exec.toReal (σ y) - TorchLean.Floats.IEEE754.IEEE32Exec.toReal (σ (TorchLean.Floats.IEEE754.IEEE32Exec.nextUp self.η))| ≤ self.lam * |TorchLean.Floats.IEEE754.IEEE32Exec.toReal y - (TorchLean.Floats.IEEE754.IEEE32Exec.nextUp self.η).toReal|

  Activation values obey the Lipschitz envelope on both sides of the threshold gap.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.Condition1.Holds (σ : F → F) : Prop

Separating activation condition for σ, packaged as existence of a Witness.

Correctly-rounded activations and real sufficient conditions

structure NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.Condition1.CorrectlyRounded (ρ : ℝ → ℝ) (σ : F → F) : Prop

• finite_input_implies (x : F) : finite x → finite (σ x) ∧ TorchLean.Floats.IEEE754.IEEE32Exec.toReal (σ x) = TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round (ρ (TorchLean.Floats.IEEE754.IEEE32Exec.toReal x))

  Finite executable inputs evaluate to finite executable outputs with the declared rounding law.

structure NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.Condition1.RealWitness (ρ : ℝ → ℝ) : Type

Real-valued sufficient conditions used to prove that a correctly-rounded activation satisfies the separating activation condition.

This is a “real” analogue of Witness that talks about a target function ρ : ℝ → ℝ.

• c1' : F

  First binary32 input used by the real sufficient conditions.

• c2' : F

  Second binary32 input used by the real sufficient conditions.

• c1'_finite : finite self.c1'

  The first input is finite.

• c2'_finite : finite self.c2'

  The second input is finite.

• rho_c1'_small : |ρ (TorchLean.Floats.IEEE754.IEEE32Exec.toReal self.c1')| ≤ ω / 2

  The real activation is close to zero at the first witness.

• rho_c2'_range : |ρ (TorchLean.Floats.IEEE754.IEEE32Exec.toReal self.c2')| ∈ Set.Icc (ε / 2 + 2 * ε ^ 2) (5 / 4 - 2 * ε)

  The real activation has the required magnitude at the second witness.

• max_abs_c1'_c2'_ge : max (rabs self.c1') (rabs self.c2') ≥ pow2 (emin + 1)

  At least one real witness input has magnitude safely above underflow.

• rho_between_on_Icc (x : ℝ) : TorchLean.Floats.IEEE754.IEEE32Exec.toReal self.c1' ≤ x → x ≤ TorchLean.Floats.IEEE754.IEEE32Exec.toReal self.c2' → min (ρ (TorchLean.Floats.IEEE754.IEEE32Exec.toReal self.c1')) (ρ (TorchLean.Floats.IEEE754.IEEE32Exec.toReal self.c2')) ≤ ρ x ∧ ρ x ≤ max (ρ (TorchLean.Floats.IEEE754.IEEE32Exec.toReal self.c1')) (ρ (TorchLean.Floats.IEEE754.IEEE32Exec.toReal self.c2'))

  On the witness interval, ρ stays between its endpoint values.

• δ : ℝ

  Real-valued threshold location used by the sufficient conditions.

• δ_abs_mem : |self.δ| ∈ Set.Icc (3 / 8) (7 / 8)

  The threshold lies in the specified central window.

• rho_threshold_properties : (∀ (x y : ℝ), x ≤ self.δ - 1 / 8 → self.δ + 1 / 8 ≤ y → ρ x ≤ ρ (self.δ - 1 / 8) ∧ ρ (self.δ - 1 / 8) < ρ (self.δ + 1 / 8) ∧ ρ (self.δ + 1 / 8) ≤ ρ y ∨ ρ x ≥ ρ (self.δ - 1 / 8) ∧ ρ (self.δ - 1 / 8) > ρ (self.δ + 1 / 8) ∧ ρ (self.δ + 1 / 8) ≥ ρ y) ∧ ∀ (x y : ℝ), x ∈ Set.Icc (self.δ - 1 / 8) (self.δ + 1 / 8) → y ∈ Set.Icc (self.δ - 1 / 8) (self.δ + 1 / 8) → |ρ x| ∈ Set.Icc (1 / 4) 1 ∧ |ρ x - ρ y| > 1 / 8 * |x - y|

  Threshold separation and local growth conditions for the real activation.

• lam : ℝ

  Lipschitz constant for the real activation.

• lam_mem : self.lam ∈ Set.Icc 0 (1 / 5 * pow2 (emax - 9))

  The Lipschitz constant is in the binary32-safe range required by the theorem.

• lipschitz (x y : ℝ) : |ρ x - ρ y| ≤ self.lam * |x - y|

  Global Lipschitz bound for the real activation.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.Condition1.RealSufficientConditions (ρ : ℝ → ℝ) : Prop

Existence of a RealWitness for ρ.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.Condition1.correctRoundingSatisfiesSeparatingActivation (ρ : ℝ → ℝ) (σ : F → F) : Prop

Correct-rounding bridge: a real activation satisfying the sufficient conditions induces a rounded floating-point activation satisfying the separating activation condition.

Finite σ-network model

structure NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.SigmaNet.Affine (din dout : ℕ) : Type

Parameters of an affine layer din → dout over IEEE32Exec scalars.

• W : Fin dout → Fin din → F

  W.

• b : Fin dout → F

  b.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.SigmaNet.aff {din dout : ℕ} (A : Affine din dout) (x : Fin din → F) : Fin dout → F

Apply an affine layer to an input vector using IEEE32Exec primitives.

inductive NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.SigmaNet.Net : ℕ → ℕ → Type

A feedforward σ-network: affine layers with σ between them, no σ after the final affine.

• last {din dout : ℕ} (A : Affine din dout) : Net din dout
• step {din mid dout : ℕ} (A : Affine din mid) (n : Net mid dout) : Net din dout

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.SigmaNet.eval (σ : F → F) {din dout : ℕ} : Net din dout → (Fin din → F) → Fin dout → F

Evaluate a σ-network on a concrete input vector.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.SigmaNet.eval1 {din : ℕ} (σ : F → F) (n : Net din 1) (x : Fin din → F) : F

Specialized evaluator for scalar-output (dout = 1) networks.

Interval semantics using OpsExact

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.SigmaNet.sigmaSharp (σ : F → F) (J : I) : I

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.SigmaNet.affSharp {din dout : ℕ} (A : Affine din dout) (B : I.Box din) : I.Box dout

Interval semantics of an affine layer, using the exact interval ops from OpsExact.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.SigmaNet.evalSharp (σ : F → F) {din dout : ℕ} : Net din dout → I.Box din → I.Box dout

Interval semantics for a network: apply affSharp and then push the activation through sigmaSharp.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.SigmaNet.evalSharp1 {din : ℕ} (σ : F → F) (n : Net din 1) (B : I.Box din) : I

Specialized interval evaluator for scalar-output (dout = 1) networks.

Bounded interval domains and direct-image hulls

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.IntervalIn (a b : F) (J : I) : Prop

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.BoxIn {d : ℕ} (a b : F) (B : I.Box d) : Prop

A product box B lies in I[a,b]^d (componentwise).

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.CubeBox {d : ℕ} (B : I.Box d) : Prop

The canonical cube domain [-1,1]^d.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.idealSharp {d : ℕ} (h : (Fin d → F) → F) (B : I.Box d) : I

Ideal abstraction h♯(B): interval hull of the direct image h(γ(B)) (computed over the finite concretization).

Indicator functions and separability

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.Indicators.ι {d : ℕ} (S : Set (Fin d → F)) : (Fin d → F) → F

Indicator of a set S ⊆ F^d, returning 1/0 in F.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.Indicators.ιGt (a : F) : F → F

Strict-threshold indicator ι_{>a} on F.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.Indicators.ιGe (a : F) : F → F

Non-strict threshold indicator ι_{≥a} on F.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.Indicators.ιLt (a : F) : F → F

Strict-threshold indicator ι_{<a} on F.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.Indicators.ιLe (a : F) : F → F

Non-strict threshold indicator ι_{≤a} on F.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.Indicators.scale (K : F) (g : F → F) : F → F

Scaled (by K) indicator: K ⊗ ι.

We model “there exists a σ-network implementing a scaled threshold-indicator exactly under interval semantics on I[a,b]” using our SigmaNet.Net interval interpreter evalSharp1.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.Separability.IntervalDomain (a b : F) : Set I

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.Separability.unaryIdealSharp (g : F → F) (J : I) : I

“Ideal” abstraction g♯ for a unary function g : F → F on an input interval J.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.Separability.SeparableOn (σ : F → F) (a b η K : F) : Prop

Separability of σ on I[a,b] with threshold η and scale K.

Informally, this asserts existence of σ-networks whose interval semantics coincides with the ideal abstraction of scaled threshold indicators (ι_{≤z}, ι_{≥z}, and ι_{>η}).

Finite min/max witnesses for ideal hulls

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.IdealMinMax.chooseMin_le_of_mem (s : Finset F) (hs : s.Nonempty) (hn : ∀ z ∈ s, TorchLean.Floats.IEEE754.IEEE32Exec.isNaN z = false) {y : F} (hy : y ∈ s) : OpsExact.chooseMin s hs ≤ y

chooseMin is below every element of the finset (under the no-NaN side condition).

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.IdealMinMax.le_chooseMax_of_mem (s : Finset F) (hs : s.Nonempty) (hn : ∀ z ∈ s, TorchLean.Floats.IEEE754.IEEE32Exec.isNaN z = false) {y : F} (hy : y ∈ s) : y ≤ OpsExact.chooseMax s hs

chooseMax is above every element of the finset (under the no-NaN side condition).

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.IdealMinMax.exists_minmax_for_idealSharp {d : ℕ} (h : (Fin d → F) → F) (B : I.Box d) (hB : (I.γ B).Nonempty) (hnan : ∀ (x : Fin d → F), TorchLean.Floats.IEEE754.IEEE32Exec.isNaN (h x) = false) : ∃ (m : F) (M : F), ExactImage.IsMinOn h (I.γ B) m ∧ ExactImage.IsMaxOn h (I.γ B) M ∧ (idealSharp h B).γI = ExactImage.Icc m M

Existence of min/max witnesses for idealSharp on a nonempty box domain.

This packages the interval hull characterization of idealSharp as an Icc m M.

Exact interval images from separating threshold networks

Separability and exact-semantics premises

@[reducible, inline]

abbrev NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.ExactImageFromSeparability.SeparatingActivation (σ : F → F) : Prop

Separating activation condition specialized to IEEE32Exec.

Premise: the separating activation condition yields exact threshold-indicator networks on [-1,1].

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.ExactImageFromSeparability.separatingActivationYieldsThresholdNetworksOnCube (σ : F → F) : Prop

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.ExactImageFromSeparability.thresholdNetworksYieldExactIntervalSemantics (σ : F → F) : Prop

Premise: separability yields a σ-network whose interval semantics equals the direct-image hull.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.ExactImageFromSeparability.exactIntervalSemanticsUniversalOnCube (σ : F → F) : Prop

For any NaN-free rounded target h, there exists a σ-network with exact interval semantics.

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.ExactImageFromSeparability.exactIntervalSemantics_universalOnCube_of_condition1_and_separableOn (σ : F → F) : SeparatingActivation σ → separatingActivationYieldsThresholdNetworksOnCube σ → thresholdNetworksYieldExactIntervalSemantics σ → exactIntervalSemanticsUniversalOnCube σ

Separating activations and threshold-network composition imply exact interval semantics.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.ExactImageFromSeparability.roundedTargetExactIntervalImage (σ : F → F) : Prop

Exact interval-image theorem for rounded targets: for every NaN-free rounded target fHat, there is a σ-network whose interval semantics is exactly the min/max hull of fHat '' γ(B) on every cube box.

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.ExactImageFromSeparability.roundedTargetExactIntervalImage_of_exactIntervalSemantics (σ : F → F) : exactIntervalSemanticsUniversalOnCube σ → roundedTargetExactIntervalImage σ

Derive exact interval images from exact interval semantics by choosing finite min/max witnesses.

Correct rounding to exact interval images

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.PaperStatements.ExactImageFromSeparability.roundedTargetExactIntervalImage_of_correctRounding (ρ : ℝ → ℝ) (σ : F → F) (hRound : Condition1.correctRoundingSatisfiesSeparatingActivation ρ σ) (hCR : Condition1.CorrectlyRounded ρ σ) (hReal : Condition1.RealSufficientConditions ρ) (hThresholds : separatingActivationYieldsThresholdNetworksOnCube σ) (hExactConstruction : thresholdNetworksYieldExactIntervalSemantics σ) : roundedTargetExactIntervalImage σ

Pipeline theorem: correctly-rounded real activations plus separating-threshold constructions imply exact interval images for rounded targets.