Registry · Proposition IV.P108 tau-effective formalized

IV.P108 — Tower monotonicity

Tower monotonicity: delta_{n+1}^s >= delta_n^s for all n >= 3, so the spectral gap is non-decreasing along the refinement tower. Higher refinement strengthens admissibility constraints, increasing the energy cost of any excitation.

Book IV Part 5 Ch. 41

Dependency Graph

Depends on (1)

Lean Formalization

Module: TauLib.BookIV.Strong.YangMillsGap

Symbol: Tau.BookIV.Strong.TowerMonotonicity