def Hex.GraphIso.Nauty.ValidStore {n : Nat} (ctx : Ctx n) (S : List (Array Nat)) : Prop

Every stored generator passes the executable automorphism check against the context's rows.

Equations

• Hex.GraphIso.Nauty.ValidStore ctx S = ∀ (γ : Array Nat), γ ∈ S → Hex.GraphIso.Nauty.checkAutom ctx.g γ = true

theorem Hex.GraphIso.Nauty.validStore_append {n : Nat} {ctx : Ctx n} {S T : List (Array Nat)} (hS : ValidStore ctx S) (hT : ValidStore ctx T) : ValidStore ctx (S ++ T)

@[irreducible]

def Hex.GraphIso.Nauty.sweepG {n : Nat} (ctx : Ctx n) (tcLevel : Nat) (adm : Array Nat → Option (Key n) → List (Array Nat)) (fuel level : Nat) (rsLab rsPtn : Array Nat) (tc numcells : Nat) : List Nat → Key n × List (Array Nat) → Key n × List (Array Nat)

The child sweep with a growing store: each unpruned child is searched with the store as it stands, and the store that child returns, possibly grown at leaves below it, is what later siblings are pruned against.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.sweepG ctx tcLevel adm fuel level rsLab rsPtn tc numcells [] x✝ = x✝

@[irreducible]

def Hex.GraphIso.Nauty.stepG {n : Nat} (ctx : Ctx n) (tcLevel : Nat) (adm : Array Nat → Option (Key n) → List (Array Nat)) (fuel level : Nat) (rs : RefineSt n) (tail0 : Option (Key n)) (S : List (Array Nat)) : Key n × List (Array Nat)

One node step at a refined state. At a discrete leaf the oracle's proposals join the store. At a live node the first child absorbs the incumbent and sweepG threads the store across the rest.

Equations

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

@[irreducible]

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

Branch-and-bound with code prune, generator prune, and a store that grows at leaves and travels forward through the search order.

Equations

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

theorem Hex.GraphIso.Nauty.keysMax_concat {n : Nat} (k y : Key n) (l : List (Key n)) : keysMax k (l ++ [y]) = keyMax (keysMax k l) y

theorem Hex.GraphIso.Nauty.incMax_keyMax {n : Nat} (tail0 : Option (Key n)) (m y : Key n) : keyMax (incMax tail0 m) y = incMax tail0 (keyMax m y)

theorem Hex.GraphIso.Nauty.keysMax_range'_covered {n : Nat} {key : Nat → Key n} {j : Nat} (hj : 1 ≤ j) (hcov : ∃ (o' : Nat), o' < j ∧ key o' = key j) : keysMax (key 0) (List.map key (List.range' 1 j)) = keysMax (key 0) (List.map key (List.range' 1 (j - 1)))

The maximum over child positions 0..j collapses to the maximum over 0..j-1 when position j's key repeats an earlier one.

theorem Hex.GraphIso.Nauty.map_range'_one {α : Type} (f : Nat → α) (m : Nat) : List.map f (List.range' 1 m) = List.map f (List.map (fun (x : Nat) => x + 1) (List.range m))

Child positions 1..m as a shifted range.

