FP32

Directed-rounding and nonlinear-enclosure instances for the rounded-real FP32 model.

This is not an executable backend (it is noncomputable in general, because FP32 is modeled on ℝ). It exists so proofs can state “sound w.r.t. float32 semantics” without mentioning Lean’s builtin Float.

FP32 is an unbounded-exponent binary32 model: it has 24-bit significands and gradual underflow, but no overflow, infinities, or NaNs. The nonlinear bounds use Real.exp and other real functions, so results here hold for this proof model and say nothing about overflow on a real binary32 device.

This module is an optional convenience layer and lives under NN/MLTheory/CROWN/Extras/.

FP32 instances

@[reducible, inline]

abbrev NN.MLTheory.CROWN.FP32 : Type

FP32 scalar type used for FP32-specialized CROWN/LiRPA statements.

noncomputable def NN.MLTheory.CROWN.FP32.roundDownEndpoint (x : ℝ) : FP32

Embed a real endpoint after rounding it downward to the binary32 grid.

noncomputable def NN.MLTheory.CROWN.FP32.roundUpEndpoint (x : ℝ) : FP32

Embed a real endpoint after rounding it upward to the binary32 grid.

@[instance_reducible]

noncomputable instance NN.MLTheory.CROWN.FP32.instBoundOps : BoundOps FP32

Directed endpoint arithmetic for the rounded-real FP32 model.

Each operation is performed on the underlying real values and rounded directly toward the appropriate side of the binary32 grid. The enclosure laws are FloatLib.Floats.Interval.roundDown_le and FloatLib.Floats.Interval.le_roundUp.

@[instance_reducible]

noncomputable instance NN.MLTheory.CROWN.FP32.instLawfulBoundOps : LawfulBoundOps FP32

The proof-oriented FP32 endpoint operations enclose exact real arithmetic.

This follows directly from the format-generic floor and ceiling rounding theorems. It is the law dictionary used by sound rounded CROWN statements over FP32.

instance NN.MLTheory.CROWN.FP32.instLawfulMinBoundOps : LawfulMinBoundOps FP32

Minimum selects an existing endpoint, so it preserves the underlying real value.

@[instance_reducible]

noncomputable instance NN.MLTheory.CROWN.FP32.instNonlinearBoundOps : NonlinearBoundOps FP32

Exact-real nonlinear operations rounded outward to the binary32 grid.

theorem NN.MLTheory.CROWN.FP32.roundDownEndpoint_le (x : ℝ) : (roundDownEndpoint x).val ≤ x

Downward-rounded proof endpoints do not exceed their exact real inputs.

theorem NN.MLTheory.CROWN.FP32.le_roundUpEndpoint (x : ℝ) : x ≤ (roundUpEndpoint x).val

Upward-rounded proof endpoints do not fall below their exact real inputs.

theorem NN.MLTheory.CROWN.FP32.normalizationEpsilon_nonneg : 0 ≤ LawfulBoundOps.toReal TorchLean.normalizationEpsilon

FP32 rounds the positive rational stabilizer once; valid rounding preserves nonnegativity.

instance NN.MLTheory.CROWN.FP32.instLawfulNonlinearBoundOps : LawfulNonlinearBoundOps FP32

The rounded-real FP32 nonlinear transfers enclose their exact real meanings.