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

David B. HulakArthur F. RamosRuy J. G. B. de Queiroz

article2026arXiv0 citations

Develops a fully verified Isabelle/HOL framework connecting local Picard-Lindelöf flows to the global qualitative dynamics of the classic SIR epidemic model, supplying reusable proof infrastructure for analyzing general compartment differential equations.

Listen

Compartmental models that track populations across susceptible, infectious, and recovered stages form the baseline for modern mathematical epidemiology and public health planning. While their general mathematical properties are well known in theory, standard scientific literature frequently relies on informal assumptions regarding underlying physical constraints, such as ensuring population counts never fall below zero or that solutions exist infinitely forward in time. When translating these models into mission-critical software, automated reasoning frameworks, or verified policy simulations, unstated assumptions introduce severe reliability risks.

The article addresses this gap by mechanically checking and certifying the qualitative properties of the classical susceptible-infectious-recovered ordinary differential equation model using the Isabelle/HOL interactive theorem prover. Its main objective is to establish a verified, reusable software bridge connecting foundational differential equation existence theorems to the qualitative behavior of epidemic trajectories without circular mathematical assumptions.

To achieve this, the authors implemented a high-level formalization structured in modular layers. Rather than analyzing numerical trajectories or running empirical simulations, they constructed machine-checked logical proofs within the 2024 releases of Isabelle/HOL and its Archive of Formal Proofs. The proof framework establishes generic calculus lemmas for scalar compartment models, proves sign preservation and conservation on local time segments, and applies a compact continuation principle to safely extend the unique trajectory to all future forward times.

The formal verification produced several core findings. First, it rigorously proves global forward existence and uniqueness from nonnegative initial data, successfully resolving a subtle circularity trap by establishing conservation and nonnegativity on local prefixes before proving that the solution continues indefinitely. Second, it formally confirms the forward invariance and boundedness of the population, ensuring all compartments remain nonnegative and bounded by the initial total population. Third, it certifies the Kermack-McKendrick phase-plane conservation law, proving that epidemic trajectories strictly follow defined level curves. Finally, it proves threshold ratio conditions, certifying that infection declines monotonically over the entire interval whenever the initial effective reproduction threshold ratio is less than or equal to one.

These results demonstrate that classical epidemiological reasoning can be made fully rigorous and integrated directly into certified formal verification environments. For decision-makers and developers in critical modeling, high-assurance software, and biosecurity, this infrastructure lowers compliance and validation risks by replacing informal analytical assumptions with mathematically certified guarantees. Downstream applications can now import verified conservation, sign preservation, and threshold properties as certified theorems rather than re-proving them or treating them as unverified premises.

Moving forward, engineering and research teams building verified epidemiological tools should adopt this modular framework to certify more complex dynamics. Recommended next steps supported by the article include extending the generic calculus library to handle multi-compartment structures with additive source terms (such as exposed stages in SEIR models), indexed multi-group populations, asymptotic terminal size equations, and equilibrium stability analysis.

Confidence in these findings is exceptionally high within the stated boundary conditions, as the codebase contains zero unproven placeholders, axioms, or aborted proof commands across all 11 theory files. However, leaders should note that the model applies strictly to autonomous, closed-population dynamics without vital processes such as births, deaths, vaccination, or seasonal forcing, and the theorems verify structural qualitative dynamics rather than executing numerical simulations.

Microsoft Universidade Federal de Pernambuco formal proofs isabelle/hol ode SIR ODE Isabelle/HOL ODE formalization

arXiv: 2605.02474

No sufficiently relevant recommendations were found.

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

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.

Topics

formal proofs isabelle/hol ode

Keywords

SIR ODE Isabelle/HOL ODE formalization scalar lemmas qualitative analysis differential dynamic logic SIR dynamics

