Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL

TL;DR

This paper develops a formal Isabelle/HOL framework connecting local flow properties to global qualitative facts for the SIR epidemic model, ensuring rigorous proof of key epidemiological invariants.

Contribution

It introduces reusable theorem infrastructure linking AFP local flow construction to global properties for the SIR ODE, enhancing formal verification capabilities.

Findings

Proved nonnegativity and conservation of the SIR model within Isabelle/HOL.

Extended local flow to global flow over arbitrary intervals.

Provided reusable scalar lemmas for compartmental equations and monotonicity.

Abstract

We present a mechanically checked Isabelle/HOL bridge from the Picard-Lindelof flow infrastructure in the Archive of Formal Proofs (AFP) to selected qualitative facts for the mass-action, closed-population SIR epidemic ODE. The epidemiological facts are classical; the contribution is reusable theorem infrastructure connecting the AFP local-flow construction to global forward existence, uniqueness, forward invariance of the nonnegative orthant, conservation, monotonicity, the Kermack-McKendrick conserved phase-plane relation, compartment bounds, and threshold-ratio conditions for infectious growth and monotonicity. The proof first establishes sign and conservation facts for local AFP flow segments, then uses the conserved nonnegative simplex as the compactness witness for extending the flow to all forward times. The finite-interval qualitative facts are then transferred to the unique AFP forward flow on arbitrary intervals [0,b] with b>0, so the results apply to the constructed Isabelle/AFP SIR solution rather than to an assumed trajectory. The reusable layer provides homogeneous-linear scalar compartment lemmas for equations X'(t)=f(t)X(t), derivative-sign monotonicity, three-compartment conservation, and an SIR transfer bridge to the AFP flow infrastructure. We do not formalize stability, final-size, or asymptotic theory. The accompanying Isabelle artifact builds with Isabelle 2024 and AFP 2024 and contains no sorry or oops proof placeholders.