Backend Views for ODE Enclosures

Enclosure.lean proves the ODE corridor theorems over exact real-valued functions. The executable verification pipeline, however, often evaluates candidate PINN corridors in concrete numeric backends:

• TorchLean.Floats.FP32, our proof-level binary32-style rounded real model;
• TorchLean.Floats.IEEE754.IEEE32Exec, the executable IEEE-754 binary32 bridge.

This file does not prove that those backends are numerically sound by itself. Instead, it gives the clean final adapters: if the backend-valued functions satisfy the real hypotheses after applying their toReal interpretation, then the real ODE enclosure theorem applies.

That is the same trust split used by Tanaka and Yatabe's learn-and-verify framework (arXiv:2601.19818): interval/CROWN/IBP machinery verifies inequalities for a concrete producer, while the ODE comparison theorem consumes the resulting real inequalities.

@[reducible, inline]

abbrev NN.Proofs.Verification.ODE.Enclosure.Backend.realView {α : Type} (toReal : α → ℝ) (g : ℝ → α) : ℝ → ℝ

Interpret a backend-valued trajectory g : ℝ → α as a real-valued function via toReal.

Local corridor wrapper

theorem NN.Proofs.Verification.ODE.Enclosure.Backend.LocalCorridor.fromRealView {α : Type} (toReal : α → ℝ) {T : ℝ} (hT : 0 ≤ T) {f : ℝ → ℝ → ℝ} {u uL uU uL' uU' : ℝ → α} {a : ℝ} (hu_cont : ContinuousOn (realView toReal u) (Set.Icc 0 T)) (hu_der : ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt (realView toReal u) (f t (clampToCorridor (realView toReal uL) (realView toReal uU) t (realView toReal u t))) (Set.Ici t) t) (hu0 : realView toReal u 0 = a) (hL_cont : ContinuousOn (realView toReal uL) (Set.Icc 0 T)) (hL_der : ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt (realView toReal uL) (realView toReal uL' t) (Set.Ici t) t) (hL_sub : ∀ t ∈ Set.Ico 0 T, realView toReal uL' t ≤ f t (realView toReal uL t)) (hL0 : realView toReal uL 0 ≤ a) (hU_cont : ContinuousOn (realView toReal uU) (Set.Icc 0 T)) (hU_der : ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt (realView toReal uU) (realView toReal uU' t) (Set.Ici t) t) (hU_sup : ∀ t ∈ Set.Ico 0 T, f t (realView toReal uU t) ≤ realView toReal uU' t) (hU0 : a ≤ realView toReal uU 0) (hLU : ∀ t ∈ Set.Icc 0 T, realView toReal uL t ≤ realView toReal uU t) : (∀ t ∈ Set.Icc 0 T, realView toReal uL t ≤ realView toReal u t ∧ realView toReal u t ≤ realView toReal uU t) ∧ ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt (realView toReal u) (f t (realView toReal u t)) (Set.Ici t) t

Generic backend wrapper for the local corridor theorem.

The hypotheses are deliberately phrased over realView toReal ...: a caller must already have translated backend computations into real continuity, derivative, and inequality facts. Given those facts, the result is the same enclosure + unclamping statement for the backend trajectory's real interpretation.

theorem NN.Proofs.Verification.ODE.Enclosure.Backend.LocalCorridor.forFP32 {T : ℝ} (hT : 0 ≤ T) {f : ℝ → ℝ → ℝ} {u uL uU uL' uU' : ℝ → TorchLean.Floats.FP32} {a : ℝ} (hu_cont : ContinuousOn (realView TorchLean.Floats.FP32.toReal u) (Set.Icc 0 T)) (hu_der : ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt (realView TorchLean.Floats.FP32.toReal u) (f t (clampToCorridor (realView TorchLean.Floats.FP32.toReal uL) (realView TorchLean.Floats.FP32.toReal uU) t (realView TorchLean.Floats.FP32.toReal u t))) (Set.Ici t) t) (hu0 : realView TorchLean.Floats.FP32.toReal u 0 = a) (hL_cont : ContinuousOn (realView TorchLean.Floats.FP32.toReal uL) (Set.Icc 0 T)) (hL_der : ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt (realView TorchLean.Floats.FP32.toReal uL) (realView TorchLean.Floats.FP32.toReal uL' t) (Set.Ici t) t) (hL_sub : ∀ t ∈ Set.Ico 0 T, realView TorchLean.Floats.FP32.toReal uL' t ≤ f t (realView TorchLean.Floats.FP32.toReal uL t)) (hL0 : realView TorchLean.Floats.FP32.toReal uL 0 ≤ a) (hU_cont : ContinuousOn (realView TorchLean.Floats.FP32.toReal uU) (Set.Icc 0 T)) (hU_der : ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt (realView TorchLean.Floats.FP32.toReal uU) (realView TorchLean.Floats.FP32.toReal uU' t) (Set.Ici t) t) (hU_sup : ∀ t ∈ Set.Ico 0 T, f t (realView TorchLean.Floats.FP32.toReal uU t) ≤ realView TorchLean.Floats.FP32.toReal uU' t) (hU0 : a ≤ realView TorchLean.Floats.FP32.toReal uU 0) (hLU : ∀ t ∈ Set.Icc 0 T, realView TorchLean.Floats.FP32.toReal uL t ≤ realView TorchLean.Floats.FP32.toReal uU t) : (∀ t ∈ Set.Icc 0 T, realView TorchLean.Floats.FP32.toReal uL t ≤ realView TorchLean.Floats.FP32.toReal u t ∧ realView TorchLean.Floats.FP32.toReal u t ≤ realView TorchLean.Floats.FP32.toReal uU t) ∧ ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt (realView TorchLean.Floats.FP32.toReal u) (f t (realView TorchLean.Floats.FP32.toReal u t)) (Set.Ici t) t

Specialization of fromRealView to TorchLean's proof-level FP32 model.

Constant-extension wrapper

theorem NN.Proofs.Verification.ODE.Enclosure.Backend.ConstantExtension.fromRealView {α : Type} (toReal : α → ℝ) {T τ : ℝ} (hT : 0 ≤ T) (hτ : T ≤ τ) {f : ℝ → ℝ → ℝ} {u uL uU uL' uU' : ℝ → α} {a : ℝ} (hu_cont : ContinuousOn (realView toReal u) (Set.Icc 0 τ)) (hu_der : ∀ t ∈ Set.Ico 0 τ, HasDerivWithinAt (realView toReal u) (f t (clampToCorridor (constantExtensionAfter T (realView toReal uL)) (constantExtensionAfter T (realView toReal uU)) t (realView toReal u t))) (Set.Ici t) t) (hu0 : realView toReal u 0 = a) (hL_cont : ContinuousOn (realView toReal uL) (Set.Icc 0 T)) (hL_der : ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt (realView toReal uL) (realView toReal uL' t) (Set.Ici t) t) (hL_sub : ∀ t ∈ Set.Ico 0 T, realView toReal uL' t ≤ f t (realView toReal uL t)) (hL0 : realView toReal uL 0 ≤ a) (hU_cont : ContinuousOn (realView toReal uU) (Set.Icc 0 T)) (hU_der : ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt (realView toReal uU) (realView toReal uU' t) (Set.Ici t) t) (hU_sup : ∀ t ∈ Set.Ico 0 T, f t (realView toReal uU t) ≤ realView toReal uU' t) (hU0 : a ≤ realView toReal uU 0) (hLU : ∀ t ∈ Set.Icc 0 T, realView toReal uL t ≤ realView toReal uU t) (hLower : ∀ (t : ℝ), T < t → 0 ≤ f T (realView toReal uL T) ∧ f T (realView toReal uL T) ≤ f t (realView toReal uL T)) (hUpper : ∀ (t : ℝ), T < t → f t (realView toReal uU T) ≤ f T (realView toReal uU T) ∧ f T (realView toReal uU T) ≤ 0) : (∀ t ∈ Set.Icc 0 τ, constantExtensionAfter T (realView toReal uL) t ≤ realView toReal u t ∧ realView toReal u t ≤ constantExtensionAfter T (realView toReal uU) t) ∧ ∀ t ∈ Set.Ico 0 τ, HasDerivWithinAt (realView toReal u) (f t (realView toReal u t)) (Set.Ici t) t

Generic backend wrapper for the constant-extension theorem.

The corridor is interpreted as real-valued first and then frozen after T with constantExtensionAfter. This mirrors the paper's global step while keeping all backend arithmetic outside this proof.

theorem NN.Proofs.Verification.ODE.Enclosure.Backend.ConstantExtension.forFP32 {T τ : ℝ} (hT : 0 ≤ T) (hτ : T ≤ τ) {f : ℝ → ℝ → ℝ} {u uL uU uL' uU' : ℝ → TorchLean.Floats.FP32} {a : ℝ} (hu_cont : ContinuousOn (realView TorchLean.Floats.FP32.toReal u) (Set.Icc 0 τ)) (hu_der : ∀ t ∈ Set.Ico 0 τ, HasDerivWithinAt (realView TorchLean.Floats.FP32.toReal u) (f t (clampToCorridor (constantExtensionAfter T (realView TorchLean.Floats.FP32.toReal uL)) (constantExtensionAfter T (realView TorchLean.Floats.FP32.toReal uU)) t (realView TorchLean.Floats.FP32.toReal u t))) (Set.Ici t) t) (hu0 : realView TorchLean.Floats.FP32.toReal u 0 = a) (hL_cont : ContinuousOn (realView TorchLean.Floats.FP32.toReal uL) (Set.Icc 0 T)) (hL_der : ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt (realView TorchLean.Floats.FP32.toReal uL) (realView TorchLean.Floats.FP32.toReal uL' t) (Set.Ici t) t) (hL_sub : ∀ t ∈ Set.Ico 0 T, realView TorchLean.Floats.FP32.toReal uL' t ≤ f t (realView TorchLean.Floats.FP32.toReal uL t)) (hL0 : realView TorchLean.Floats.FP32.toReal uL 0 ≤ a) (hU_cont : ContinuousOn (realView TorchLean.Floats.FP32.toReal uU) (Set.Icc 0 T)) (hU_der : ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt (realView TorchLean.Floats.FP32.toReal uU) (realView TorchLean.Floats.FP32.toReal uU' t) (Set.Ici t) t) (hU_sup : ∀ t ∈ Set.Ico 0 T, f t (realView TorchLean.Floats.FP32.toReal uU t) ≤ realView TorchLean.Floats.FP32.toReal uU' t) (hU0 : a ≤ realView TorchLean.Floats.FP32.toReal uU 0) (hLU : ∀ t ∈ Set.Icc 0 T, realView TorchLean.Floats.FP32.toReal uL t ≤ realView TorchLean.Floats.FP32.toReal uU t) (hLower : ∀ (t : ℝ), T < t → 0 ≤ f T (realView TorchLean.Floats.FP32.toReal uL T) ∧ f T (realView TorchLean.Floats.FP32.toReal uL T) ≤ f t (realView TorchLean.Floats.FP32.toReal uL T)) (hUpper : ∀ (t : ℝ), T < t → f t (realView TorchLean.Floats.FP32.toReal uU T) ≤ f T (realView TorchLean.Floats.FP32.toReal uU T) ∧ f T (realView TorchLean.Floats.FP32.toReal uU T) ≤ 0) : (∀ t ∈ Set.Icc 0 τ, constantExtensionAfter T (realView TorchLean.Floats.FP32.toReal uL) t ≤ realView TorchLean.Floats.FP32.toReal u t ∧ realView TorchLean.Floats.FP32.toReal u t ≤ constantExtensionAfter T (realView TorchLean.Floats.FP32.toReal uU) t) ∧ ∀ t ∈ Set.Ico 0 τ, HasDerivWithinAt (realView TorchLean.Floats.FP32.toReal u) (f t (realView TorchLean.Floats.FP32.toReal u t)) (Set.Ici t) t

Specialization of fromRealView to TorchLean's proof-level FP32 model.

IEEE32Exec wrappers

@[reducible, inline]

noncomputable abbrev NN.Proofs.Verification.ODE.Enclosure.Backend.ieee32RealView (g : ℝ → TorchLean.Floats.IEEE754.IEEE32Exec) : ℝ → ℝ

Real interpretation of an executable IEEE-754 binary32 trajectory.

This is intentionally just toReal. Rounding/error guarantees have to be proved before these wrappers are invoked; this abbreviation only keeps theorem statements readable.

theorem NN.Proofs.Verification.ODE.Enclosure.Backend.LocalCorridor.forIEEE32Exec {T : ℝ} (hT : 0 ≤ T) {f : ℝ → ℝ → ℝ} {u uL uU uL' uU' : ℝ → TorchLean.Floats.IEEE754.IEEE32Exec} {a : ℝ} (hu_cont : ContinuousOn (ieee32RealView u) (Set.Icc 0 T)) (hu_der : ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt (ieee32RealView u) (f t (clampToCorridor (ieee32RealView uL) (ieee32RealView uU) t (ieee32RealView u t))) (Set.Ici t) t) (hu0 : ieee32RealView u 0 = a) (hL_cont : ContinuousOn (ieee32RealView uL) (Set.Icc 0 T)) (hL_der : ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt (ieee32RealView uL) (ieee32RealView uL' t) (Set.Ici t) t) (hL_sub : ∀ t ∈ Set.Ico 0 T, ieee32RealView uL' t ≤ f t (ieee32RealView uL t)) (hL0 : ieee32RealView uL 0 ≤ a) (hU_cont : ContinuousOn (ieee32RealView uU) (Set.Icc 0 T)) (hU_der : ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt (ieee32RealView uU) (ieee32RealView uU' t) (Set.Ici t) t) (hU_sup : ∀ t ∈ Set.Ico 0 T, f t (ieee32RealView uU t) ≤ ieee32RealView uU' t) (hU0 : a ≤ ieee32RealView uU 0) (hLU : ∀ t ∈ Set.Icc 0 T, ieee32RealView uL t ≤ ieee32RealView uU t) : (∀ t ∈ Set.Icc 0 T, ieee32RealView uL t ≤ ieee32RealView u t ∧ ieee32RealView u t ≤ ieee32RealView uU t) ∧ ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt (ieee32RealView u) (f t (ieee32RealView u t)) (Set.Ici t) t

Local corridor theorem specialized to the executable IEEE-754 binary32 backend.

theorem NN.Proofs.Verification.ODE.Enclosure.Backend.ConstantExtension.forIEEE32Exec {T τ : ℝ} (hT : 0 ≤ T) (hτ : T ≤ τ) {f : ℝ → ℝ → ℝ} {u uL uU uL' uU' : ℝ → TorchLean.Floats.IEEE754.IEEE32Exec} {a : ℝ} (hu_cont : ContinuousOn (ieee32RealView u) (Set.Icc 0 τ)) (hu_der : ∀ t ∈ Set.Ico 0 τ, HasDerivWithinAt (ieee32RealView u) (f t (clampToCorridor (constantExtensionAfter T (ieee32RealView uL)) (constantExtensionAfter T (ieee32RealView uU)) t (ieee32RealView u t))) (Set.Ici t) t) (hu0 : ieee32RealView u 0 = a) (hL_cont : ContinuousOn (ieee32RealView uL) (Set.Icc 0 T)) (hL_der : ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt (ieee32RealView uL) (ieee32RealView uL' t) (Set.Ici t) t) (hL_sub : ∀ t ∈ Set.Ico 0 T, ieee32RealView uL' t ≤ f t (ieee32RealView uL t)) (hL0 : ieee32RealView uL 0 ≤ a) (hU_cont : ContinuousOn (ieee32RealView uU) (Set.Icc 0 T)) (hU_der : ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt (ieee32RealView uU) (ieee32RealView uU' t) (Set.Ici t) t) (hU_sup : ∀ t ∈ Set.Ico 0 T, f t (ieee32RealView uU t) ≤ ieee32RealView uU' t) (hU0 : a ≤ ieee32RealView uU 0) (hLU : ∀ t ∈ Set.Icc 0 T, ieee32RealView uL t ≤ ieee32RealView uU t) (hLower : ∀ (t : ℝ), T < t → 0 ≤ f T (ieee32RealView uL T) ∧ f T (ieee32RealView uL T) ≤ f t (ieee32RealView uL T)) (hUpper : ∀ (t : ℝ), T < t → f t (ieee32RealView uU T) ≤ f T (ieee32RealView uU T) ∧ f T (ieee32RealView uU T) ≤ 0) : (∀ t ∈ Set.Icc 0 τ, constantExtensionAfter T (ieee32RealView uL) t ≤ ieee32RealView u t ∧ ieee32RealView u t ≤ constantExtensionAfter T (ieee32RealView uU) t) ∧ ∀ t ∈ Set.Ico 0 τ, HasDerivWithinAt (ieee32RealView u) (f t (ieee32RealView u t)) (Set.Ici t) t

Constant-extension theorem specialized to the executable IEEE-754 binary32 backend.