theorem Hex.GraphIso.Nauty.mem_of_subset {n : Nat} {a b : VSet n} {u : Nat} (h : a.subset b = true) (hu : a.mem u = true) : b.mem u = true

A passed fix test is a pointwise inclusion of the fixed base.

def Hex.GraphIso.Nauty.windowSet (n : Nat) (lab : Array Nat) (tc len : Nat) : VSet n

The vertex set of a labelling window.

Equations

• Hex.GraphIso.Nauty.windowSet n lab tc len = List.foldl (fun (s : Hex.GraphIso.Nauty.VSet n) (w : Nat) => s.insert w) Hex.GraphIso.Nauty.VSet.empty (Hex.GraphIso.Nauty.segN lab tc len)

theorem Hex.GraphIso.Nauty.mem_windowSet {n : Nat} {lab : Array Nat} {tc len u : Nat} : (windowSet n lab tc len).mem u = true ↔ u < n ∧ u ∈ segN lab tc len

Window-set membership is window membership of a vertex.

theorem Hex.GraphIso.Nauty.windowSet_lt {n : Nat} {lab : Array Nat} {tc len u : Nat} (hu : (windowSet n lab tc len).mem u = true) : u < n

Every window vertex is a vertex.

theorem Hex.GraphIso.Nauty.windowSet_carry {n : Nat} {ptn lab γ : Array Nat} {level tc len u : Nat} (hstab : CellStab ptn level lab γ) (hic : IsCell ptn level tc len) (hsz : tc + len ≤ lab.size) (hok : LabOk lab n) (hu : (windowSet n lab tc len).mem u = true) : (windowSet n lab tc len).mem γ[u]! = true

Cell stabilization preserves the cell's vertex set.

def Hex.GraphIso.Nauty.PairOk {nn : Nat} (g : Array (VSet nn)) (ptn lab : Array Nat) (level : Nat) (fix mcr : VSet nn) : Prop

The reading of one stored (fix, mcr) pair at a node: every vertex outside mcr is carried strictly downward by a checked automorphism fixing fix pointwise and stabilizing the node's cells. The realizers are per-vertex: the explicit fmperm pairs use powers of the admitted generator, the implicit fmptn pairs the small-cell subtree theorem.

Equations

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

def Hex.GraphIso.Nauty.AutosOk {nn : Nat} (g : Array (VSet nn)) (ptn lab : Array Nat) (level : Nat) (autos : Array (VSet nn × VSet nn)) : Prop

The store ledger: every workspace pair reads validly at the node.

Equations

• Hex.GraphIso.Nauty.AutosOk g ptn lab level autos = ∀ (p : Hex.GraphIso.Nauty.VSet nn × Hex.GraphIso.Nauty.VSet nn), p ∈ autos.toList → Hex.GraphIso.Nauty.PairOk g ptn lab level p.fst p.snd

def Hex.GraphIso.Nauty.WorkspaceOk {n : Nat} (st : SearchSt n) : Prop

The bounded automorphism workspace has a positive capacity and has not grown beyond it.

Equations

• Hex.GraphIso.Nauty.WorkspaceOk st = (0 < st.wsCap ∧ st.autos.size ≤ st.wsCap)

theorem Hex.GraphIso.Nauty.WorkspaceOk.ofFields {n : Nat} {st out : SearchSt n} (h : WorkspaceOk st) (hcap : out.wsCap = st.wsCap) (hautos : out.autos = st.autos) : WorkspaceOk out

Workspace validity depends only on the capacity and pair array.

theorem Hex.GraphIso.Nauty.WorkspaceOk.push {n : Nat} {st : SearchSt n} {pair : VSet n × VSet n} (h : WorkspaceOk st) : WorkspaceOk (pushAuto st pair)

Admitting one pair preserves the bounded workspace invariant.

theorem Hex.GraphIso.Nauty.WorkspaceOk.pushCap {n : Nat} (st : SearchSt n) (pair : VSet n × VSet n) : (pushAuto st pair).wsCap = st.wsCap

