Editable family: success; trace [[6, 1], [5, 2]].
Conjunction family: rejected; completed rejection DAGs are independently checked.
Six-vertex Hall example: initial matching True, recognizer rejected, 322 memoized states.
Projection of a <-> h gives a supported visible singleton; deletion of h does not.
Three-vertex census: 55 graph-realizable families among 61 union-closed empty-containing families.
Budget exhaustion is unresolved. These finite certificates do not rerun Lean or prove polynomial-time recognition.