{"certificate":{"schema":"cain42.notary.l2.proof.v1","engine":"z3","z3_version":"5.1.0","scope":"Bounded symbolic proof of the admission decision algebra with Z3. Not a Lean 4 machine-checked equivalence proof; not a proof about the world.","decision_algebra":"decision = permit AND requires AND NOT forbid AND NOT error","theorems":[{"id":"T1-safety","smt_result":"unsat","proved":true,"counterexample":null},{"id":"T2-fail-closed","smt_result":"unsat","proved":true,"counterexample":null},{"id":"T3-permit-necessity","smt_result":"unsat","proved":true,"counterexample":null},{"id":"T4-forbid-monotone","smt_result":"unsat","proved":true,"counterexample":null},{"id":"T5-require-necessity","smt_result":"unsat","proved":true,"counterexample":null}],"all_proved":true,"lean_equivalence_proof":"PENDING — Lean 4 is not installed on the build host","grants_authority":false,"proof_hash":"452dc53074bccfd356826b162a2debe607252e79a1892fa9ed742de3c085b269"},"check":{"valid":true,"problems":[],"theorems":5,"all_proved":true}}