ODE Corridor Enclosures

This file formalizes the real-analysis endpoint used by Tanaka and Yatabe, Learn and Verify: A Framework for Rigorous Verification of Physics-Informed Neural Networks, arXiv:2601.19818.

The paper trains candidate lower/upper PINN corridors and then verifies, using interval arithmetic, that they are sub- and super-solutions of a scalar ODE. Once those inequalities are certified, the mathematical argument is independent of the neural-network producer:

1. Local corridor enclosure. A solution of the clamped ODE u' = f(t, clampToCorridor uL uU t (u t)) cannot cross the verified corridor [uL(t), uU(t)]. Inside the corridor, clamping is a no-op, so the same trajectory solves the original ODE u' = f(t,u).
2. Constant-extension enclosure. The finite-time corridor can be extended after T by holding both walls constant, provided the paper's sign/monotonicity hypotheses for f hold beyond T.

The proof is deliberately stated over exact ℝ functions. Floating-point or executable backends must first justify these real hypotheses; EnclosureBackends.lean only reuses this theorem through backend toReal views. This keeps the trust boundary sharp.

Corridor clamping

def NN.Proofs.Verification.ODE.Enclosure.clampToCorridor (uL uU : ℝ → ℝ) (t u : ℝ) : ℝ

The paper's truncation function 𝒯u(t) (Eq. 16), named here by what it does: clamp the current value into the certified corridor [uL(t), uU(t)].

If u is below the lower wall we feed the vector field uL(t); if it is above the upper wall we feed uU(t); otherwise we feed u itself. The enclosure theorem then proves the clamped solution never actually needs those emergency branches.

theorem NN.Proofs.Verification.ODE.Enclosure.clampToCorridor_def (uL uU : ℝ → ℝ) (t u : ℝ) : clampToCorridor uL uU t u = max (uL t) (min (uU t) u)

Unfolding lemma for clampToCorridor.

theorem NN.Proofs.Verification.ODE.Enclosure.clampToCorridor_eq_self {uL uU : ℝ → ℝ} {t u : ℝ} (hL : uL t ≤ u) (hU : u ≤ uU t) : clampToCorridor uL uU t u = u

If u is already within the corridor, clamping is a no-op.

theorem NN.Proofs.Verification.ODE.Enclosure.clampToCorridor_eq_upper {uL uU : ℝ → ℝ} {t u : ℝ} (hLU : uL t ≤ uU t) (hU : uU t < u) : clampToCorridor uL uU t u = uU t

If u lies strictly above the corridor, clamping snaps to the upper wall.

theorem NN.Proofs.Verification.ODE.Enclosure.clampToCorridor_eq_lower {uL uU : ℝ → ℝ} {t u : ℝ} (hLU : uL t ≤ uU t) (hL : u < uL t) : clampToCorridor uL uU t u = uL t

If u lies strictly below the corridor, clamping snaps to the lower wall.

Local corridor enclosure

This is the comparison theorem used in the paper's local enclosure result. It is a “no first crossing” statement: if u evolves according to the clamped ODE u' = f(t, clampToCorridor uL uU t (u t)), and uL,uU are a sub- and super-solution pair for the original ODE, then u cannot leave the corridor.

We implement this by reducing to mathlib’s 1D fencing theorem image_le_of_deriv_right_lt_deriv_boundary' twice:

1. an upper fence u ≤ uU + ε(1+t) for any ε>0;
2. a lower fence via the same argument applied to -u.

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

Core local corridor theorem:

If u solves the clamped ODE (right-derivative form), and uL,uU are sub- and super-solutions for the original ODE, then u is trapped between uL and uU on [0,T].

This corresponds to the paper's local enclosure result, but the public Lean name describes the mathematical content rather than the theorem number.

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

Local unclamping theorem.

Once the local enclosure proves uL(t) ≤ u(t) ≤ uU(t), the clamp is definitionally equal to u(t). So a solution of the clamped ODE is not merely enclosed; it also solves the original ODE on the same interval. This is the exact real-analysis contract that interval/PINN certificate producers must establish before TorchLean can claim a verified ODE solve.

Constant-extension corridor

noncomputable def NN.Proofs.Verification.ODE.Enclosure.constantExtensionAfter (T : ℝ) (g : ℝ → ℝ) : ℝ → ℝ

Constant extension used by the paper's global-time argument: follow g until the verified time horizon T, then freeze it at g T.

The function is intentionally right-derivative friendly. At and after T, viewed from the right-neighborhood Ici t, the extension is locally constant and has derivative zero.

@[simp]

theorem NN.Proofs.Verification.ODE.Enclosure.constantExtensionAfter_of_le {T : ℝ} {g : ℝ → ℝ} {t : ℝ} (ht : t ≤ T) : constantExtensionAfter T g t = g t

On the left side of the switching time (t ≤ T), the extension agrees with g.

@[simp]

theorem NN.Proofs.Verification.ODE.Enclosure.constantExtensionAfter_of_gt {T : ℝ} {g : ℝ → ℝ} {t : ℝ} (ht : T < t) : constantExtensionAfter T g t = g T

On the right side of the switching time (T < t), the extension is constant g T.

The next two lemmas provide derivatives for constantExtensionAfter T g:

• strictly before T, the derivative matches g' because the extension and g agree locally;
• at/after T, the derivative is zero because the extension is locally constant there when viewed within the right-derivative filter 𝓝[Ici t] t).

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

Constant-extension enclosure theorem:

Assume we have uL,uU on [0,T] satisfying the local corridor hypotheses, and assume the paper's extra sign/monotonicity conditions for f beyond T. Then for any τ ≥ T, any solution u of the clamped ODE built from the constant extensions is enclosed on [0,τ] and is a genuine solution of u' = f(t,u) on [0,τ].

This is the reusable Lean form of the paper's global-in-time step: after the verified horizon, the walls stop moving, and the vector field points inward at those frozen walls.