Registry · Lemma IV.L10 tau-effective formalized

IV.L10 — Positive gap at each stage

For each n >= n_* the positive gap mu_1^(n) > 0 holds: by (KH-3), Q_n(p,p) > 0 for all nontrivial p, and the minimum of a finite set of positive numbers is positive. In continuum QFT the analogous infimum need not be attained.

Book IV Part 5 Ch. 40

Dependency Graph

Depends on (1)

Lean Formalization

Module: TauLib.BookIV.Strong.GapMetaTheorem

Symbol: Tau.BookIV.Strong.PositiveGapAtEachStage