def Hex.GraphIso.Nauty.keyLe {n : Nat} (k1 k2 : Key n) : Prop

k1 ≤ k2 in the leaf-key order.

Equations

• Hex.GraphIso.Nauty.keyLe k1 k2 = (Hex.GraphIso.Nauty.keyCmp k1 k2 ≠ Ordering.gt)

theorem Hex.GraphIso.Nauty.keyLe_iff {n : Nat} {a b : Key n} : keyLe a b ↔ keyCmp b a ≠ Ordering.lt

theorem Hex.GraphIso.Nauty.keyLe_refl {n : Nat} (x : Key n) : keyLe x x

theorem Hex.GraphIso.Nauty.keyLe_of_eq {n : Nat} {a b : Key n} (h : a = b) : keyLe a b

theorem Hex.GraphIso.Nauty.keyLe_trans {n : Nat} {a b c : Key n} (h1 : keyLe a b) (h2 : keyLe b c) : keyLe a c

theorem Hex.GraphIso.Nauty.keyLe_antisym {n : Nat} {a b : Key n} (h1 : keyLe a b) (h2 : keyLe b a) : a = b

theorem Hex.GraphIso.Nauty.keysMax_le {n : Nat} {b k : Key n} {l : List (Key n)} (hk : keyLe k b) (hl : ∀ (y : Key n), y ∈ l → keyLe y b) : keyLe (keysMax k l) b

theorem Hex.GraphIso.Nauty.keyLe_keysMax {n : Nat} {y k : Key n} {l : List (Key n)} (hy : y = k ∨ y ∈ l) : keyLe y (keysMax k l)

theorem Hex.GraphIso.Nauty.keysMax_eq_of_le {n : Nat} {b k : Key n} {l : List (Key n)} (hk : keyLe k b) (hl : ∀ (y : Key n), y ∈ l → keyLe y b) (hb : b = k ∨ b ∈ l) : keysMax k l = b

theorem Hex.GraphIso.Nauty.keyMax_eq_left {n : Nat} {b y : Key n} (h : keyLe y b) : keyMax b y = b

A key that dominates its partner is the maximum of the two.

theorem Hex.GraphIso.Nauty.keyMax_eq_right {n : Nat} {b y : Key n} (h : keyCmp b y = Ordering.lt) : keyMax b y = y

When the first key compares below the second, the second is the maximum.