pushAuto does not change the configured workspace capacity.

theorem Hex.GraphIso.Nauty.WorkspaceOk.processCap {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : SearchSt n) : (processnode ctx level numcells st).snd.wsCap = st.wsCap

processnode never changes the configured workspace capacity.

theorem Hex.GraphIso.Nauty.WorkspaceOk.prepCap {n : Nat} (level code : Nat) (st : SearchSt n) : (otherNodePrep level code st).wsCap = st.wsCap

Comparison preparation does not change workspace capacity.

theorem Hex.GraphIso.Nauty.WorkspaceOk.recoverCap (n inf level : Nat) (st : SearchSt n) : (recover n inf level st).wsCap = st.wsCap

Parent recovery does not change workspace capacity.

theorem Hex.GraphIso.Nauty.WorkspaceOk.firstCap {n : Nat} (level : Nat) (st : SearchSt n) : (firstterminal level st).wsCap = st.wsCap

First-leaf installation does not change workspace capacity.

theorem Hex.GraphIso.Nauty.autosOk_pushAuto {n : Nat} {g : Array (VSet n)} {ptn lab : Array Nat} {level : Nat} {st : SearchSt n} {pair : VSet n × VSet n} (hok : AutosOk g ptn lab level st.autos) (hp : PairOk g ptn lab level pair.fst pair.snd) : AutosOk g ptn lab level (pushAuto st pair).autos

Recording a valid pair keeps the ledger, in both the push and the cap-slot overwrite branch.

theorem Hex.GraphIso.Nauty.pushAuto_back {n : Nat} {st : SearchSt n} {pair : VSet n × VSet n} (hcap : 0 < st.wsCap) : (pushAuto st pair).autos.back? = some pair

With a positive bounded workspace, pushAuto leaves the admitted pair in the slot read by shortprune, both before and at capacity.

