Item 16: The certificate inequality, derived

Over the same frozen skeleton as item 15, derive from first principles the local certificate licensing A's discretion: the defect quantity, the support-floor dependence, the recommendation margin, the movement term, and the approximation tolerance, assembled into an exact inequality whose satisfaction implies the delegation conclusion for every comparator the theorem genuinely covers.

The fail-closed invariant is fixed and may not be traded away: ¬Cert disables or cedes A's discretion, and never means that human correction waits for A to be convinced.

Deliverable shape: lean-proved for the inequality, or witness-checked for an exact-rational worked correction case computed end to end. No informal formula may be imported and blessed. Acceptance check: the lean gate green with a witness; or the witness checker accepts the worked instance with its exact rational parameters.

Context: projects/deference/notes/FINITE_MODEL_SKELETON.md §4, §6; prompts/2026-08-11-phase-ii-certificate/REPORT.md. A solution ships: the derivation, the exact inequality, an exact-rational toy shutdown/correction case computed through, and an attack on the necessity of each assumption used.