No barber shaves exactly those who do not shave themselves

Ran 2026-08-17: the file asserts the NEGATION of formal.statement and the harness printed `; evidence kind=unsat-quant-instance-set certified=1 recheck=na arena=ok ms=22`, then `unsat`. This fact was `open` until this date and this row is what closed it; the reason it was open is recorded in the fact's notes and is worth reading, because the gap was never the theorem. WHAT THE CERTIFICATE IS. `Evidence::UnsatQuantInstanceSet`, a `QuantifierInstanceSetCertificate` (`crates/axeyum-solver/src/quant_instance_set_cert.rs`). It contains no term of the producing run at all: a per-assertion count of top-level existential binders eliminated (here `[1]`), and one universal instantiation naming its universal by INDEX into the skolemised assertion list and its single binding as `Witness { assertion: 0, index: 0 }` -- 'the witness introduced for the outermost existential of assertion 0'. Positional, because a `TermId` from the producing arena names nothing in a checker's. WHAT `arena=ok` MEANS HERE. `Evidence::check` re-parsed the file into an arena sharing nothing with the solve and then, in that arena: re-ran the SAME existential elimination (`auto::eliminate_top_existentials`) to obtain ITS OWN witness -- so freshness, the soundness condition for eliminating an existential, is established by the checker rather than taken from the producer; required the recorded binder counts to equal its own; rebuilt the instance by substituting its own witness into its own universal; replayed that instance through the public `check_quantifier_ground_derivation`; rebuilt the ground set from its own non-universal assertions plus that instance (so nothing can be smuggled into a set the checker constructs); and re-refuted it. WHAT IS NOT CERTIFIED, stated because the route name could otherwise flatter it. The final sufficiency step re-invokes `auto::check_auto` on the ground residue rather than checking a clause-level proof object. Measured 2026-08-17 with `cargo run --release -q -p axeyum-bench --example diagnose_evidence` on that residue (`(= (shaves sk sk) (not (shaves sk sk)))`): `euf-online: decided unsat`. So the CDCL(T) EUF core and its CNF abstraction are in the trust base, and -- unlike the other `smt-clausal` facts in this ledger -- there is NO DRAT or Alethe object here. What this certificate independently establishes is the QUANTIFIER reduction: the existential elimination and the one instantiation that were previously performed, recorded, and then dropped on the floor. Independently cross-checked: `z3 -smt2` (/usr/bin/z3) on the same file also reports `unsat`.