1 Introduction
2 Background
2.1 Isabelle/HOL and HOL-Analysis
2.2 Derivatives in Isabelle
2.3 Integration in Isabelle
2.4 Locales
3 A Reusable Compartmental Framework
3.1 Linear ODE Solution via Integrating Factor
3.2 Scalar Sign Preservation
3.3 Nonnegativity from Nonnegative Derivative
3.4 Three-Compartment Conservation
3.5 Monotonicity Wrappers
3.6 Design Decisions
4 SIR Model Instantiation
4.1 The SIR ODE System
4.2 The Locales SIR_solution and SIR_ODE
4.3 Non-circular Globalization and Flow Bridge
4.4 Formalization Architecture
4.5 Forward Invariance
4.6 Integrating-Factor Integral Representations
4.7 Conservation of Total Population
4.8 Monotonicity
4.9 The Kermack–McKendrick Phase-Plane Invariant
4.10 Epidemic Growth Condition
4.11 Initial Effective Threshold Ratio
4.11.1 Definitions and Notation
4.11.2 Threshold Theorems
4.12 Stationary Infection Condition
4.13 Boundedness
5 Related Work
5.1 ODE Formalization in Isabelle
5.2 Verified Reachability and Hybrid-System Verification
5.3 Formal Epidemiology in Other Proof Assistants
5.4 Positioning
6 Discussion
6.1 What Is Assumed vs. Proved
6.2 The Integrating Factor vs. Picard–Lindelöf
6.3 Proof Engineering Observations
6.4 Scope Boundaries and Limitations
6.5 Artifact Statement
6.6 Using the Theorem Package
6.7 Future Work
7 Conclusion
References

Knowls

Knowl 1 — Non-Circular Global Forward Existence and Flow Bridge for the SIR ODE
theoretical result
In Isabelle/HOL, using the Archive of Formal Proofs (AFP) Picard–Lindelöf infrastructure, the mass-action susceptible–infectious–recovered (SIR) vector field on $\mathbb{R}^3$ with positive parameters $\beta > 0, \gamma > 0$ and nonnegative initial conditions $(S_0, I_0, R_{\text{rec},0})$ has a unique solution that exists for all forward times $t \in [0, \infty)$ .

To avoid circular dependencies where all-time forward invariance is assumed before existence is established, nonnegativity and total population conservation $S(t) + I(t) + R(t) = S_0 + I_0 + R_{\text{rec},0} = N_0$ are proved strictly on local-flow prefixes whose times already belong to the maximal existence interval. These prefix invariants confine the trajectory to the compact 2-simplex:

$K = \left\{(S, I, R) \in \mathbb{R}^3 \;\middle|\; S \ge 0,\; I \ge 0,\; R \ge 0,\; S + I + R = N_0\right\} \subseteq [0, N_0]^3$

Applying the AFP compact-continuation theorem (flow_in_compact_right_existence) with $K$ as the compact witness proves that the maximal right existence interval contains $[0, \infty)$ . Consequently, for every $b > 0$ , the forward flow instantiates the finite-interval solution context (SIR_solution) on $[0, b]$ , and any other differentiable trajectory satisfying the SIR ODE on $[0, b]$ in the same derivative convention with the same initial state coincides pointwise with this flow.
Knowl 2 — Integrating-Factor Representation and Sign Preservation for Scalar Compartment ODEs
theoretical result
Let $f, X : \mathbb{R} \to \mathbb{R}$ be functions on a nondegenerate closed interval $[a, b]$ with $a < b$ , where $f$ is continuous on $[a, b]$ , and $X$ satisfies $(X \text{ has\_real\_derivative } f(t)X(t)) \text{ at } t$ for each $t \in [a, b]$ . Then for all $t \in [a, b]$ :

$X(t) = X(a) \cdot \exp\left( \int_a^t f(s) \, ds \right)$

