Classification of Conformally Covariant 2-Tensors from the Kulkarni–Nomizu Product in Dimension 4

We classify all natural, conformally covariant, symmetric (0,2)-tensors of conformal weight -2 and differential order ≤ 4 in dimension 4, built from the metric, the Schouten tensor, covariant derivatives, and the Kulkarni–Nomizu product. We prove that the space of such tensors is exactly 2-dimensional, spanned by the Bach tensor (order 2) and the Eastwood–Singer tensor (order 4). The classification uses: enumeration of 11 linearly independent candidate tensors; 8 independent algebraic constraints from conformal covariance; and the divergence-free condition as the 9th (differential) constraint. The algebraic core is formally verified using the Lean 4 proof assistant with the Mathlib library. The constraint matrix is verified via exact Gaussian elimination over ℚ (Python/sympy). The paper includes: the explicit formula for the Eastwood–Singer tensor; the 8×11 constraint matrix; the complete set of Kulkarni–Nomizu product identities in dimension 4; and the self-dual splitting of the Weyl tensor. Both English and Russian versions are provided.