The target has the exact ideal-membership identity

T = (a+b+c+d)(a^3+b^3+c^3+d^3+abc+abd+acd+bcd)
    -(a^2+b^2+c^2+d^2)(ab+ac+ad+bc+bd+cd).

The first factor is the linear generator and the second factor is the quadratic generator; their displayed integer multipliers are exactly the certificate checked below.

The verifier expands both products coefficient by coefficient over QQ. The multiplier of the linear generator and the multiplier of the quadratic generator both have integer coefficients. Since each generator is divisible by n for integer inputs, their integer-polynomial linear combination is divisible by n as well. This is an exact computed certificate, not a proof-assistant VERIFIED theorem artifact.