This explicit representation establishes sign preservation for scalar compartment equations:
- Nonnegativity: If $X(a) \ge 0$ , then $X(t) \ge 0$ for all $t \in [a, b]$ .
- Strict positivity: If $X(a) > 0$ , then $X(t) > 0$ for all $t \in [a, b]$ .
The formal Isabelle/HOL lemmas (linear_ode_solution, linear_ode_nonneg, linear_ode_pos) require full two-sided neighbourhood derivatives across $[a, b]$ , converting within-interval Fundamental Theorem of Calculus derivatives to full derivatives at interior points.
Knowl 3 — Kermack–McKendrick Conserved Phase-Plane Invariant
theoretical result
For any differentiable trajectory $(S, I, R)$ satisfying the classical mass-action SIR system with transmission coefficient $\beta > 0$ and recovery rate $\gamma > 0$ on $[a, b]$ , if the initial susceptible count is strictly positive ( $S(a) > 0$ ), then the Kermack–McKendrick level-curve quantity:

$V(t) = I(t) + S(t) - \frac{\gamma}{\beta} \ln(S(t))$

is constant throughout $[a, b]$ . That is, for all $s, t \in [a, b]$ , $V(s) = V(t)$ .

Equivalently, expressing the invariant relative to initial conditions yields:

$I(t) + S(t) - I(a) - S(a) = \frac{\gamma}{\beta} \ln\left( \frac{S(t)}{S(a)} \right) \quad \text{for all } t \in [a, b]$

Because $S(a) > 0$ implies $S(t) > 0$ for all $t \in [a, b]$ via integrating-factor sign preservation, the real natural logarithm $\ln(S(t))$ and its derivative are well-defined across the entire interval.
Knowl 4 — Effective Threshold Ratios and Infectious Compartment Dynamics
theoretical result
In the unnormalized mass-action SIR model with parameters $\beta > 0$ and $\gamma > 0$ on $[a, b]$ , the initial effective threshold ratio is $\mathcal{R}_{\text{init}} = \frac{\beta S(a)}{\gamma}$ and the time-dependent effective threshold ratio is $\mathcal{R}_{\text{eff}}(t) = \frac{\beta S(t)}{\gamma}$ . The dynamics of the infectious compartment $I$ satisfy:
- Pointwise epidemic growth: For any $t \in [a, b]$ with $I(t) > 0$ , $I'(t) > 0 \iff \mathcal{R}_{\text{eff}}(t) > 1$
- Pointwise initial growth and decline: At $t = a$ , if $I(a) > 0$ :
  - $\mathcal{R}_{\text{init}} > 1 \implies I'(a) > 0$ (initial growth)
  - $\mathcal{R}_{\text{init}} < 1 \implies I'(a) < 0$ (initial decline)
  - $\mathcal{R}_{\text{init}} \le 1 \implies I'(a) \le 0$ (initial non-growth)
