IV.P83 — Properties of \Delta_n^s

The strong defect functional Delta_n^s is non-negative, vanishes on the identity endomorphism, is finite-valued (L_s[n] is finite), and is refinement-monotone: Delta_{n+1}^s(f) >= Delta_n^s(f|_n) for all admissible f.