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.

翻译：我们提出一个经由机械验证的 Isabelle/HOL 桥梁，将形式证明档案库 (AFP) 中的 Picard-Lindelöf 流基础设施连接到质量作用、封闭种群 SIR 流行病常微分方程选定的定性结论。这些流行病学结论是经典的；贡献在于可复用的定理基础设施，它将 AFP 局部流构造连接到全局正向存在性、唯一性、非负卦限的正向不变性、守恒性、单调性、Kermack-McKendrick 守恒相平面关系、分区界限以及传染增长与单调性的阈值比率条件。证明首先确立局部 AFP 流段的符号与守恒事实，然后利用守恒非负单纯形作为紧致性证据，将流扩展到所有正向时间。随后，有限区间上的定性结论被转移到任意区间 [0,b]（其中 b>0）上唯一的 AFP 正向流，因此结果适用于构造出的 Isabelle/AFP SIR 解，而非假定的轨迹。可复用层提供了方程 X'(t)=f(t)X(t) 的齐次线性标量分区引理、导数符号单调性、三分区守恒性，以及通往 AFP 流基础设施的 SIR 传输桥梁。我们未形式化稳定性、最终规模或渐近理论。随附的 Isabelle 工件使用 Isabelle 2024 和 AFP 2024 构建，不包含任何 sorry 或 oops 证明占位符。