theorem Hex.GraphIso.Nauty.keyCmp_cons_lt {n c c' : Nat} (h : c < c') (cs cs' : List Nat) (r r' : List (VSet n)) : keyCmp { codes := c :: cs, rows := r } { codes := c' :: cs', rows := r' } = Ordering.lt

theorem Hex.GraphIso.Nauty.keyCmp_cons_gt {n c c' : Nat} (h : c' < c) (cs cs' : List Nat) (r r' : List (VSet n)) : keyCmp { codes := c :: cs, rows := r } { codes := c' :: cs', rows := r' } = Ordering.gt

theorem Hex.GraphIso.Nauty.keyCmp_cons_eq {n : Nat} (c : Nat) (cs cs' : List Nat) (r r' : List (VSet n)) : keyCmp { codes := c :: cs, rows := r } { codes := c :: cs', rows := r' } = keyCmp { codes := cs, rows := r } { codes := cs', rows := r' }

theorem Hex.GraphIso.Nauty.keyMax_cons {n : Nat} (c : Nat) (cs cs' : List Nat) (r r' : List (VSet n)) : keyMax { codes := c :: cs, rows := r } { codes := c :: cs', rows := r' } = { codes := c :: (keyMax { codes := cs, rows := r } { codes := cs', rows := r' }).codes, rows := (keyMax { codes := cs, rows := r } { codes := cs', rows := r' }).rows }

Prefixing a common code commutes with the key maximum.

theorem Hex.GraphIso.Nauty.keyLe_cons_tail {n c : Nat} {cs brest : List Nat} {r br : List (VSet n)} (h : keyLe { codes := c :: cs, rows := r } { codes := c :: brest, rows := br }) : keyLe { codes := cs, rows := r } { codes := brest, rows := br }

theorem Hex.GraphIso.Nauty.specNode_codes_head {n : Nat} (ctx : Ctx n) (tcLevel fuel level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) : ∃ (rest : List Nat), (specNode ctx tcLevel (fuel + 1) level lab ptn active numcells).codes = (refine ctx level lab ptn active numcells).longcode :: rest

theorem Hex.GraphIso.Nauty.specNode_autom {n : Nat} {ctx : Ctx n} {γ : Renaming n} (hg : RowsMap γ ctx.g ctx.g) (tcLevel fuel level : Nat) {lab₁ lab₂ ptn : Array Nat} {active : VSet n} {numcells : Nat} (hcp : cellsPerm ptn level lab₁ (Array.map γ.toFun lab₂)) (hs1 : lab₁.size = n) (hs2 : lab₂.size = n) (hok1 : LabOk lab₁ n) (hok2 : LabOk lab₂ n) (hsp : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hstarts : ∀ (v : Nat), active.mem v = true → v = 0 ∨ ptn[v - 1]! ≤ level) (hvals : ∀ (q : Nat), ptn[q]! ≤ level ∨ ptn[q]! = n + 2) (hlf : level + fuel ≤ n + 1) : specNode ctx tcLevel fuel level lab₂ ptn active numcells = specNode ctx tcLevel fuel level lab₁ ptn active numcells

If γ fixes the adjacency rows and carries the cells of lab₂ to the cells of lab₁, the two subtrees produce the same key.

theorem Hex.GraphIso.Nauty.isCell_mem_cells {ptn : Array Nat} {level a len nn : Nat} (h : IsCell ptn level a len) (hnn : nn ≤ ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) (ha : a < nn) : (a, a + len - 1) ∈ cells ptn level nn

theorem Hex.GraphIso.Nauty.cellsPerm_of_forall_cells {n : Nat} {ptn lab₁ lab₂' : Array Nat} {level : Nat} (hsp : ptn.size = n) (hs1 : lab₁.size = n) (hs2 : lab₂'.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hcells : ∀ (p : Nat × Nat), p ∈ cells ptn level n → (segN lab₁ p.fst (p.snd + 1 - p.fst)).Perm (segN lab₂' p.fst (p.snd + 1 - p.fst))) : cellsPerm ptn level lab₁ lab₂'

theorem Hex.GraphIso.Nauty.image_congr {n : Nat} {f f' : Nat → Nat} (s : VSet n) (h : ∀ (v : Nat), v < n → f v = f' v) : VSet.image f s = VSet.image f' s

def Hex.GraphIso.Nauty.checkAutom {n : Nat} (g : Array (VSet n)) (γ : Array Nat) : Bool

Executable check that γ names an automorphism of the rows g: a permutation of [0, n) whose induced row transport fixes g.

Equations

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

def Hex.GraphIso.Nauty.renamingOfArray (γ : Array Nat) (n : Nat) (hbound : ∀ (v : Nat), v < n → γ[v]! < n) (hinj : ∀ (a b : Nat), a < n → b < n → γ[a]! = γ[b]! → a = b) : Renaming n

The renaming named by a checked automorphism array.

Equations

• Hex.GraphIso.Nauty.renamingOfArray γ n hbound hinj = { toFun := fun (v : Nat) => if v < n then γ[v]! else v, inj := ⋯, maps := ⋯ }

theorem Hex.GraphIso.Nauty.checkAutom_sound {n : Nat} {g : Array (VSet n)} {γ : Array Nat} (hg : g.size = n) (h : checkAutom g γ = true) : ∃ (σ : Renaming n), (∀ (v : Nat), v < n → σ.toFun v = γ[v]!) ∧ RowsMap σ g g

def Hex.GraphIso.Nauty.checkCellsPerm (ptn lab₁ lab₂' : Array Nat) (level nn : Nat) : Bool

Executable check that two labellings fill each cell of ptn with the same vertices.

Equations

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

theorem Hex.GraphIso.Nauty.checkCellsPerm_sound {n : Nat} {ptn lab₁ lab₂' : Array Nat} {level : Nat} (hsp : ptn.size = n) (hs1 : lab₁.size = n) (hs2 : lab₂'.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (h : checkCellsPerm ptn lab₁ lab₂' level n = true) : cellsPerm ptn level lab₁ lab₂'

inductive Hex.GraphIso.Nauty.CertNode : Type

One node of a canonical certificate: the shape of the pruned search tree the producer visited. Prune variants justify discarding a subtree; node lists one entry per position of the target cell.

• leaf : CertNode

  The replayed state is discrete; compare its leaf key with the claimed best.

• codePrune : CertNode

  The subtree's refinement code falls below the best code at this depth.

• autom (o : Nat) (γ : Array Nat) : CertNode

  γ maps this subtree onto the earlier sibling at offset o.

• node (children : List CertNode) : CertNode

  Recurse into every position of the target cell.

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

The number of proof-rule records in a certificate tree.

Equations

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

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

The total record count of a list of certificate subtrees.

Equations

• Hex.GraphIso.Nauty.CertNode.sizeList [] = 0
• Hex.GraphIso.Nauty.CertNode.sizeList (c :: cs) = c.size + Hex.GraphIso.Nauty.CertNode.sizeList cs

def Hex.GraphIso.Nauty.gammaEq (a b : Array Nat) : Bool

Permutation-array equality through the list view, which the kernel reduces by projection (the Array BEq instance does not).

Equations

• Hex.GraphIso.Nauty.gammaEq a b = (a.toList == b.toList)

theorem Hex.GraphIso.Nauty.gammaEq_eq {a b : Array Nat} (h : gammaEq a b = true) : a = b

def Hex.GraphIso.Nauty.containsGamma (vgens : List (Array Nat)) (γ : Array Nat) : Bool

Membership of a permutation array in the validated-generator list, by explicit recursion.

Equations

• Hex.GraphIso.Nauty.containsGamma [] γ = false
• Hex.GraphIso.Nauty.containsGamma (g :: rest) γ = (Hex.GraphIso.Nauty.gammaEq g γ || Hex.GraphIso.Nauty.containsGamma rest γ)

theorem Hex.GraphIso.Nauty.containsGamma_mem {vgens : List (Array Nat)} {γ : Array Nat} (h : containsGamma vgens γ = true) : γ ∈ vgens

def Hex.GraphIso.Nauty.certGammas : Nat → CertNode → List (Array Nat) → List (Array Nat)

The automorphism arrays of a certificate, deduplicated, fuel bounded by the tree depth.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.certGammas 0 x✝¹ x✝ = x✝
• Hex.GraphIso.Nauty.certGammas n.succ Hex.GraphIso.Nauty.CertNode.leaf x✝ = x✝
• Hex.GraphIso.Nauty.certGammas n.succ Hex.GraphIso.Nauty.CertNode.codePrune x✝ = x✝
• Hex.GraphIso.Nauty.certGammas n.succ (Hex.GraphIso.Nauty.CertNode.autom o γ) x✝ = if Hex.GraphIso.Nauty.containsGamma x✝ γ = true then x✝ else γ :: x✝

def Hex.GraphIso.Nauty.validGammas {n : Nat} (g : Array (VSet n)) (cert : CertNode) : List (Array Nat)

Validate each distinct automorphism of a certificate once: the replay then looks records up in this list instead of re-validating the same generator at every .autom record.

Equations

• Hex.GraphIso.Nauty.validGammas g cert = List.filter (fun (γ : Array Nat) => Hex.GraphIso.Nauty.checkAutom g γ) (Hex.GraphIso.Nauty.certGammas (n + 2) cert [])

theorem Hex.GraphIso.Nauty.validGammas_sound {n : Nat} {g : Array (VSet n)} {cert : CertNode} {γ : Array Nat} (h : γ ∈ validGammas g cert) : checkAutom g γ = true

def Hex.GraphIso.Nauty.checkNode {n : Nat} (ctx : Ctx n) (tcLevel : Nat) (brows : List (VSet n)) (vgens : List (Array Nat)) : Nat → Nat → Array Nat → Array Nat → VSet n → Nat → CertNode → List Nat → Option Bool

Replay one node of the certificate. ⟨bcodes, brows⟩ is the claimed best key's suffix at this depth. Returns none if the replay fails, otherwise some achieved where achieved records whether this subtree attains the claimed best. Success certifies that every leaf key of the subtree is ≤ the claimed suffix.

One structural recursion (fuel-first, the child fold written inline with none absorbing, the per-node refine/breakout results bound once with let for shared reduction), so goals about certificates reduce in any module's kernel. checkChildren below spells the same child fold as a separate recursion, and checkNode_children_eq relates the two.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.checkNode ctx tcLevel brows vgens 0 x✝⁶ x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = none
• Hex.GraphIso.Nauty.checkNode ctx tcLevel brows vgens fuel.succ x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ [] = none
• Hex.GraphIso.Nauty.checkNode ctx tcLevel brows vgens fuel.succ x✝⁴ x✝³ x✝² x✝¹ x✝ (Hex.GraphIso.Nauty.CertNode.autom o γ) (bc :: brest) = none

def Hex.GraphIso.Nauty.checkChildren {n : Nat} (ctx : Ctx n) (tcLevel : Nat) (brows : List (VSet n)) (vgens : List (Array Nat)) (fuel level : Nat) (rsLab rsPtn : Array Nat) (tc numcells : Nat) (brest : List Nat) : List CertNode → Nat → Option Bool

The child fold of checkNode as its own recursion over the child list, from offset o on: the spelling the soundness induction consumes.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.checkChildren ctx tcLevel brows vgens fuel level rsLab rsPtn tc numcells brest [] x✝ = some false

theorem Hex.GraphIso.Nauty.checkNode_children_eq {n : Nat} (ctx : Ctx n) (tcLevel : Nat) (brows : List (VSet n)) (vgens : List (Array Nat)) (fuel level : Nat) (rsLab rsPtn : Array Nat) (tc numcells : Nat) (brest : List Nat) (certs : List CertNode) (o : Nat) (a : Bool) : List.foldl (fun (acc : Option Bool) (co : CertNode × Nat) => match acc with | none => none | some a => match match co.fst with | CertNode.autom o' γ => if (decide (o' < co.snd) && containsGamma vgens γ && checkCellsPerm (breakout n rsLab rsPtn (level + 1) tc rsLab[tc + co.snd]!).snd.fst (breakout n rsLab rsPtn (level + 1) tc rsLab[tc + o']!).fst (Array.map' (fun (w : Nat) => γ[w]!) (breakout n rsLab rsPtn (level + 1) tc rsLab[tc + co.snd]!).fst) (level + 1) n) = true then some false else none | x => checkNode ctx tcLevel brows vgens fuel (level + 1) (breakout n rsLab rsPtn (level + 1) tc rsLab[tc + co.snd]!).fst (breakout n rsLab rsPtn (level + 1) tc rsLab[tc + co.snd]!).snd.fst (breakout n rsLab rsPtn (level + 1) tc rsLab[tc + co.snd]!).snd.snd (numcells + 1) co.fst brest with | none => none | some a' => some (a || a')) (some a) (certs.zipIdx o) = match checkChildren ctx tcLevel brows vgens fuel level rsLab rsPtn tc numcells brest certs o with | none => none | some a' => some (a || a')

The inline child fold of checkNode agrees with the checkChildren spelling.

def Hex.GraphIso.Nauty.checkKey {n k : Nat} (G : Colored n k) (cert : CertNode) (B : Key n) : Bool

Replay a whole certificate against the claimed best key B.

Equations

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

structure Hex.GraphIso.Nauty.NodeOk (n level : Nat) (lab ptn : Array Nat) (active : VSet n) : Prop

The well-formedness facts carried down the replayed tree.

• labSize : lab.size = n
• labOk : LabOk lab n
• ptnSize : ptn.size = n
• ptnEnd : ptn[ptn.size - 1]! ≤ level
• starts (v : Nat) : active.mem v = true → v = 0 ∨ ptn[v - 1]! ≤ level
• vals (q : Nat) : ptn[q]! ≤ level ∨ ptn[q]! = n + 2

theorem Hex.GraphIso.Nauty.key_eta {n : Nat} (b : Key n) : { codes := b.codes, rows := b.rows } = b

theorem Hex.GraphIso.Nauty.map_congr_of_labOk {n : Nat} {f f' : Nat → Nat} {lab : Array Nat} (hok : LabOk lab n) (h : ∀ (w : Nat), w < n → f w = f' w) : Array.map f lab = Array.map f' lab

theorem Hex.GraphIso.Nauty.targetcell_facts {n : Nat} {ctx : Ctx n} {level tcLevel : Nat} (rsLab : Array Nat) {rsPtn : Array Nat} (hsp : rsPtn.size = n) (hend : rsPtn[rsPtn.size - 1]! ≤ level) (hdisc : discreteAt rsPtn level n = false) : ∃ (p : Nat × Nat), specTargetcell ctx rsLab rsPtn level tcLevel = p.fst ∧ p.fst < p.snd ∧ p.snd < n ∧ IsCell rsPtn level p.fst (p.snd + 1 - p.fst) ∧ cellEnd rsPtn level (p.fst + 1) = p.snd

The target cell of a live (non-discrete) replayed state.

theorem Hex.GraphIso.Nauty.childNodeOk {n level tc lenT o : Nat} {rsLab rsPtn : Array Nat} (hs : rsLab.size = n) (hok : LabOk rsLab n) (hsp : rsPtn.size = n) (hend : rsPtn[rsPtn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), rsPtn[q]! ≤ level ∨ rsPtn[q]! = n + 2) (hic : IsCell rsPtn level tc lenT) (hrange : tc + lenT ≤ n) (ho : o < lenT) : NodeOk n (level + 1) (breakout n rsLab rsPtn (level + 1) tc rsLab[tc + o]!).fst (rsPtn.set! tc (level + 1)) (VSet.empty.insert tc)

The state after individualizing one target-cell vertex is again well formed at the next level.

@[reducible]

def Hex.GraphIso.Nauty.childKey {n : Nat} (ctx : Ctx n) (tcLevel fuel level : Nat) (rsLab rsPtn : Array Nat) (tc numcells i : Nat) : Key n

The spec key of the i-th child of a replayed node.

Equations

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

theorem Hex.GraphIso.Nauty.specNode_keyLe_of_code_lt {n : Nat} {ctx : Ctx n} {level : Nat} {lab ptn : Array Nat} {active : VSet n} {numcells : Nat} (tcLevel fuel : Nat) {bc : Nat} (brest : List Nat) (brows : List (VSet n)) (hlt : (refine ctx level lab ptn active numcells).longcode < bc) : keyLe (specNode ctx tcLevel (fuel + 1) level lab ptn active numcells) { codes := bc :: brest, rows := brows }

A subtree whose refinement code falls below the best code at its depth is dominated.

theorem Hex.GraphIso.Nauty.step_assemble {n : Nat} {key : Nat → Key n} {Bt : Key n} {o m : Nat} {achieved a a' : Bool} (hach : achieved = (a || a')) (hk : keyLe (key o) Bt) (hka : a = true → key o = Bt) (hall : ∀ (i : Nat), o + 1 ≤ i → i < o + 1 + m → keyLe (key i) Bt) (hex : a' = true → ∃ (i : Nat), o + 1 ≤ i ∧ i < o + 1 + m ∧ key i = Bt) : (∀ (i : Nat), o ≤ i → i < o + (m + 1) → keyLe (key i) Bt) ∧ (achieved = true → ∃ (i : Nat), o ≤ i ∧ i < o + (m + 1) ∧ key i = Bt)

theorem Hex.GraphIso.Nauty.checkNode_sound {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) (cert : CertNode) (bcodes : List Nat) (achieved : Bool) (h : checkNode ctx tcLevel brows vgens fuel level lab ptn active numcells cert bcodes = some achieved) (hok : NodeOk n level lab ptn active) (hlf : level + fuel ≤ n + 1) : keyLe (specNode ctx tcLevel fuel level lab ptn active numcells) { codes := bcodes, rows := brows } ∧ (achieved = true → specNode ctx tcLevel fuel level lab ptn active numcells = { codes := bcodes, rows := brows })

theorem Hex.GraphIso.Nauty.checkChildren_sound {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) (rsLab rsPtn : Array Nat) (tc lenT numcells : Nat) (brest : List Nat) (certs : List CertNode) (o : Nat) (achieved : Bool) (h : checkChildren ctx tcLevel brows vgens fuel level rsLab rsPtn tc numcells brest certs o = some achieved) (hs : rsLab.size = n) (hok : LabOk rsLab n) (hsp : rsPtn.size = n) (hend : rsPtn[rsPtn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), rsPtn[q]! ≤ level ∨ rsPtn[q]! = n + 2) (hic : IsCell rsPtn level tc lenT) (hrange : tc + lenT ≤ n) (hlen : o + certs.length ≤ lenT) (hlf : level + 1 + fuel ≤ n + 1) (hprev : ∀ (i : Nat), i < o → keyLe (childKey ctx tcLevel fuel level rsLab rsPtn tc numcells i) { codes := brest, rows := brows }) : (∀ (i : Nat), o ≤ i → i < o + certs.length → keyLe (childKey ctx tcLevel fuel level rsLab rsPtn tc numcells i) { codes := brest, rows := brows }) ∧ (achieved = true → ∃ (i : Nat), o ≤ i ∧ i < o + certs.length ∧ childKey ctx tcLevel fuel level rsLab rsPtn tc numcells i = { codes := brest, rows := brows })

theorem Hex.GraphIso.Nauty.initial_nodeOk {n k : Nat} (G : Colored n k) (hn0 : 0 < n) : NodeOk n 1 (initialPartition G).fst (initPtn n (n + 2) (initialPartition G).snd) (initActive n (initialPartition G).snd)

The initial coloured-partition state is well formed.

theorem Hex.GraphIso.Nauty.checkKey_sound {n k : Nat} {G : Colored n k} {cert : CertNode} {B : Key n} (h : checkKey G cert B = true) : canonSpecKey G = B

A successful certificate replay pins the nauty-semantic canonical key.

def Hex.GraphIso.Nauty.validateKey? {n k : Nat} (G : Colored n k) (cand : CertNode) (Bc : Key n) : Option (CertNode × Key n)

Validate a candidate certificate and key through the trusted checkKey replay, independently of the producer that built them.

Equations

• Hex.GraphIso.Nauty.validateKey? G cand Bc = if Hex.GraphIso.Nauty.checkKey G cand Bc = true then some (cand, Bc) else none

theorem Hex.GraphIso.Nauty.validateKey?_sound {n k : Nat} {G : Colored n k} {cand : CertNode} {Bc : Key n} {cert : CertNode} {B : Key n} (h : validateKey? G cand Bc = some (cert, B)) : canonSpecKey G = B

Whatever passes validation carries the spec key.