同与不同：光化学理论的机器验证谱系
The Same and Not the Same: A Machine-Checked Genealogy of Photochemical Theory
浏览论文内容
中文总结 AI 辅助
本文提出PhotoLean，在Lean 4中形式化十七种光化学理论并验证其全部136对关系，解决三项关键混淆，为理论提供机器可审计的谱系。
中文摘要 AI 辅助
化学的现象学理论随其可观测量的增加而增多：同一物理实在在不同的测量语境中被反复命名，而理论之间的关系从未有过可审计的载体。在此，我们提出PhotoLean，一个在Lean 4中于共享内核上形式化的十七种光化学与光物理理论的机器验证谱系。每一对理论要么带有已验证的关系（等价、蕴含、与已注册前提的组合、定义性证书），要么带有其缺失的已注册原因，覆盖全部136对。三项裁决解决了继承性的混淆，并给出了当且仅当的边界与见证：对称因子β恰好当反应物与产物的力常数一致时等于二分之一；Kasha规则与Kasha-Vavilov规则仅在带有损失通道的封闭量化下一致；仅基于强度的Stern-Volmer数据无法区分静态猝灭与动态猝灭，而寿命通道则能精确区分。随着命题生成转向机器，此类机器验证的关系账本为理论本身提供了可复制的审计层。
英文摘要
Chemistry's phenomenological theories multiply with its observables: the same physical reality is repeatedly named in different measurement contexts, and the relations among theories have never had an auditable carrier. Here we present PhotoLean, a machine-checked genealogy of seventeen photochemical and photophysical theories formalized in Lean 4 over a shared kernel. Every pair of theories carries either a verified relation (equivalence, implication, composition with registered premises, definitional certificate) or a registered reason for its absence, covering all 136 pairs. Three adjudications resolve inherited conflations with if-and-only-if boundaries and witnesses: the symmetry factor $β$ equals one-half exactly when reactant and product force constants coincide; Kasha's rule and the Kasha-Vavilov rule agree only under closed quantification with a loss channel; and intensity-only Stern-Volmer data cannot distinguish static from dynamic quenching, whereas the lifetime channel discriminates exactly. As proposition generation shifts to machines, such machine-checked relational ledgers offer a replicable audit layer for theory itself.
发表机构
- Shenzhen MSU-BIT University（深圳北理莫斯科大学）
- The Chinese University of Hong Kong, Shenzhen (CUHK-SZ)（香港中文大学（深圳））
- Hong Kong University of Science and Technology（香港科技大学）
机构由 AI 辅助整理，请以论文原文为准。
