Remark: What the proposition does not prove

The proposition does not construct either required nonlocal retarded operation. It also does not classify every allowed finite renormalization. An explicitly added order-${\kappa }^2\hslash$ counterterm is outside Assumption ass:graphs and must be tested separately.

The absence of higher-loop contraction graphs is therefore not an unconditional all-$\hslash$ theorem about every possible normalized observable.