The Same and Not the Same: A Machine-Checked Genealogy of Photochemical Theory
Abstract
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.
Related
- Experimental Inter-Report Scatter Bounds Machine-Learning Accuracy for TADF Singlet–Triplet Gaps—Structure and Semi-Empirical Features Reach the Same Limit
- Integrating DLVO Theory with Machine Learning for Predictive Toxicology and Multi-Objective Design of Quercetin-Loaded Nanocarriers
- Built in Minutes, Checked by Script: Instructor-Made Interactive Chemistry Study Guides with Generative AI
- Zinc Redox Catalysis in the Photochemical Borylation of Fluorocarbons
- Direct photochemical activation of aliphatic carboxylic acids toward phosphinylation via polarity-reversed Arbuzov process
BibTeX
@misc{gong2026same,
title = {{The Same and Not the Same: A Machine-Checked Genealogy of Photochemical Theory}},
author = {Junyi Gong and Zijie Qiu and Ben Zhong Tang},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.32251},
eprint = {2609.32251},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.32251},
note = {CC BY-NC-ND 4.0},
}
RIS
TY - UNPB
TI - The Same and Not the Same: A Machine-Checked Genealogy of Photochemical Theory
AU - Junyi Gong
AU - Zijie Qiu
AU - Ben Zhong Tang
PY - 2026
DA - 2026/09/26
PB - arXiv
DO - 10.48550/arxiv.2609.32251
UR - https://arxiv.org/abs/2609.32251
AB - 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.
ER -