GenServer that detects global closure and extracts countermodels.

Subscribes as a peer of SuggestionAgent to the shared branch_evidence_<session> PubSub topic. Workers publish every branch lifecycle event (:branch_split, :branch_closed, :branch_saturated, :local_clashes) once; both agents receive them independently. Manager commands (:settle, :verify_all_closed, :verify_csa) still arrive as direct GenServer.call/cast since they are coordination, not evidence.

Two stores are maintained:

• branch_closures — branches discharged by ground contradiction. A closed branch is dropped from active_branches immediately and its closure is retained only for proof reconstruction.
• clashing_local_pairs — unifiable literal pairs from still-open branches, indexed by branch id and inherited by descendant branches.

Closure is detected through three coordinated triggers, all funneling into find_global_closure/2:

• check_global_closure — eager, async via dispatch_csp. Runs after every clash or split as long as no other search is in flight.
• :settle — sync call from the manager when workers stall but branches are still parked. Reuses the eager path and replies once the task completes via settle_waiter.
• :verify_all_closed / :verify_csa — manager-coordinated settle points when no work remains. The former short-circuits to :unsat when every branch has already closed; the latter falls back to SAT/:unknown if the CSP cannot find a global unifier.

Closures and clashes are kept disjoint by construction: once a branch is in branch_closures it is no longer in active_branches, so the CSP only sees open branches' rigid-unification options.

Out-of-order tolerance

Losing the sync worker→CA edge means BEAM's cross-sender ordering guarantee no longer serializes lifecycle events. In particular, a :branch_closed for a child may arrive before its parent's :branch_split. The split handler defensively excludes any child already present in branch_closures; the closure handler tolerates branches it has never seen as active (they get recorded as closures and are then filtered out if the split arrives later).