theorem Hex.GraphIso.Nauty.keyCmp_codes_nil_gt {n c : Nat} {cs : List Nat} {r br : List (VSet n)} : keyCmp { codes := c :: cs, rows := r } { codes := [], rows := br } = Ordering.gt

A key with a nonempty code list exceeds any key with an empty one.

theorem Hex.GraphIso.Nauty.keysMax_lt {n : Nat} {b k : Key n} {l : List (Key n)} (hk : keyCmp k b = Ordering.lt) (hl : ∀ (y : Key n), y ∈ l → keyCmp y b = Ordering.lt) : keyCmp (keysMax k l) b = Ordering.lt

The maximum of strictly dominated keys is strictly dominated.

def Hex.GraphIso.Nauty.AutomsOk (P : Array Nat → Prop) : CertNode → Prop

Every .autom record's generator satisfies P.

Equations

• Hex.GraphIso.Nauty.AutomsOk P Hex.GraphIso.Nauty.CertNode.leaf = True
• Hex.GraphIso.Nauty.AutomsOk P Hex.GraphIso.Nauty.CertNode.codePrune = True
• Hex.GraphIso.Nauty.AutomsOk P (Hex.GraphIso.Nauty.CertNode.autom o γ) = P γ
• Hex.GraphIso.Nauty.AutomsOk P (Hex.GraphIso.Nauty.CertNode.node children) = Hex.GraphIso.Nauty.AutomsOkList P children

def Hex.GraphIso.Nauty.AutomsOkList (P : Array Nat → Prop) : List CertNode → Prop

AutomsOk over a list of subtrees.

Equations

• Hex.GraphIso.Nauty.AutomsOkList P [] = True
• Hex.GraphIso.Nauty.AutomsOkList P (c :: cs) = (Hex.GraphIso.Nauty.AutomsOk P c ∧ Hex.GraphIso.Nauty.AutomsOkList P cs)

theorem Hex.GraphIso.Nauty.automsOkList_of_mem {P : Array Nat → Prop} {cs : List CertNode} (h : AutomsOkList P cs) (c : CertNode) : c ∈ cs → AutomsOk P c

theorem Hex.GraphIso.Nauty.automsOkList_of_forall {P : Array Nat → Prop} {cs : List CertNode} : (∀ (c : CertNode), c ∈ cs → AutomsOk P c) → AutomsOkList P cs

theorem Hex.GraphIso.Nauty.automsOk_mono {P Q : Array Nat → Prop} (hPQ : ∀ (γ : Array Nat), P γ → Q γ) (c : CertNode) : AutomsOk P c → AutomsOk Q c

theorem Hex.GraphIso.Nauty.automsOkList_mono {P Q : Array Nat → Prop} (hPQ : ∀ (γ : Array Nat), P γ → Q γ) (cs : List CertNode) : AutomsOkList P cs → AutomsOkList Q cs

def Hex.GraphIso.Nauty.CertNode.depth : CertNode → Nat

The depth of a certificate tree.

Equations

• Hex.GraphIso.Nauty.CertNode.leaf.depth = 1
• Hex.GraphIso.Nauty.CertNode.codePrune.depth = 1
• (Hex.GraphIso.Nauty.CertNode.autom o γ).depth = 1
• (Hex.GraphIso.Nauty.CertNode.node children).depth = 1 + Hex.GraphIso.Nauty.CertNode.depthList children

def Hex.GraphIso.Nauty.CertNode.depthList : List CertNode → Nat

The maximum depth of a list of certificate subtrees.

Equations

• Hex.GraphIso.Nauty.CertNode.depthList [] = 0
• Hex.GraphIso.Nauty.CertNode.depthList (c :: cs) = max c.depth (Hex.GraphIso.Nauty.CertNode.depthList cs)

theorem Hex.GraphIso.Nauty.depthList_le {cs : List CertNode} {d : Nat} (h : ∀ (c : CertNode), c ∈ cs → c.depth ≤ d) : CertNode.depthList cs ≤ d

theorem Hex.GraphIso.Nauty.depth_le_of_mem {cs : List CertNode} {c : CertNode} (hc : c ∈ cs) : c.depth ≤ CertNode.depthList cs

theorem Hex.GraphIso.Nauty.certifyNodeAutom_depth {n : Nat} (ctx : Ctx n) (tcLevel fuel level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (bcodes : List Nat) (st : AutState) : (certifyNodeAutom ctx tcLevel fuel level lab ptn active numcells bcodes st).fst.depth ≤ fuel + 1

The walk emits trees no deeper than its fuel allows.

theorem Hex.GraphIso.Nauty.automsOk_validGammas {nn : Nat} {g : Array (VSet nn)} {cert : CertNode} (hd : cert.depth ≤ nn + 2) (hv : AutomsOk (fun (γ : Array Nat) => checkAutom g γ = true) cert) : AutomsOk (fun (γ : Array Nat) => containsGamma (validGammas g cert) γ = true) cert

A certificate whose records all pass checkAutom has every record's generator in its own validated store.

theorem Hex.GraphIso.Nauty.certifyNode_replays {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) {vgens : List (Array Nat)} (hv : ∀ (γ : Array Nat), γ ∈ vgens → checkAutom ctx.g γ = true) (tcLevel : Nat) (brows : List (VSet n)) (fuel level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (bcodes : List Nat) (st : AutState) : st.budget = none → st.exhausted = false → NodeOk n level lab ptn active → level + fuel ≤ n + 1 → n + 1 ≤ level + fuel → level ≤ bcount ptn level n → keyLe (specNode ctx tcLevel fuel level lab ptn active numcells) { codes := bcodes, rows := brows } → AutomsOk (fun (γ : Array Nat) => containsGamma vgens γ = true) (certifyNodeAutom ctx tcLevel fuel level lab ptn active numcells bcodes st).fst → ∃ (a : Bool), checkNode ctx tcLevel brows vgens fuel level lab ptn active numcells (certifyNodeAutom ctx tcLevel fuel level lab ptn active numcells bcodes st).fst bcodes = some a ∧ (a = false → keyCmp (specNode ctx tcLevel fuel level lab ptn active numcells) { codes := bcodes, rows := brows } = Ordering.lt)

A dominated walk's certificate replays: checkNode accepts it, and a some false verdict forces the subtree strictly below the claimed suffix.

def Hex.GraphIso.Nauty.tracedKey {n k : Nat} (G : Colored n k) : Key n

The traced key of the candidate producer, as produceCand claims it.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.produceCand_checkKey {n k : Nat} {G : Colored n k} {cert : CertNode} {B : Key n} (hp : produceCand G none = some (cert, B)) (hval : AutomsOk (fun (γ : Array Nat) => checkAutom (rowsOf G) γ = true) cert) (hdom : canonSpecKey G = B) : checkKey G cert B = true

The produced certificate replays: under domination (the traced key is the spec key) and store validity (every record's generator is a checked automorphism), checkKey accepts the produced pair.

theorem Hex.GraphIso.Nauty.certifyCanon?_isSome_of_dominated {n k : Nat} (G : Colored n k) (hdom : canonSpecKey G = tracedKey G) (hval : ∀ (cert : CertNode) (B : Key n), produceCand G none = some (cert, B) → AutomsOk (fun (γ : Array Nat) => checkAutom (rowsOf G) γ = true) cert) : (certifyCanon? G).isSome = true

Two hypotheses suffice for certifyCanon? totality: domination (the traced key is the spec key) and store validity (every produced record's generator is a checked automorphism).