Registry · Lemma VI.L15 tau-effective not_formalized

VI.L15 — Complexity Monotone

Complexity budget C(n) is monotonically increasing: C(n) <= C(n+1) for all n; follows from Master Exhaustion Inequality V.T62.

Book VI Part 2 Ch. 14

Dependency Graph

Depends on (1)

VI.D75

Depended on by (2)

VI.T44 VI.T46

Lean Formalization

Module:

Symbol: