Formally Verified Epidemic Thresholds: The SIR Model as a Grade-2 Dynamical System

The classical SIR (Susceptible-Infected-Recovered) epidemic model of Kermack and McKendrick (1927) is the foundation of mathematical epidemiology. We present a formally verified analysis of this model by identifying its algebraic structure as a Grade-2 dynamical system: the infection rate \(g(S,I) = \beta S I - \gamma I\) decomposes into a linear Grade-1 recovery term (\(\gamma I\)) and a quadratic Grade-2 pairwise transmission term (\(\beta S I\)), with a critical threshold \(S_c = \gamma/\beta\) corresponding to the basic reproduction number \(R_0 = 1\).

We prove 18 theorems establishing: (1) existence and positivity of the epidemic threshold; (2) sub-threshold decay guaranteeing epidemic extinction; (3) super-threshold growth characterizing epidemic outbreak; (4) herd immunity fraction \(1 - 1/R_0\) as the algebraically necessary immune proportion; (5) vaccination sufficiency bounds with rigorous intervention guarantees; (6) minimum population size \(N \geq 4\) for sustained transmission via binary counting; and (7) delay penalty monotonicity showing that postponed intervention always increases total cost.

All results are machine-verified via the proof kernel type-checker and exported to 325 lines of Lean 4 proof code. The structural identity between the SIR model (\(g = \beta S I - \gamma I\), threshold \(S_c = \gamma/\beta\)) and Kessler space debris cascades (\(f = \beta \rho^2 - \alpha \rho\), threshold \(\rho_c = \alpha/\beta\)) demonstrates that Grade-2 systems govern critical bifurcations across radically different physical domains.