Inductive proof of the scalar Wick theorem (source code)

= Inductive proof of the scalar Wick theorem

Split each free <real scalar field> as $\phi=\phi^{(-)}+\phi^{(+)}$, into creation and annihilation parts. For chronologically ordered arguments, the first field has the latest time. Multiplying it into a <normal-ordered product> of the remaining fields gives
$$
\phi_1:\!\prod_{r\in I}\phi_r\!:
=:\!\phi_1\prod_{r\in I}\phi_r\!:
+\sum_{j\in I}[\phi_1^{(+)},\phi_j^{(-)}]:\!\prod_{r\in I\setminus\{j\}}\phi_r\!:.
$$
This follows by commuting the annihilation part through each creation part; each <commutator> is a scalar, and all creation parts commute among themselves, as do all annihilation parts. The scalar commutator is the <Feynman propagator> for the chronological pair. Induction on the number of fields therefore lists every partial pairing exactly once: either field 1 remains unpaired or it pairs with one $j$. This proves the <Wick theorem> for free bosonic fields, including the empty pairing. Vacuum expectation retains only complete pairings. The identities are understood for regulated or smeared <operator-valued distributions>.