The theorem proved and the question not yet decided

The overall factor $i$ in (eq:apptarget) is part of the selected-family convention. There is no $1/\hslash$ prefactor. Section sec:normalization explains its coupling and contraction multiplicity completely.

The proof of Theorem thm:main is completed in Section sec:estimate. The distinction between ordinary contractions, time ordering, and their domains is retained throughout; these are separate operations in perturbative algebraic quantum field theory FR (Sections 5–7).