What the Karpowicz Theorem Does Not Prove: A Three-Component Decomposition of the LLM Einstein Test

A growing literature claims that large language models cannot, in principle, produce paradigm-replacing scientific theories on the model of Einstein's 1905 work, an "LLM Einstein Test" grounded in a purported binary impossibility theorem. Karpowicz (2025) is widely cited as supplying such an impossibility theorem. We argue this is a misreading. Karpowicz proves a four-way trade-off, not a binary impossibility, and the trade-off applies equally to human reasoners. We attempt an impossibility theorem directly and report a symmetry argument against any LLM-only impossibility framing, then prove a positive structural decomposition supported by five results. The Einstein Test factors strictly into three cost components (generation, computational verification, and empirical verification), each governed by a different mathematical category. Empirical verification has a generator-independent non-negative lower bound τ_min tied to the wall-clock time of the minimum decisive experiment (Theorem 1, for T* the correct successor in the sense of that theorem); this bound is exogenous to AI capability and applies to human science as well. The canonical Mercury-perihelion case (1859–1915) is best read as an illustrative analogy where the decisive observation came before the successor theory; strictly applying Theorem 1 requires (E1), which excludes the case where the decisive observation already refutes T_0, and the standard 1859–1915 narrative implicitly switches T_0 across time-slices. Generation admits a soft Kolmogorov-complexity emission lower bound (Theorem 2), with three escape routes identified (test-time search, decreasing conditional complexity for ripe innovations, and continual training). Computational verification of the distinguishability predicate is Σ⁰₁-hard on recursively axiomatised classes containing Robinson arithmetic (Theorem 3, in particular not total computable), and decidable on the Tarski class of theories whose prediction sets are first-order definable over the real-closed-field signature with decidable prediction membership. Theorem 4 combines these into a strict three-component decomposition with a coupling structure under which AI capability gains lower the generation and computational-verification components but cannot lower the empirical-verification component. Theorem 5 closes a popular loophole: no purely computational system can self-verify Einstein-replacement outputs when the prompt contains no observations beyond any sub-collection of accumulated data, since soundness requires external empirical data that no internal computation can supply; the corollary shows the impossibility is structural and applies to any reasoner (computational or human) that lacks empirical access. As a foundational refinement, we upgrade the formal definition of "ontological innovation" from a syntactic to a Beth-definability condition, ruling out trivial renamings. The composite claim "LLMs cannot do Einstein" is false in the generation sense, partially true on adversarial computational classes, and trivially true on the empirical floor for reasons unrelated to AI capability. No LLM-specific Einstein Test impossibility theorem exists at the level of pure mathematics, since any such theorem would also bind human reasoners qua finite physical systems; what exists is a verification-asymmetric decomposition together with a structural self-verification impossibility result that applies to any reasoner lacking empirical access. The Lean source is available at: https://github.com/crabsatellite/einstein-test-lean4-formalization