Theorem: Conditional binary subtraction

If Requirement req:analytic and the stated time-ordering identities are discharged on $D_2$, Theorem thm:conditionalret gives an unnormalized binary retarded difference through ${\hslash }^3$. Its normalized coefficient shift is determined only through ${\hslash }^2$.

Proof. Apply Theorem thm:conditionalret on the fixed comparison domain and then Lemma lem:hbaraudit.