# EXTERNAL BAR — `proof-estate-lean-z3`

## The lab's own F2 line (verbatim, `CROWN_JEWELS_RESOLVED.md:79` at commit `cb6d9d7d`)

> **F2 — what would move the third-party axis to A.** Axis B — a system Genesis does not own already grades this one: Z3 and cvc5 (two SMT kernels, cross-checked) discharge our theorems; no bar, kernels (bar recorded: `kernel`). To reach axis A, that same external system must be run against a bar **pre-registered before the run** and its own output cited. Today only Gate 97 (FastCap) and Gate 133 (Touchstone) sit under a content-sealed bar, and `PEER_REVIEW_2026-09.md:20-23` records axis A = 0 across this register.

## What an independent party would have to do to move this entry to axis A

1. **Pre-register the bar before running anything.** Write down which properties must come back `unsat` (the 27
   required theorems named by the modules in `proofs/z3/`) and which must come back `sat` (the 8 fault injections).
   Seal the list, with a content sha256 and a timestamp, where Genesis cannot edit it.
2. **Run the kernels themselves.** On their own machine, with their own Z3 and cvc5 builds, run
   `PYTHONPATH=. python3 scripts/audit/verify_z3_proofs_gate.py` at the named commit, or re-encode the properties in
   SMT-LIB and hand them to the solvers directly. Then publish the solver output.
3. **What they need.** Any laptop: the run takes seconds and uses no GPU. The only data is the eleven files listed in
   `INPUTS.sha256`. Tools: Z3 (4.15.4 here) and cvc5 (1.3.4 here).

## What would falsify the claim

- Any required theorem comes back `sat` or `unknown` from Z3 or cvc5. `sat` means the ceiling is refuted, as this
  packet's `DEFECT.json` demonstrates.
- The two solvers disagree on any property.
- A fault injection comes back `unsat`: then the harness cannot tell a false property from a true one.
- An encoding in `proofs/z3/` turns out not to state the ceiling the register claims it states. This packet cannot
  detect that, because a solver checks the encoded proposition, not the physics it abstracts
  (`CROWN_JEWELS_RESOLVED.md` §1, "What the claim does not cover").