Machine-Checked Decompositions of Information Science Theorems: Subtraction Formalization and the Limits of Interpretive Collapse

This collection contains two companion manuscripts that introduce and demonstrate "Subtraction Formalization," a diagnostic method for auditing frontier theorems in information science, algorithmic fairness, and organizational theory that currently exceed the capabilities of proof assistant libraries. The first manuscript, False, Elided, or Over-Strong: Three Diagnostic Formalizations of Theorems That Cannot Yet Be Proved, establishes the methodology. It deliberately strips heavy analytic machinery (optimal transport, calibrated probability, Perron-Frobenius theory) from three target theorems, retaining only the order-theoretic or counting skeleton checkable in Lean 4. It classifies the diagnostic outcomes into three categories: hypotheses that are false in the intended setting (interpretive collapse), hypotheses that are true but routinely dropped in downstream restatements (classifier fairness impossibility), and hypotheses that are stronger than the result requires (DeGroot opinion dynamics). The second manuscript, Irreversibility Is a Ratio: A Machine-Checked Decomposition of Interpretive Collapse, provides the deep-dive application for the first case. Using Lean 4, it strips the Wasserstein metric from a measure-theoretic model of receiver-constituted interpretation. It proves that exact convergence to certainty is dynamically impossible under persistent diffusion, revealing that the threshold for interpretive collapse is governed by a ratio of drift to diffusion, and that the geometry of the system dictates whether support is preserved or destroyed. Together, these papers demonstrate how order-theoretic subtraction can identify load-bearing hypotheses, expose elided base-rate conditions, and reveal over-strong spectral assumptions in socio-technical models, providing a low-cost diagnostic tool for fields awaiting the formalization of heavy analytic libraries.