Classify all natural, conformally covariant, symmetric (0,2)-tensors of conformal weight -2 and differential order at most 4 in dimension 4, built from the metric, Schouten tensor, covariant derivatives, and the Kulkarni–Nomizu product.

Eleven linearly independent candidate tensor terms are enumerated and the infinitesimal conformal covariance condition is imposed, producing an 8×11 algebraic constraint matrix plus a divergence-free condition. The matrix rank is verified over the rationals by exact Gaussian elimination in a Python script. The final dimension count via the rank–nullity theorem for linear maps between finite-dimensional real vector spaces is formally verified in Lean 4 with Mathlib.

The space of such tensors is exactly 2-dimensional, spanned by the order-2 Bach tensor and the order-4 Eastwood–Singer tensor (11 − 8 − 1 = 2).