Lock double-negation identity, Always/Eventually duality with bound preservation, leaf pushdown, and not(always true) reaching Violated.
pj