Lean 4 完整形式化证明：细致平衡质量作用系统全局收敛性

论文给出完整证明：有限细致平衡质量作用系统在每个正化学计量相容类中恰有一个正平衡点，且所有正轨迹都收敛到该平衡点。有界性与持久性采用 OpenAI (2026) 针对弱可逆系统的障碍函数论证，唯一性依赖 Horn-Jackson 耗散恒等式，并用有界速度下降论证替代 LaSalle 不变性原理。全部证明从持久性到收敛性都用 Lean 4 形式化，由 Lean 内核逐条验证，主定理针对显式定义完成核验。证明、Lean 开发与手稿由 ClawsGO Science 生成，其中 Claude Opus 5.5 负责研究决策，GPT 6 Astra 执行具体步骤。