- Interval-wide monotonicity: If $\mathcal{R}_{\text{init}} \le 1$ , then $I(t)$ is nonincreasing on the entire interval $[a, b]$ : $\forall s, t \in [a, b]. \; s \le t \implies I(t) \le I(s)$
Here $\mathcal{R}_{\text{init}}$ governs initial growth for the initial state $(S(a), I(a), R(a))$ and is distinct from the fully susceptible disease-free equilibrium quantity $\mathcal{R}_0^{\text{DFE}} = \frac{\beta N}{\gamma}$ whenever $S(a) < N$ .
Knowl 5 — Forward Invariance of the Nonnegative Orthant and Compartment Bounds
theoretical result
For any differentiable solution $(S, I, R)$ to the SIR ODE on $[a, b]$ with $\beta > 0, \gamma > 0$ and initial values $S(a) \ge 0, I(a) \ge 0, R(a) \ge 0$ :
- Forward Invariance: For all $t \in [a, b]$ , $S(t) \ge 0, \quad I(t) \ge 0, \quad R(t) \ge 0$ Nonnegativity of $S$ and $I$ is established independently via integrating factor representations ( $S'(t) = -\beta I(t) S(t)$ and $I'(t) = (\beta S(t) - \gamma) I(t)$ ), while nonnegativity of $R$ is derived from $R'(t) = \gamma I(t) \ge 0$ via derivative-sign monotonicity.
- Integral Representations: $S(t) = S(a) \exp\left( -\beta \int_a^t I(s) \, ds \right), \quad I(t) = I(a) \exp\left( \int_a^t (\beta S(s) - \gamma) \, ds \right)$
- Compartment Boundedness: For initial total population $N = S(a) + I(a) + R(a)$ , combining conservation with nonnegativity gives uniform bounds for each compartment $X \in \{S, I, R\}$ : $0 \le X(t) \le N \quad \text{for all } t \in [a, b]$
Knowl 6 — Three-Compartment Conservation and Derivative-Sign Monotonicity
theoretical result
The generic compartmental framework in Isabelle/HOL provides conservation and monotonicity wrapper theorems for scalar functions on $[a, b]$ with $a < b$ :
- Three-Compartment Conservation: If $f, g, h : \mathbb{R} \to \mathbb{R}$ have full-neighbourhood derivatives $D_f(s), D_g(s), D_h(s)$ satisfying $D_f(s) + D_g(s) + D_h(s) = 0$ for all $s \in [a, b]$ , then: $f(t) + g(t) + h(t) = f(a) + g(a) + h(a) \quad \text{for all } t \in [a, b]$ In the SIR model, the right-hand sides $(-\beta SI) + (\beta SI - \gamma I) + (\gamma I) = 0$ sum to zero, establishing total population conservation $S(t) + I(t) + R(t) = N$ .
- Monotonicity:
  - If $f'(u) \le 0$ on $[s, t]$ , then $f(t) \le f(s)$ . For SIR, $S'(t) = -\beta S(t)I(t) \le 0$ implies $S$ is nonincreasing.
  - If $f'(u) \ge 0$ on $[s, t]$ , then $f(s) \le f(t)$ . For SIR, $R'(t) = \gamma I(t) \ge 0$ implies $R$ is nondecreasing.
Knowl 7 — Stationary Infection Characterization in the SIR Model
theoretical result
For a trajectory $(S, I, R)$ satisfying the SIR ODE on $[a, b]$ with parameters $\beta > 0, \gamma > 0$ , at any time $t \in [a, b]$ where the infectious population is strictly positive ( $I(t) > 0$ ), the time derivative of $I$ vanishes if and only if the susceptible population equals $\gamma/\beta$ :

$\beta S(t)I(t) - \gamma I(t) = 0 \iff S(t) = \frac{\gamma}{\beta}$