theorem Hex.GraphIso.Nauty.keysMax_range'_snoc {n : Nat} {key : Nat → Key n} {j : Nat} (hj : 1 ≤ j) : keyMax (keysMax (key 0) (List.map key (List.range' 1 (j - 1)))) (key j) = keysMax (key 0) (List.map key (List.range' 1 j))

Extending the maximum over 0..j-1 by position j's key gives the maximum over 0..j.

theorem Hex.GraphIso.Nauty.sweepG_eq {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) {adm : Array Nat → Option (Key n) → List (Array Nat)} (hadm : ∀ (lab : Array Nat) (inc : Option (Key n)), ValidStore ctx (adm lab inc)) (tcLevel fuel level : Nat) (rsLab rsPtn : Array Nat) (tc m numcells : Nat) (tail0 : Option (Key n)) (c j : Nat) (acc : Key n × List (Array Nat)) : rsLab.size = n → LabOk rsLab n → rsPtn.size = n → rsPtn[rsPtn.size - 1]! ≤ level → (∀ (q : Nat), rsPtn[q]! ≤ level ∨ rsPtn[q]! = n + 2) → IsCell rsPtn level tc (m + 1) → tc + (m + 1) ≤ n → level + 1 + fuel ≤ n + 1 → j + c = m + 1 → 1 ≤ j → ValidStore ctx acc.snd → acc.fst = incMax tail0 (keysMax (childKey ctx tcLevel fuel level rsLab rsPtn tc numcells 0) (List.map (childKey ctx tcLevel fuel level rsLab rsPtn tc numcells) (List.range' 1 (j - 1)))) → (sweepG ctx tcLevel adm fuel level rsLab rsPtn tc numcells (List.range' j c) acc).fst = incMax tail0 (keysMax (childKey ctx tcLevel fuel level rsLab rsPtn tc numcells 0) (List.map (childKey ctx tcLevel fuel level rsLab rsPtn tc numcells) (List.range' 1 m))) ∧ ValidStore ctx (sweepG ctx tcLevel adm fuel level rsLab rsPtn tc numcells (List.range' j c) acc).snd

The sweep from position j with a valid store computes the full sweep maximum: pruned positions are covered by earlier keys via the store valid at the moment of the test, and the store stays valid as it grows through the children.

theorem Hex.GraphIso.Nauty.stepG_eq {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) {adm : Array Nat → Option (Key n) → List (Array Nat)} (hadm : ∀ (lab : Array Nat) (inc : Option (Key n)), ValidStore ctx (adm lab inc)) (tcLevel fuel level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (tail0 : Option (Key n)) (S : List (Array Nat)) : NodeOk n level lab ptn active → level + (fuel + 1) ≤ n + 1 → ValidStore ctx S → (stepG ctx tcLevel adm fuel level (refine ctx level lab ptn active numcells) tail0 S).fst = 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) ∧ ValidStore ctx (stepG ctx tcLevel adm fuel level (refine ctx level lab ptn active numcells) tail0 S).snd

One growing-store step at a refined state computes the incumbent maximum against the unpruned node key.

theorem Hex.GraphIso.Nauty.searchNodeG_eq {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) {adm : Array Nat → Option (Key n) → List (Array Nat)} (hadm : ∀ (lab : Array Nat) (inc : Option (Key n)), ValidStore ctx (adm lab inc)) (tcLevel fuel level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (inc : Option (Key n)) (S : List (Array Nat)) : NodeOk n level lab ptn active → level + fuel ≤ n + 1 → ValidStore ctx S → (searchNodeG ctx tcLevel adm fuel level lab ptn active numcells inc S).fst = incMax inc (specNode ctx tcLevel fuel level lab ptn active numcells) ∧ ValidStore ctx (searchNodeG ctx tcLevel adm fuel level lab ptn active numcells inc S).snd

The growing-store branch-and-bound computes exactly the maximum of the incumbent and the unpruned subtree key, and returns a valid store, for any valid initial store and any oracle proposing only checked automorphisms.

def Hex.GraphIso.Nauty.searchCanonG (n : Nat) (adm : Array Nat → Option (Key n) → List (Array Nat)) (gens0 : List (Array Nat)) (g : Array (VSet n)) (lab0 : Array Nat) (cellEnds : List Nat) : Key n

The growing-store search from an empty incumbent: code prune, generator prune, and a store seeded with gens0 that grows at leaves by the oracle's proposals.

Equations

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

theorem Hex.GraphIso.Nauty.searchCanonG_key {n k : Nat} (G : Colored n k) {adm : Array Nat → Option (Key n) → List (Array Nat)} (hadm : ∀ (lab : Array Nat) (inc : Option (Key n)), ValidStore { g := rowsOf G } (adm lab inc)) {gens0 : List (Array Nat)} (hv : ValidStore { g := rowsOf G } gens0) : searchCanonG n adm gens0 (rowsOf G) (initialPartition G).fst (initialPartition G).snd = canonSpecKey G

For any valid seed store and any oracle proposing only checked automorphisms, the growing-store search computes the nauty-semantic canonical key.