Codex 辅助研究优先级控制器故障检测的精确可达集合与复杂度分类，Lean 登记早于论文发表

Idris Ali Shaik 于 10 月 23 日公开一项逻辑与形式验证研究，分析 c432 优先级控制器任意规模扩展在指定首阶段 bridge fault 下的可达 qualifier 集合，并对特定 guarded decoder 子类给出线性复杂度检测算法、完整 CNF 不可满足实例的 O(N³) resolution refutation 界，同时报告检测问题 P-complete、最小集优化 NP-hard、计数 #P-complete 等结论。OpenAI Codex 协助发现论证、Lean 形式化和手稿准备，人类作者逐项审核承担责任；页面链接 PALOMAR-2026-10-19-000010，故其**首次 Lean 登记是 10 月 19 日，不是 23 日**。本条记录 23 日首次公开的完整研究论文，而非新登记或无条件验证所有复杂度证明。