def Hex.GraphIso.Nauty.autPruned (nn : Nat) (gens : List (Array Nat)) (rsLab rsPtn : Array Nat) (level tc o : Nat) : Bool

Pairwise generator skip for child o at a node: some stored generator maps this child's labelling, cell by cell, to an earlier sibling's. This is the executable form of the .autom replay condition.

Equations

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

@[irreducible]

def Hex.GraphIso.Nauty.stepA {n : Nat} (ctx : Ctx n) (tcLevel : Nat) (gens : List (Array Nat)) (fuel level : Nat) (rs : RefineSt n) (tail0 : Option (Key n)) : Key n

One node of the automorphism-and-code-pruned model search at an already-refined state: leaf comparison when discrete, otherwise the child sweep skipping generator-pruned positions.

Equations

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

@[irreducible]

def Hex.GraphIso.Nauty.searchNodeA {n : Nat} (ctx : Ctx n) (tcLevel : Nat) (gens : List (Array Nat)) : Nat → Nat → Array Nat → Array Nat → VSet n → Nat → Option (Key n) → Key n

Branch-and-bound with both prunes: the incumbent's code prunes a subtree exactly as in searchNode, and stored generators prune sibling positions among the children of a node. It is not trusted as an evaluator. The theorem searchNodeA_eq verifies it against specNode.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.searchNodeA ctx tcLevel gens 0 x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = x✝.getD { codes := [], rows := [] }
• Hex.GraphIso.Nauty.searchNodeA ctx tcLevel gens fuel.succ x✝⁴ x✝³ x✝² x✝¹ x✝ none = Hex.GraphIso.Nauty.stepA ctx tcLevel gens fuel x✝⁴ (Hex.GraphIso.Nauty.refine ctx x✝⁴ x✝³ x✝² x✝¹ x✝) none

theorem Hex.GraphIso.Nauty.incMax_cons {n : Nat} (lc : Nat) (tail0 : Option (Key n)) (cs : List Nat) (rws : List (VSet n)) : incMax (Option.map (fun (t : Key n) => { codes := lc :: t.codes, rows := t.rows }) tail0) { codes := lc :: cs, rows := rws } = { codes := lc :: (incMax tail0 { codes := cs, rows := rws }).codes, rows := (incMax tail0 { codes := cs, rows := rws }).rows }

theorem Hex.GraphIso.Nauty.foldl_incMax {n : Nat} {f : Option (Key n) → Nat → Option (Key n)} {key : Nat → Key n} (os : List Nat) : (∀ (acc : Option (Key n)) (o : Nat), o ∈ os → f acc o = some (incMax acc (key o))) → ∀ (t : Key n), List.foldl f (some t) os = some (keysMax t (List.map key os))

theorem Hex.GraphIso.Nauty.foldl_incMax_cons {n : Nat} {f : Option (Key n) → Nat → Option (Key n)} {key : Nat → Key n} {o : Nat} {os : List Nat} (h : ∀ (acc : Option (Key n)) (x : Nat), x ∈ o :: os → f acc x = some (incMax acc (key x))) (tail0 : Option (Key n)) : List.foldl f tail0 (o :: os) = some (incMax tail0 (keysMax (key o) (List.map key os)))

theorem Hex.GraphIso.Nauty.surviving_key {n : Nat} {p : Nat → Bool} {key : Nat → Key n} {m : Nat} (hcov : ∀ (o : Nat), o < m → p o = false → ∃ (o' : Nat), o' < o ∧ key o' = key o) (fuel o : Nat) : o ≤ fuel → o < m → ∃ (o'' : Nat), o'' ≤ o ∧ p o'' = true ∧ key o'' = key o

theorem Hex.GraphIso.Nauty.keysMax_head_filter {n : Nat} {key : Nat → Key n} {p : Nat → Bool} {m : Nat} (hcov : ∀ (o : Nat), o < m + 1 → p o = false → ∃ (o' : Nat), o' < o ∧ key o' = key o) : keysMax (key 0) (List.map key (List.filter p (List.map (fun (x : Nat) => x + 1) (List.range m)))) = keysMax (key 0) (List.map key (List.map (fun (x : Nat) => x + 1) (List.range m)))

theorem Hex.GraphIso.Nauty.childKey_of_autPruned {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) {gens : List (Array Nat)} (hv : ∀ (γ : Array Nat), γ ∈ gens → checkAutom ctx.g γ = true) (tcLevel fuel level : Nat) {rsLab rsPtn : Array Nat} {tc lenT numcells o : 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) (hlf : level + 1 + fuel ≤ n + 1) (hpr : autPruned n gens rsLab rsPtn level tc o = true) : ∃ (o' : Nat), o' < o ∧ childKey ctx tcLevel fuel level rsLab rsPtn tc numcells o' = childKey ctx tcLevel fuel level rsLab rsPtn tc numcells o

theorem Hex.GraphIso.Nauty.stepA_eq {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) {gens : List (Array Nat)} (hv : ∀ (γ : Array Nat), γ ∈ gens → checkAutom ctx.g γ = true) (tcLevel fuel level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (tail0 : Option (Key n)) : NodeOk n level lab ptn active → level + (fuel + 1) ≤ n + 1 → stepA ctx tcLevel gens fuel level (refine ctx level lab ptn active numcells) tail0 = incMax (Option.map (fun (t : Key n) => { codes := (refine ctx level lab ptn active numcells).longcode :: t.codes, rows := t.rows }) tail0) (specNode ctx tcLevel (fuel + 1) level lab ptn active numcells)

One pruned step at a refined state computes the incumbent maximum against the unpruned node key, the node's leading code absorbed on both sides.

theorem Hex.GraphIso.Nauty.searchNodeA_eq {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) {gens : List (Array Nat)} (hv : ∀ (γ : Array Nat), γ ∈ gens → checkAutom ctx.g γ = true) (tcLevel fuel level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (inc : Option (Key n)) : NodeOk n level lab ptn active → level + fuel ≤ n + 1 → searchNodeA ctx tcLevel gens fuel level lab ptn active numcells inc = incMax inc (specNode ctx tcLevel fuel level lab ptn active numcells)

The doubly-pruned branch-and-bound computes exactly the maximum of the incumbent and the unpruned subtree key, for any store of checked automorphisms of the rows.

def Hex.GraphIso.Nauty.searchCanonA (n : Nat) (gens : List (Array Nat)) (g : Array (VSet n)) (lab0 : Array Nat) (cellEnds : List Nat) : Key n

The doubly-pruned search from an empty incumbent and a generator store: skips code-dominated subtrees and generator-repeated sibling positions.

Equations

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

theorem Hex.GraphIso.Nauty.searchCanonA_key {n k : Nat} (G : Colored n k) {gens : List (Array Nat)} (hv : ∀ (γ : Array Nat), γ ∈ gens → checkAutom (rowsOf G) γ = true) : searchCanonA n gens (rowsOf G) (initialPartition G).fst (initialPartition G).snd = canonSpecKey G

For any store of checked automorphisms of the rows, the doubly-pruned search computes the nauty-semantic canonical key.