Registry · Lemma IV.L07 tau-effective formalized

IV.L07 — Discrete Hessian Spectrum

Sequence {lambda_1^(n)} is monotonically decreasing and bounded below, converging to lambda_1 > 0 (refinement-stable). Full limiting spectrum is discrete. Strict positivity excludes fourth flat direction.

Book IV Part 4 Ch. 34

Dependency Graph

Depends on (2)

IV.P74 IV.D140

Depended on by (3)

IV.D141 IV.P75 IV.T65

Lean Formalization

Module: TauLib.BookIV.Electroweak.TauHiggs2

Symbol: Tau.BookIV.Electroweak.DiscreteHessianSpectrum