Item 9: Forcing headlines that are squeezes

The audit's §3.3 is "The forcing headlines are squeezes over hypotheses equivalent to their conclusions". A squeeze is a theorem whose hypothesis already contains its conclusion; it is not false, it is empty.

Deliverable shape: lean-proved restatements whose hypotheses are strictly weaker than their conclusions, each with an inhabitation witness. Acceptance check: The Lean gate is green and each restated theorem ships a typechecking witness term.

Context: projects/deference/note-dump-2026-08-11/lean-deference/AUDIT.md §3.3, and §5's severity ranking. A solution ships: restated theorems whose hypotheses are strictly weaker than their conclusions, with the gap displayed — or a demonstration that the squeeze is unavoidable, which is itself a result.