Explicit Kerr Ricci component $R_{\varphi t}$ vanishes as a rational identity

Let $M,a,r,s,c,S,D$ be real numbers subject to

Then the explicit closed-form Ricci component of the Boyer-Lindquist Kerr metric (definition RicciKerr of KerrBL_Kerr_ClosedForms) vanishes:

This is a pure identity of rational functions in seven real variables: $s$ and $c$ need not be a sine and a cosine, and $S,D$ need not be evaluated from $r,c$; the trigonometric relation enters only through the hypothesis $s^2+c^2=1$ and the atoms only through the two side equations. Layer III of the mission consists of this identity for each of the eight components that are not structurally zero; ricci_flat_Kerr instantiates them at a point of the regular domain via ricci_bridge_Kerr.

Formalization Note The non-vanishing hypotheses are exactly the denominators that occur in the closed forms. No assumption about curvature is made: RicciKerr is the full Ricci formula with the generated closed forms substituted, and the statement asserts that this expression reduces to $0$.