Function check_quotient_dag 

pub fn check_quotient_dag(nodes: &[QNode]) -> bool

Zero-trust checker with twist verification: leaves carry ⊥; each internal node’s recomputed cofactor, pushed through the stored twist, must equal the child EXACTLY. A pass certifies the root UNSAT by structural induction (unsatisfiability is isomorphism-invariant and each twist is a literal renaming), in time linear in the quotient DAG.