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 less than or equal to 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 algebraic core is formally verified using Lean 4 with Mathlib. The 8x11 constraint matrix and divergence-free condition are verified computationally with exact rational arithmetic. Both English and Russian versions provided; Russian version available as ancillary.