# EXPECTED — `proof-estate-lean-z3`

<!-- kit:claim witness="PYTHONPATH=. python3 scripts/audit/verify_z3_proofs_gate.py" extract="PASS\|\| (\d+)/(\d+) required theorems proved \(unsat\), (\d+) fault-injections refuted \(sat\), (\d+) existence witnesses, (\d+)/(\d+) bonus" -->
<!-- repro:expect [{"group": 1, "equals": "27"}, {"group": 2, "equals": "27"}, {"group": 3, "equals": "8"}, {"group": 4, "equals": "3"}, {"group": 5, "equals": "3"}, {"group": 6, "equals": "3"}] -->

**The claim** (`top40.json` rank 8, `CROWN_JEWELS_RESOLVED.md` §1): the load-bearing ceilings, floors and certificate
properties ship as executable statements that third-party SMT kernels check.

**What this packet reproduces.** The Z3 lane only. `verify_z3_proofs_gate.py` imports seven modules from `proofs/z3/`.
For each property it asks Z3 (cross-checked by cvc5 when cvc5 is installed) for a verdict. It prints:

| parsed group | value | meaning |
|---|---|---|
| 1 / 2 | 27 / 27 | required theorems discharged `unsat`, out of the required theorems present |
| 3 | 8 | fault injections refuted `sat` (a harness that cannot refute a planted false property fails) |
| 4 | 3 | existence witnesses found |
| 5 / 6 | 3 / 3 | bonus theorems discharged, out of those present |

**Tolerance: exact.** Every value is a count of solver verdicts, an integer that does not depend on hardware or
timing. A count that moves means that a property was added, removed or refuted, and that change is exactly what the
packet must notice.

**Not covered.** The Lean lane named in the claim ("two independent lanes") is not exercised by this command, and
neither is the "counts went down" history. `dataroom/witness_quality.json` records both as unbound.

**Measured** 2026-09-17 in a tree holding exactly commit `cb6d9d7d`: exit 0 in 1.2 s. The run also printed the cvc5
cross-check note, whose wording depends on whether cvc5 is installed; that note is not parsed.