theorem Hex.GraphIso.Nauty.produceCand_none_isSome {n k : Nat} (G : Colored n k) : (produceCand G none).isSome = true

With no node budget, the candidate producer always returns a candidate.

theorem Hex.GraphIso.Nauty.produceCand_key {n k : Nat} {G : Colored n k} {budget : Option Nat} {cert : CertNode} {B : Key n} (h : produceCand G budget = some (cert, B)) : B = { codes := (runColoredTraced G).bestCodes ++ [codeSentinel], rows := leafRows { g := rowsOf G } (runColoredTraced G).result.canonlab }

The key of every produced candidate is read off the traced run: the recorded code chain with the sentinel, and the spec rows of the traced canonical labelling.

theorem Hex.GraphIso.Nauty.certifyCanon?_isSome_of_checkKey {n k : Nat} (G : Colored n k) (h : ∀ (cert : CertNode) (B : Key n), produceCand G none = some (cert, B) → checkKey G cert B = true) : (certifyCanon? G).isSome = true

The reduction of certifyCanon? totality to the certificate replay: if the produced certificate replays against the traced key, the transcription-side results discharge every other conjunct of the single trusted validation, so the certified canonicalization succeeds.