Perfectness predicates on scheme-derived objects

Pseudo-coherence, local finite Tor amplitude over a base, relative perfection and the universally-gluable refinement: properties of one complex over one morphism, stated before any moduli problem consumes them.

Absolute perfection, schemePerfect and schemePerfectInDqc, is older and belongs to Coherent.lean and Dqc.lean; the one-way comparisons among the repository's three uses of "perfect" stay in Moduli/PerfectComplex/Comparison.lean. See the ledger in docs/architecture/placement.md.