Verified Compartmental Models

A reusable Isabelle/HOL framework for certified reasoning about compartmental ODE models, with the classical SIR epidemic model as the flagship instantiation.

Overview

This project provides machine-checked formalizations of:

• Forward invariance — nonnegativity of each compartment derived from nonneg initial conditions via the integrating factor technique
• Conservation laws for compartmental systems (total population is constant)
• Monotonicity of susceptible and recovered compartments
• Phase plane invariant — the Kermack–McKendrick invariant V = I + S − (γ/β)ln S
• Epidemic threshold — initial effective threshold ratio βS(a)/γ with global I-monotonicity when that ratio is at most 1
• Stationary infection condition — under I(t) > 0, I'(t) = 0 iff S(t) = γ/β; the artifact does not prove existence, uniqueness, or global maximality of an infection peak (historical source identifier peak_iff)
• Simplex invariance (all compartments bounded between 0 and N)
• Picard–Lindelöf existence/uniqueness for the SIR vector field, with global forward existence for nonnegative initial data

The generic framework lemmas apply to any supplied differentiable trajectory. The SIR existence theory constructs the unique forward ODE solution and bridges the qualitative SIR theorems to that flow.

Theory Structure

Framework (theories/Framework/)

Theory	Contents
Compartmental_Model	Generic linear ODE solution via integrating factor; sign preservation (linear_ode_nonneg, linear_ode_pos); nonneg_deriv_nonneg; three-compartment conservation; monotonicity corollaries

SIR Instantiation (theories/SIR/)

Theory	Contents
SIR_Defs	Locale SIR_solution fixing S, I, R, β, γ with ODE and regularity assumptions; assumes only S(a)≥0, I(a)≥0, R(a)≥0
SIR_Forward_Invariance	Derives S≥0, I≥0, R≥0 from initial conditions via linear_ode_nonneg and nonneg_deriv_nonneg
SIR_Conservation	Total population N = S + I + R is constant (via framework)
SIR_Monotonicity	S is nonincreasing, R is nondecreasing (via framework + forward invariance)
SIR_Threshold	Epidemic growth iff S > γ/β; initial effective threshold ratio βS(a)/γ; initial_epidemic_decline; I_nonincreasing_if_R_zero_le_one
SIR_Peak	Stationary infection condition: I'(t) = 0 iff S(t) = γ/β
SIR_Phase_Plane	Kermack–McKendrick invariant: V(t) = const on trajectories with S > 0
SIR_Invariant	Simplex boundedness: 0 ≤ X(t) ≤ N for each compartment X

Final session theories (work/)

Theory	Contents
SIR_Existence	SIR vector field on ℝ³; C¹ proof; Picard–Lindelöf flow; conservation, global forward existence, and scalar-locale bridge for the unique solution
SIR_Main	Entry point importing all theories; summary documentation

Document (document/)

AFP-style LaTeX document generated by isabelle build.

Building

Requires Isabelle 2024 and AFP 2024 with the Ordinary_Differential_Equations session available.

isabelle build -d /path/to/afp-2024/thys -d . Verified_Compartmental_Models

Build time depends on hardware and cache state.

Assumptions and Scope

• Two-layer structure: SIR_solution records qualitative theorems for any differentiable solution on a finite interval. SIR_ODE constructs the unique forward solution from positive parameters and nonnegative initial data, and instantiates SIR_solution on every nontrivial interval [0,b] with b > 0.
• Nonnegativity derived: forward invariance is proved from nonnegative initial conditions using the integrating factor and then applied to the unique Picard–Lindelöf flow.
• The framework handles three-compartment models. Generalization to n-compartment models via finite sums is planned for future work.
• The global-existence bridge is forward in time from the initial instant 0.
• Terminology: βS(a)/γ is the initial effective threshold ratio, not the disease-free basic reproduction number βN/γ; the historical Isabelle identifier R_zero is retained only as a source-level name.

Artifact Metadata

• Isabelle version: 2024
• ML platform: Poly/ML 5.9.1 (x86_64_32-linux)
• Session: Verified_Compartmental_Models
• External AFP session: Ordinary_Differential_Equations
• Proof holes: 0 (zero sorry/admit/oops)

Dependencies

• Isabelle 2024
• AFP 2024, specifically the Ordinary_Differential_Equations session

License

BSD-3-Clause