theorem Hex.GraphIso.Nauty.pairOk_descend {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) {lab ptn : Array Nat} {level tc len o : Nat} {active' : VSet n} {numcells' : Nat} {fix mcr : VSet n} (hp : PairOk ctx.g ptn lab level fix mcr) (hic : IsCell ptn level tc len) (hsize : tc + len ≤ ptn.size) (hlsz : lab.size = ptn.size) (ho : o < len) (hlen2 : 2 ≤ len) (hend : ptn[ptn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), ptn[q]! ≠ level + 1) (hvo : lab[tc + o]! < n) (hfixmem : fix.mem lab[tc + o]! = true) (hlab2 : LabOk (breakout n lab ptn (level + 1) tc lab[tc + o]!).fst n) (hsl2 : (breakout n lab ptn (level + 1) tc lab[tc + o]!).fst.size = n) (hsp2 : (breakout n lab ptn (level + 1) tc lab[tc + o]!).snd.fst.size = n) (hend2 : (breakout n lab ptn (level + 1) tc lab[tc + o]!).snd.fst[(breakout n lab ptn (level + 1) tc lab[tc + o]!).snd.fst.size - 1]! ≤ level + 1) (hstarts2 : ∀ (v : Nat), active'.mem v = true → v = 0 ∨ (breakout n lab ptn (level + 1) tc lab[tc + o]!).snd.fst[v - 1]! ≤ level + 1) : PairOk ctx.g (refine ctx (level + 1) (breakout n lab ptn (level + 1) tc lab[tc + o]!).fst (breakout n lab ptn (level + 1) tc lab[tc + o]!).snd.fst active' numcells').ptn (refine ctx (level + 1) (breakout n lab ptn (level + 1) tc lab[tc + o]!).fst (breakout n lab ptn (level + 1) tc lab[tc + o]!).snd.fst active' numcells').lab (level + 1) fix mcr

The ledger moves down one individualize-and-refine step for any pair whose fix covers the individualized vertex: each realizer's cell stabilization is pushed through breakout (it fixes the split vertex) and refine, and its other three clauses are untouched.

theorem Hex.GraphIso.Nauty.pruned_carried {n : Nat} {g : Array (VSet n)} {ptn lab : Array Nat} {level tc len : Nat} {fixedpts R : VSet n} (hok : LabOk lab n) (hs : lab.size = n) (hsp : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hic : IsCell ptn level tc len) (hsz : tc + len ≤ n) (hdrop : ∀ (u : Nat), u < n → (windowSet n lab tc len).mem u = true → R.mem u = false → ∃ (fix : VSet n), ∃ (mcr : VSet n), PairOk g ptn lab level fix mcr ∧ mcr.mem u = false ∧ ∀ (w : Nat), w < n → fixedpts.mem w = true → fix.mem w = true) (v : Nat) : v < n → (windowSet n lab tc len).mem v = true → ∃ (γ : Array Nat), checkAutom g γ = true ∧ (∀ (u : Nat), u < n → fixedpts.mem u = true → γ[u]! = u) ∧ CellStab ptn level lab γ ∧ (windowSet n lab tc len).mem γ[v]! = true ∧ R.mem γ[v]! = true

The descent, stated for an arbitrary surviving set R: whenever a dropped vertex is strictly carried down by some ledger realizer, every cell vertex is carried by a composite realizer onto a survivor.

theorem Hex.GraphIso.Nauty.exists_all_false {α : Type} {f : α → Bool} {l : List α} : l.all f = false → ∃ (x : α), x ∈ l ∧ f x = false

theorem Hex.GraphIso.Nauty.mem_longprune {n : Nat} (tcell fixedpts : VSet n) (v : Nat) (autos : Array (VSet n × VSet n)) : (longprune tcell fixedpts autos).mem v = (tcell.mem v && autos.toList.all fun (p : VSet n × VSet n) => !fixedpts.subset p.fst || p.snd.mem v)

Membership after longprune: the cell bit survives exactly when every fix-passing pair's mcr keeps it.

theorem Hex.GraphIso.Nauty.longprune_drop {n : Nat} {g : Array (VSet n)} {ptn lab : Array Nat} {level v : Nat} {fixedpts tcell : VSet n} {autos : Array (VSet n × VSet n)} (hv : v < n) (hmem : tcell.mem v = true) (hdrop : (longprune tcell fixedpts autos).mem v = false) (haut : ∀ (p : VSet n × VSet n), p ∈ autos.toList → fixedpts.subset p.fst = true → PairOk g ptn lab level p.fst p.snd) : ∃ (γ : Array Nat), checkAutom g γ = true ∧ CellStab ptn level lab γ ∧ γ[v]! < v

If longprune removes a current member, one applicable ledger pair carries it strictly downward while stabilizing the node's cells.

theorem Hex.GraphIso.Nauty.longprune_subset {n : Nat} {tcell fixedpts : VSet n} {autos : Array (VSet n × VSet n)} {v : Nat} (h : (longprune tcell fixedpts autos).mem v = true) : tcell.mem v = true

longprune only removes set members.

theorem Hex.GraphIso.Nauty.shortprune_subset {n : Nat} {tcell : VSet n} {st : SearchSt n} {v : Nat} (h : (shortprune tcell st).mem v = true) : tcell.mem v = true

shortprune only removes set members.

theorem Hex.GraphIso.Nauty.shortprune_drop {n : Nat} {g : Array (VSet n)} {ptn lab : Array Nat} {level v : Nat} {tcell : VSet n} {st : SearchSt n} (hv : v < n) (hmem : tcell.mem v = true) (hdrop : (shortprune tcell st).mem v = false) (hlast : ∀ (fix mcr : VSet n), st.autos.back? = some (fix, mcr) → PairOk g ptn lab level fix mcr) : ∃ (γ : Array Nat), checkAutom g γ = true ∧ CellStab ptn level lab γ ∧ γ[v]! < v

If shortprune removes a current member, the last ledger pair carries it strictly downward while stabilizing the node's cells.

theorem Hex.GraphIso.Nauty.longprune_carried {n : Nat} {g : Array (VSet n)} {ptn lab : Array Nat} {level tc len : Nat} {fixedpts : VSet n} {autos : Array (VSet n × VSet n)} (hok : LabOk lab n) (hs : lab.size = n) (hsp : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hic : IsCell ptn level tc len) (hsz : tc + len ≤ n) (haut : ∀ (p : VSet n × VSet n), p ∈ autos.toList → fixedpts.subset p.fst = true → PairOk g ptn lab level p.fst p.snd) (v : Nat) : v < n → (windowSet n lab tc len).mem v = true → ∃ (γ : Array Nat), checkAutom g γ = true ∧ (∀ (u : Nat), u < n → fixedpts.mem u = true → γ[u]! = u) ∧ CellStab ptn level lab γ ∧ (windowSet n lab tc len).mem γ[v]! = true ∧ (longprune (windowSet n lab tc len) fixedpts autos).mem γ[v]! = true

longprune soundness: under the ledger for fix-passing pairs, every vertex of the target cell is carried by a checked, base-fixing, cell-stabilizing automorphism onto a surviving vertex of the cell.

theorem Hex.GraphIso.Nauty.shortprune_carried {n : Nat} {g : Array (VSet n)} {ptn lab : Array Nat} {level tc len : Nat} {st : SearchSt n} (hok : LabOk lab n) (hs : lab.size = n) (hsp : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hic : IsCell ptn level tc len) (hsz : tc + len ≤ n) (hlast : ∀ (fix mcr : VSet n), st.autos.back? = some (fix, mcr) → st.fixedpts.subset fix = true ∧ PairOk g ptn lab level fix mcr) (v : Nat) : v < n → (windowSet n lab tc len).mem v = true → ∃ (γ : Array Nat), checkAutom g γ = true ∧ (∀ (u : Nat), u < n → st.fixedpts.mem u = true → γ[u]! = u) ∧ CellStab ptn level lab γ ∧ (windowSet n lab tc len).mem γ[v]! = true ∧ (shortprune (windowSet n lab tc len) st).mem γ[v]! = true

shortprune soundness: given the ledger reading of the most recent pair and its fix test (which is what the needshortprune protocol requires), every vertex of the target cell is carried onto a survivor.

theorem Hex.GraphIso.Nauty.fmperm_fix {perm : Array Nat} {nn : Nat} (hb : ∀ (v : Nat), v < nn → perm[v]! < nn) (hinj : ∀ (a b : Nat), a < nn → b < nn → perm[a]! = perm[b]! → a = b) {u : Nat} (hu : (fmperm perm nn).fst.mem u = true) : u < nn ∧ perm[u]! = u

fix of an fmperm pair holds only fixed points.

theorem Hex.GraphIso.Nauty.fmperm_mcr {perm : Array Nat} {nn : Nat} (hb : ∀ (v : Nat), v < nn → perm[v]! < nn) (hinj : ∀ (a b : Nat), a < nn → b < nn → perm[a]! = perm[b]! → a = b) {v : Nat} (hv : v < nn) (hmcr : (fmperm perm nn).snd.mem v = false) : ∃ (k : Nat), applyWord (List.replicate k perm) v < v

A vertex left out of an fmperm pair's mcr is carried strictly down by a forward power of the generator.

theorem Hex.GraphIso.Nauty.pairOk_fmperm {n : Nat} {g : Array (VSet n)} {ptn lab perm : Array Nat} {level : Nat} (hok : LabOk lab n) (hs : lab.size = n) (hsp : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hca : checkAutom g perm = true) (hstab : CellStab ptn level lab perm) : PairOk g ptn lab level (fmperm perm n).fst (fmperm perm n).snd

The fmperm pair of a checked, cell-stabilizing generator reads validly at the node: the realizers are the generator's forward powers.

theorem Hex.GraphIso.Nauty.fmptn_congr {lab lab' ptn ptn' : Array Nat} {level nn : Nat} (hnn : nn ≤ ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) (hcells : cells ptn level nn = cells ptn' level nn) (hperm : cellsPerm ptn level lab lab') : fmptn lab ptn level nn = fmptn lab' ptn' level nn

fmptn is unchanged when the two partitions list the same cells and the two labellings have the same contents in each such cell.

theorem Hex.GraphIso.Nauty.fmptn_cellsPerm {lab lab' ptn : Array Nat} {level nn : Nat} (hnn : nn ≤ ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) (hperm : cellsPerm ptn level lab lab') : fmptn lab ptn level nn = fmptn lab' ptn level nn

fmptn is unchanged when vertices are permuted within every cell at the level it reads.

theorem Hex.GraphIso.Nauty.SearchOut.fmptn {n k : Nat} {G : Colored n k} {level nn : Nat} {st out : SearchSt n} (h : SearchOut G level level st out) (hnn : nn ≤ st.ptn.size) (hend : st.ptn[st.ptn.size - 1]! ≤ level) : Nauty.fmptn out.lab out.ptn level nn = Nauty.fmptn st.lab st.ptn level nn

A quartet receipt preserves the implicit cheap-automorphism pair at its frozen boundary.

theorem Hex.GraphIso.Nauty.fmptn_fix {lab ptn : Array Nat} {level nn u : Nat} (hu : (fmptn lab ptn level nn).fst.mem u = true) : ∃ (c : Nat), (c, c) ∈ cells ptn level nn ∧ lab[c]! = u

fix of an fmptn pair holds only singleton-cell vertices.

theorem Hex.GraphIso.Nauty.fmptn_singleton {lab ptn : Array Nat} {level nn c : Nat} (hcell : (c, c) ∈ cells ptn level nn) (hlt : lab[c]! < nn) : (fmptn lab ptn level nn).fst.mem lab[c]! = true

Every singleton-cell vertex is present in the fix component of the implicit pair.

theorem Hex.GraphIso.Nauty.isCell_one_mono {ptn : Array Nat} {level saved c : Nat} (h : IsCell ptn level c 1) (hle : level ≤ saved) : IsCell ptn saved c 1

A singleton cell remains a singleton when only the comparison level is raised.

theorem Hex.GraphIso.Nauty.fmptn_mcr {lab ptn : Array Nat} {level nn c1 c2 p v : Nat} (hcell : (c1, c2) ∈ cells ptn level nn) (hp1 : c1 ≤ p) (hp2 : p ≤ c2) (hpv : lab[p]! = v) (hv : v < nn) (hmcr : (fmptn lab ptn level nn).snd.mem v = false) : ∃ (q : Nat), c1 ≤ q ∧ q ≤ c2 ∧ lab[q]! < v

A vertex left out of an fmptn pair's mcr has a strictly smaller cellmate.

theorem Hex.GraphIso.Nauty.pairOk_fmptn {nn : Nat} {g : Array (VSet nn)} {ptn lab labT ptnT : Array Nat} {level lvlT : Nat} (hcover : ∀ (v : Nat), v < nn → ∃ (p : Nat), ∃ (c1 : Nat), ∃ (c2 : Nat), (c1, c2) ∈ cells ptnT lvlT nn ∧ c1 ≤ p ∧ p ≤ c2 ∧ labT[p]! = v) (hreal : ∀ (v c1 c2 : Nat), v < nn → (c1, c2) ∈ cells ptnT lvlT nn → (∃ (p : Nat), c1 ≤ p ∧ p ≤ c2 ∧ labT[p]! = v) → (∃ (q : Nat), c1 ≤ q ∧ q ≤ c2 ∧ labT[q]! < v) → ∃ (γ : Array Nat), checkAutom g γ = true ∧ (∀ (u : Nat), u < nn → (fmptn labT ptnT lvlT nn).fst.mem u = true → γ[u]! = u) ∧ CellStab ptn level lab γ ∧ γ[v]! < v) : PairOk g ptn lab level (fmptn labT ptnT lvlT nn).fst (fmptn labT ptnT lvlT nn).snd

The fmptn pair reads validly given realizers for every non-minimal cell member: the small-cell subtree theorem's interface. hreal receives the vertex, its window, and a strictly smaller cellmate, and returns an automorphism fixing the pair's fix set.