Registry · Proposition IV.P105 tau-effective formalized

IV.P105 — Properties of Q_n^s

Properties of Q_n^s: symmetric (Q_n^s(p,q) = Q_n^s(q,p)), non-negative with equality iff p is gauge-equivalent to the vacuum, finite rank (finite-dimensional configuration space), providing the spectral data for the mass gap.

Book IV Part 5 Ch. 41

Dependency Graph

Depends on (1)

Lean Formalization

Module: TauLib.BookIV.Strong.YangMillsGap

Symbol: Tau.BookIV.Strong.PropertiesOfQns