theorem Hex.GraphIso.Nauty.certifyNodeAutom_automsOk {n : Nat} (ctx : Ctx n) (tcLevel fuel level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (bcodes : List Nat) (st : AutState) : AutomsOk (fun (γ : Array Nat) => checkAutom ctx.g γ = true) (certifyNodeAutom ctx tcLevel fuel level lab ptn active numcells bcodes st).fst

theorem Hex.GraphIso.Nauty.produceCand_automsOk {n k : Nat} (G : Colored n k) {budget : Option Nat} {cert : CertNode} {B : Key n} (h : produceCand G budget = some (cert, B)) : AutomsOk (fun (γ : Array Nat) => checkAutom (rowsOf G) γ = true) cert

Every automorphism record in a produced candidate has passed the trusted automorphism checker.

theorem Hex.GraphIso.Nauty.certifyCanon?_isSome_of_keyEq {n k : Nat} (G : Colored n k) (hdom : canonSpecKey G = tracedKey G) : (certifyCanon? G).isSome = true

Once the traced key equals the specification key, no further store hypothesis is needed for totality: every emitted automorphism has already passed the trusted checker.