This characterizes the necessary algebraic condition for an interior critical point (stationary inflection or extremum) of $I(t)$ . The formalization does not prove the existence, uniqueness, or crossing of such a point.
Knowl 8 — Locale Architecture for Compartmental Models and the SIR ODE
model/method
The Isabelle/HOL formalization is organized into three distinct layers:
1. Generic Framework (Compartmental_Model.thy): Provides parameter-independent lemmas for homogeneous-linear scalar ODEs ( $X'(t) = f(t)X(t)$ ), integrating-factor representations, sign preservation, derivative-sign monotonicity wrappers, and three-compartment zero-sum conservation.
2. Finite-Interval SIR Locale (SIR_solution in SIR_Defs.thy): Fixes $\beta, \gamma, S, I, R, a, b$ with assumptions $\beta > 0, \gamma > 0, a < b$ , initial nonnegativity $S(a), I(a), R(a) \ge 0$ , and the full-neighbourhood derivative equations on $[a, b]$ : $\frac{dS}{dt} = -\beta SI, \quad \frac{dI}{dt} = \beta SI - \gamma I, \quad \frac{dR}{dt} = \gamma I$ All finite-interval qualitative properties (invariance, monotonicity, Kermack–McKendrick invariant, threshold behavior, bounds) are proved inside this locale.
3. Flow Bridge (SIR_ODE in SIR_Existence.thy): Proves that the $\mathbb{R}^3$ polynomial SIR vector field is $C^1$ , instantiates the AFP Picard–Lindelöf flow, proves global forward existence via compact continuation, and interprets SIR_solution on $[0, b]$ for any $b > 0$ .
Knowl 9 — Scope Boundaries and Limitations of the Certified SIR Model
limitation
The formalization is subject to several explicit scope boundaries:
- Epidemiological Scope: Restricted to the basic autonomous, closed-population mass-action SIR system without vital dynamics (births/deaths), vaccination, age groups, or spatial heterogeneity. Standard-incidence formulations ( $\beta SI / N$ ) and nonautonomous forced systems are not covered.
- Dynamical and Asymptotic Scope: Does not formalize equilibrium stability (local or global), asymptotic limits as $t \to \infty$ , existence or uniqueness of an infection peak time where $S(t) = \gamma/\beta$ , or the implicit final-size transcendental equation.
- Dimensional Tracking: Variables and parameters are untyped real numbers (real); dimensional consistency of parameters and logarithmic quantities (such as $\ln(S(t))$ ) is not verified.
- Framework Generality: Conservation is proved specifically for three compartments rather than an arbitrary $n$ -compartment sum, and scalar lemmas do not support affine source terms ( $X'(t) = f(t)X(t) + g(t)$ ).
- Computational Scope: The formalization is purely logical theorem infrastructure and does not provide an executable numerical simulator via code generation.

Knowl 10 — Artifact Structure and Source-Level Verification Metrics

data/table

The formalization is packaged as an Isabelle 2024 / AFP 2024 session with zero sorry placeholders, zero oops aborts, and no axiomatization, axioms, or oracle commands. The 11 theory files comprise 2,049 raw lines of Isabelle/HOL across three modules:

Theory Module	Source Files	Raw Lines
Generic Framework	theories/Framework/Compartmental_Model.thy	220
SIR Qualitative Theories	theories/SIR/*.thy (8 files)	808
Existence Bridge Flow	work/SIR_Existence.thy, work/SIR_Main.thy (2 files)	1021
Total	11 files	2049

The generic framework contains 7 named declarations; the scalar SIR theories contain 45 named declarations; and the existence bridge contains 54 named declarations. The full session builds in approximately 34 seconds of wall-clock time on a 4-vCPU AMD EPYC machine with 7.8 GiB RAM.

Coverage note — None was omitted; all contributed qualitative theorems, generic scalar lemmas, flow globalization results, architecture details, and stated limitations are represented.

References

1.R. M. Anderson and R. M. May. Infectious Diseases of Humans: Dynamics and Control. Oxford University Press, 1991. doi:10.1093/oso/9780198545996.001.0001.
2.C. Ballarin. Locales: A module system for mathematical theories. Journal of Automated Reasoning, 52(2):123–153, 2014. doi:10.1007/s10817-013-9284-7.
3.S. Boldo, C. Lelay, and G. Melquiond. Coquelicot: A user-friendly library of real analysis for Coq. Mathematics in Computer Science, 9(1):41–62, 2015. doi:10.1007/s11786-014-0181-1.
4.F. Brauer and C. Castillo-Chávez. Mathematical Models in Population Biology and Epidemiology, volume 40 of Texts in Applied Mathematics. Springer, 2nd edition, 2012. doi:10.1007/978-1-4614-1686-9.
5.F. Brauer, C. Castillo-Chávez, and Z. Feng. Mathematical Models in Epidemiology, volume 69 of Texts in Applied Mathematics. Springer, 2019. doi:10.1007/978-1-4939-9828-9.
6.F. Ciocchetta and J. Hillston. Bio-PEPA: A framework for the modelling and analysis of biological systems. Theoretical Computer Science, 410(33–34):3065–3084, 2009. doi:10.1016/j.tcs.2009.02.037.
7.O. Diekmann, H. Heesterbeek, and T. Britton. Mathematical Tools for Understanding Infectious Disease Dynamics. Princeton Series in Theoretical and Computational Biology. Princeton University Press, 2013.
8.O. Diekmann and J. A. P. Heesterbeek. Mathematical Epidemiology of Infectious Diseases: Model Building, Analysis and Interpretation. Wiley, 2000.
9.O. Diekmann, J. A. P. Heesterbeek, and J. A. J. Metz. On the definition and the computation of the basic reproduction ratio $R_0$ in models for infectious diseases in heterogeneous populations. Journal of Mathematical Biology, 28(4):365–382, 1990. doi:10.1007/BF00178324.
10.O. Diekmann, J. A. P. Heesterbeek, and M. G. Roberts. The construction of next-generation matrices for compartmental epidemic models. Journal of the Royal Society Interface, 7(47):873–885, 2010. doi:10.1098/rsif.2009.0386.
11.J. Fisher and T. A. Henzinger. Executable cell biology. Nature Biotechnology, 25(11):1239–1249, 2007. doi:10.1038/nbt1356.
12.N. Fulton. Analyzing disease spread models using a theorem prover. Web note, 2020. https://nfulton.org/2020/03/27/SIR-Models-In-KeYmaeraX/, last checked 3 May 2026.
13.N. Fulton, S. Mitsch, J.-D. Quesel, M. Völp, and A. Platzer. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In Automated Deduction – CADE-25, volume 9195 of LNCS, pages 527–538. Springer, 2015. doi:10.1007/978-3-319-21401-6_36.
14.J. Harrison. The HOL Light theory of euclidean space. Journal of Automated Reasoning, 50(2):173–190, 2013. doi:10.1007/s10817-012-9250-9.
15.H. W. Hethcote. Qualitative analyses of communicable disease models. Mathematical Biosciences, 28(3–4):335–356, 1976. doi:10.1016/0025-5564(76)90132-2.
16.H. W. Hethcote. The mathematics of infectious diseases. SIAM Review, 42(4):599–653, 2000. doi:10.1137/S0036144500371907.
17.J. Hölzl. Markov models. Archive of Formal Proofs, 2012. Archive of Formal Proofs entry, https://www.isa-afp.org/entries/Markov_Models.html.
18.J. Hölzl, F. Immler, and B. Huffman. Type classes and filters for mathematical analysis in Isabelle/HOL. In Interactive Theorem Proving (ITP 2013), volume 7998 of LNCS, pages 279–294. Springer, 2013. doi:10.1007/978-3-642-39634-2_21.
19.F. Immler. Verified reachability analysis of continuous systems. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015), volume 9035 of LNCS, pages 37–51. Springer, 2015. doi:10.1007/978-3-662-46681-0_3.
20.F. Immler. A verified ODE solver and the Lorenz attractor. Journal of Automated Reasoning, 61(1–4):73–111, 2018. doi:10.1007/s10817-017-9448-y.
21.F. Immler and J. Hölzl. Numerical analysis of ordinary differential equations in Isabelle/HOL. In Interactive Theorem Proving (ITP 2012), volume 7406 of LNCS, pages 377–392. Springer, 2012. doi:10.1007/978-3-642-32347-8_26.
22.F. Immler and J. Hölzl. Ordinary differential equations. Archive of Formal Proofs, 2012. Archive of Formal Proofs entry, https://www.isa-afp.org/entries/Ordinary_Differential_Equations.html.
23.F. Immler and Y. K. Tan. The Poincaré-Bendixson theorem in Isabelle/HOL. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 338–352. ACM, 2020. doi:10.1145/3372885.3373833.
24.W. O. Kermack and A. G. McKendrick. A contribution to the mathematical theory of epidemics. Proceedings of the Royal Society A, 115(772):700–721, 1927. doi:10.1098/rspa.1927.0118.
25.M. Maggesi. A formalization of metric spaces in HOL Light. Journal of Automated Reasoning, 60(2):237–254, 2018. doi:10.1007/s10817-017-9412-x.
26.E. Makarov and B. Spitters. The Picard algorithm for ordinary differential equations in Coq. In Interactive Theorem Proving (ITP 2013), volume 7998 of LNCS, pages 463–468. Springer, 2013. doi:10.1007/978-3-642-39634-2_34.
27.J. D. Murray. Mathematical Biology I: An Introduction, volume 17 of Interdisciplinary Applied Mathematics. Springer, 3rd edition, 2002. doi:10.1007/b98868.
28.M. Nagumo. Über die lage der integralkurven gewöhnlicher differentialgleichungen. Proceedings of the Physico-Mathematical Society of Japan. 3rd Series, 24:551–559, 1942.
29.T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. doi:10.1007/3-540-45949-9.
30.S. Park and H. Thies. A Coq formalization of Taylor models and power series for solving ordinary differential equations. In 15th International Conference on Interactive Theorem Proving (ITP 2024), volume 309 of Leibniz International Proceedings in Informatics (LIPIcs), pages 30:1–30:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPIcs.ITP.2024.30.
31.A. Platzer. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 41(2):143–189, 2008. doi:10.1007/s10817-008-9103-8.
32.A. Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018. doi:10.1007/978-3-319-63588-0.
33.Y. K. Tan and A. Platzer. An axiomatic approach to existence and liveness for differential equations. Formal Aspects of Computing, 33(4):461–518, 2021. doi:10.1007/s00165-020-00525-0.
34.G. Teschl. Ordinary Differential Equations and Dynamical Systems, volume 140 of Graduate Studies in Mathematics. American Mathematical Society, 2012.
35.The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 367–381. ACM, 2020. doi:10.1145/3372885.3373824.
36.P. van den Driessche and J. Watmough. Reproduction numbers and sub-threshold endemic equilibria for compartmental models of disease transmission. Mathematical Biosciences, 180:29–48, 2002. doi:10.1016/S0025-5564(02)00108-6.
37.M. Wenzel. Isabelle/Isar—a Versatile Environment for Human-Readable Formal Proof Documents. PhD thesis, Technische Universität München, 2002. https://isabelle.in.tum.de/Isar/isar-thesis-Isabelle2002.pdf.

Citation

MLA

Hulak, D. B., et al. “Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL”. arXiv, 2026, http://arxiv.org/abs/2605.02474v1.

APA

Hulak, D. B., Ramos, A. F., & Queiroz, R. J. G. B. de . (2026). Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL. arXiv. http://arxiv.org/abs/2605.02474v1

Chicago

Hulak, D. B., A. F. Ramos, and R. J. G. B. de . Queiroz. 2026. “Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL”. arXiv. http://arxiv.org/abs/2605.02474v1.

Harvard

Hulak, D.B., Ramos, A.F. and Queiroz, R.J.G.B. de . (2026) “Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL”, arXiv [Preprint]. Available at: http://arxiv.org/abs/2605.02474v1.

Vancouver

1. Hulak DB, Ramos AF, Queiroz RJGB de (2026) Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL. arXiv

BibTeX

@article{hulak2026certified,
  title = {Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL},
  author = {Hulak, David B. and Ramos, Arthur F. and Queiroz, Ruy J. G. B. de},
  year = {2026},
  journal = {arXiv},
  url = {http://arxiv.org/abs/2605.02474v1},
  eprint = {2605.02474}
}

Metadata:arXiv

Access the Paper

This paper is available from its original source. Click below to access the PDF.

Open PDF

License: https://creativecommons.org/licenses/by/4.0/

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

Abstract

Topics

Keywords

Table of Contents

Knowls

Knowl 1 — Non-Circular Global Forward Existence and Flow Bridge for the SIR ODE

Knowl 2 — Integrating-Factor Representation and Sign Preservation for Scalar Compartment ODEs

Knowl 3 — Kermack–McKendrick Conserved Phase-Plane Invariant

Knowl 4 — Effective Threshold Ratios and Infectious Compartment Dynamics

Knowl 5 — Forward Invariance of the Nonnegative Orthant and Compartment Bounds

Knowl 6 — Three-Compartment Conservation and Derivative-Sign Monotonicity

Knowl 7 — Stationary Infection Characterization in the SIR Model

Knowl 8 — Locale Architecture for Compartmental Models and the SIR ODE

Knowl 9 — Scope Boundaries and Limitations of the Certified SIR Model

Knowl 10 — Artifact Structure and Source-Level Verification Metrics

References

Citation

BibTeX

Access the Paper