Wick's theorem

The combinatorial engine of field theory -- correlators as sums over pairings -- survives the finite cutoff exactly, with the threshold where it fails stated as part of the theorem.

proved in corpus · proved here, no imported axiomsLean timeFourPoint_wick

In plain terms

Here is the problem. Quantum field theory computes everything from a miracle of bookkeeping: any correlation of many field operators reduces to a sum over ways of pairing them up, each pair contributing a basic propagator. That is Wick's theorem, and it is usually proved with infinitely many oscillator levels in hand.

Cut the ladder at N quanta -- as any finite arena must -- and the question becomes quantitative: does the pairing formula survive, and where exactly does it break? The corpus's answer: it survives verbatim below an explicit threshold, because a 2n-step return walk simply cannot reach the missing levels; at the threshold it fails by a computed amount.

Approximation with an error bar is replaced by exactness with a boundary.

In CSD

This is the field track's breadth at its most textbook: four-point functions at equal and distinct times closing into the pairing sum, the two-time kernel carrying the time dependence, and the full moment ladder -- the double-factorial law for arbitrary even powers -- proved by a commutator recursion in which the cutoff defect is killed by the walk band, not ignored.

The honest boundary is in the header: the one-shot sum-over-matchings formula for arbitrary interleaved operator words is not claimed; the double factorial carries that content on the mode diagonal.

Mathematically

timeFourPoint_wick: the distinct-times four-point function equals the pairing sum of two-time kernels over every mode pattern, for cutoffs above two. The moment ladder: the vacuum expectation of Q to the 2n is (2n-1) double factorial times one-half to the n, exactly, for n below the cutoff, via the recursion against the truncated commutation relation; odd moments vanish by walk parity, and grouped mode patterns factorise by clustering.

The name

Gian Carlo Wick (1909-1992) was born in Turin, worked alongside Fermi in Rome in the 1930s, and after the war held positions at Berkeley -- which he left rather than sign the loyalty oath -- then Carnegie Tech, Brookhaven and Columbia. The 1950 theorem on evaluating products of field operators, published in the Physical Review, systematised the calculations of the newly renormalised quantum electrodynamics and has been the daily tool of the subject ever since.

Module
CsdLean4/CV/Wick.lean
Related
field arena, gibbs state, kms condition

Source links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.

Part of Constraint-Surface Dynamics · Formalised in csd-lean4.

Privacy policy