Registry · Definition IV.D166 tau-effective formalized

IV.D166 — Excitation cost

The excitation cost lambda_n(p) := (Q_n(p,p), ||p||_n) is the lexicographic pair of the quadratic energy cost and the NF-norm, measuring how energetically expensive a perturbation is above the vacuum with degeneracy-breaking.

Book IV Part 5 Ch. 40

Lean Formalization

Module: TauLib.BookIV.Strong.GapMetaTheorem

Symbol: Tau.BookIV.Strong.ExcitationCost