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.
timeFourPoint_wickHere 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.
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.
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.
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.
CsdLean4/CV/Wick.leanSource 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.
Google Analytics counts visits to this page, which stores cookies in your browser. They record how the page was reached, not who you are, and nothing is passed on. Blocking cookies for this site breaks nothing here. Details.