Backend Views for ODE Enclosures

The generic adapters apply the real-valued corridor theorems to a supplied interpretation toReal : α → ℝ. The FP32 wrappers use TorchLean's rounded-real model.

Continuity, exact derivatives, and corridor inequalities of the interpreted functions remain caller hypotheses. Correct rounding or finite-error bounds alone do not supply these hypotheses: an ordinary sampled floating-point trajectory is not automatically a continuous ODE solution. These adapters establish neither backend numerical soundness nor a certificate-to-ODE bridge.

A directly decoded binary32 trajectory has finite range, so continuity on an interval forces it to be constant. To reason about sampled trajectories, use a real-valued interpolant instead. The corridor theorem still needs the interpolant's clamped-ODE derivative hypothesis; sample values and interval boxes alone do not establish that it solves the ODE.

@[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 : ℝ} {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 : ℝ} {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) {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) {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.

Continuity of a directly decoded binary32 trajectory

@[reducible, inline]

noncomputable abbrev NN.Proofs.Verification.ODE.Enclosure.Backend.ieee32RealView (g : ℝ → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) ieee32RealView._proof_1 ieee32RealView._proof_2 ieee32RealView._proof_3 ieee32RealView._proof_4) : ℝ → ℝ

Real interpretation of an executable IEEE-754 binary32 trajectory.

This view does not establish continuity, derivative identities, or finiteness of the trajectory.

theorem NN.Proofs.Verification.ODE.Enclosure.Backend.ieee32RealView_eq_of_continuousOn (u : ℝ → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) ieee32RealView._proof_1 ieee32RealView._proof_2 ieee32RealView._proof_3 ieee32RealView._proof_4) {a b s t : ℝ} (continuous : ContinuousOn (ieee32RealView u) (Set.Icc a b)) (hs : s ∈ Set.Icc a b) (ht : t ∈ Set.Icc a b) : ieee32RealView u s = ieee32RealView u t

A directly decoded binary32 trajectory that is continuous on an interval is constant there. Use a real-valued interpolant when stating an ODE theorem about discrete samples.