theorem Hex.GraphIso.Nauty.charge_of_budget_none {st : AutState} (h : st.budget = none) : st.charge = st

theorem Hex.GraphIso.Nauty.admit_budget {n : Nat} (ctx : Ctx n) (st : AutState) (γ : Array Nat) : (AutState.admit ctx st γ).budget = st.budget

theorem Hex.GraphIso.Nauty.admit_exhausted {n : Nat} (ctx : Ctx n) (st : AutState) (γ : Array Nat) : (AutState.admit ctx st γ).exhausted = st.exhausted

theorem Hex.GraphIso.Nauty.harvest_budget {n : Nat} (ctx : Ctx n) (st : AutState) (lab : Array Nat) : (AutState.harvest ctx st lab).budget = st.budget

theorem Hex.GraphIso.Nauty.harvest_exhausted {n : Nat} (ctx : Ctx n) (st : AutState) (lab : Array Nat) : (AutState.harvest ctx st lab).exhausted = st.exhausted

theorem Hex.GraphIso.Nauty.foldl_preserves {α σ : Type} (P : σ → Prop) (g : σ → α → σ) (h : ∀ (s : σ) (a : α), P s → P (g s a)) (l : List α) (s : σ) : P s → P (List.foldl g s l)

A fold preserves any invariant its step preserves.

theorem Hex.GraphIso.Nauty.certifyNodeAutom_budget {n : Nat} (ctx : Ctx n) (tcLevel fuel level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (bcodes : List Nat) (st : AutState) : st.budget = none → (certifyNodeAutom ctx tcLevel fuel level lab ptn active numcells bcodes st).snd.budget = none ∧ (certifyNodeAutom ctx tcLevel fuel level lab ptn active numcells bcodes st).snd.exhausted = st.exhausted

theorem Hex.GraphIso.Nauty.produceCand_none_isSome {n k : Nat} (G : Colored n k) : (produceCand G none).isSome = true

The trace-driven producer always returns a candidate under an absent budget: nothing in the walk can exhaust it.

theorem Hex.GraphIso.Nauty.rowsOf_symm {n k : Nat} (G : Colored n k) (i j : Nat) : i < n → j < n → (rowsOf G)[i]!.mem j = (rowsOf G)[j]!.mem i

theorem Hex.GraphIso.Nauty.rowsOf_loopless {n k : Nat} (G : Colored n k) (i : Nat) : i < n → (rowsOf G)[i]!.mem i = false

theorem Hex.GraphIso.Nauty.composePerm_getElem! (f π : Array Nat) {nn v : Nat} (hv : v < nn) : (composePerm f π nn)[v]! = f[π[v]!]!

theorem Hex.GraphIso.Nauty.composePerm_size (f π : Array Nat) (nn : Nat) : (composePerm f π nn).size = nn

theorem Hex.GraphIso.Nauty.image_comp {n : Nat} (σ τ : Nat → Nat) (s : VSet n) (hτ : ∀ (v : Nat), v < n → τ v < n) : VSet.image (fun (w : Nat) => σ (τ w)) s = VSet.image σ (VSet.image τ s)

image composes when the inner map stays in range.

theorem Hex.GraphIso.Nauty.checkAutom_compose {n : Nat} {g : Array (VSet n)} {f π : Array Nat} (hf : checkAutom g f = true) (hπ : checkAutom g π = true) : checkAutom g (composePerm f π n) = true

checkAutom is closed under the producer's witness composition.

theorem Hex.GraphIso.Nauty.image_id {n : Nat} (s : VSet n) : VSet.image (fun (w : Nat) => w) s = s

The identity image of a set is itself.

theorem Hex.GraphIso.Nauty.checkAutom_invPerm {n : Nat} {g : Array (VSet n)} {γ : Array Nat} (hγ : checkAutom g γ = true) : checkAutom g (invPerm γ) = true

checkAutom is closed under inversion, for bounded row sets.

theorem Hex.GraphIso.Nauty.checkAutom_range {n : Nat} {g : Array (VSet n)} : checkAutom g (Array.range n) = true

The identity array is a checked automorphism of any graph with bounded rows: the base case of witness composition.

theorem Hex.GraphIso.Nauty.isautom_iff {n : Nat} (ctx : Ctx n) (γ : Array Nat) : isautom ctx γ = true ↔ ∀ (i : Nat), i < n → ∀ (pos : Nat), pos ∈ ctx.g[i]!.toList → pos > i → ctx.g[γ[i]!]!.mem γ[pos]! = true

isautom returns true exactly when every edge maps to an edge under γ: the loop's specification, consumable with the rowsOf dischargers.

theorem Hex.GraphIso.Nauty.checkAutom_of_isautom {n : Nat} {ctx : Ctx n} {γ : Array Nat} (hsz : γ.size = n) (hperm : (List.map (fun (v : Nat) => γ[v]!) (List.range n)).isPerm (List.range n) = true) (hsymm : ∀ (i j : Nat), i < n → j < n → ctx.g[i]!.mem j = ctx.g[j]!.mem i) (hloop : ∀ (i : Nat), i < n → ctx.g[i]!.mem i = false) (haut : isautom ctx γ = true) : checkAutom ctx.g γ = true

The counting argument: for a permutation of [0, n), the admission filter's isautom implies the replay's checkAutom, over any symmetric, loopless, per-row-bounded row array. rowsOf_symm, rowsOf_loopless and rowsOf_bounded discharge the row hypotheses for rowsOf G. scatter_isPerm supplies the permutation hypothesis at the use site in Invariant/Store.

def Hex.GraphIso.Nauty.GensOk {n : Nat} (ctx : Ctx n) (st : AutState) : Prop

The store invariant: every stored generator pair passes checkAutom in both components.

Equations

• Hex.GraphIso.Nauty.GensOk ctx st = ∀ (p : Array Nat × Array Nat), p ∈ st.gens → Hex.GraphIso.Nauty.checkAutom ctx.g p.fst = true ∧ Hex.GraphIso.Nauty.checkAutom ctx.g p.snd = true

theorem Hex.GraphIso.Nauty.GensOk.admit {n : Nat} {ctx : Ctx n} {st : AutState} {γ : Array Nat} (hsymm : ∀ (i j : Nat), i < n → j < n → ctx.g[i]!.mem j = ctx.g[j]!.mem i) (hloop : ∀ (i : Nat), i < n → ctx.g[i]!.mem i = false) (hγ : isautom ctx γ = true → (List.map (fun (v : Nat) => γ[v]!) (List.range n)).isPerm (List.range n) = true) (hst : GensOk ctx st) : GensOk ctx (AutState.admit ctx st γ)

Admission preserves the store invariant: the filter re-verifies size, bounds, and isautom, so with the candidate's permutation side (hypothesis hγ) checkAutom_of_isautom validates the stored pair.

theorem Hex.GraphIso.Nauty.foldl_preserves_mem {α σ : Type} (P : σ → Prop) (g : σ → α → σ) (l : List α) : (∀ (s : σ) (a : α), a ∈ l → P s → P (g s a)) → ∀ (s : σ), P s → P (List.foldl g s l)

A fold preserves any invariant its step preserves on the list's elements.

theorem Hex.GraphIso.Nauty.GensOk.init {n : Nat} (ctx : Ctx n) (nn : Nat) (budget : Option Nat) : GensOk ctx (AutState.init nn budget)

The fresh store is trivially valid.

theorem Hex.GraphIso.Nauty.GensOk.foldl_admit {n : Nat} {ctx : Ctx n} {st : AutState} (hsymm : ∀ (i j : Nat), i < n → j < n → ctx.g[i]!.mem j = ctx.g[j]!.mem i) (hloop : ∀ (i : Nat), i < n → ctx.g[i]!.mem i = false) {autos : List (Array Nat)} (hautos : ∀ (γ : Array Nat), γ ∈ autos → isautom ctx γ = true → (List.map (fun (v : Nat) => γ[v]!) (List.range n)).isPerm (List.range n) = true) (hst : GensOk ctx st) : GensOk ctx (List.foldl (fun (st : AutState) (γ : Array Nat) => AutState.admit ctx st γ) st autos)

An admission fold over candidates that are permutations whenever they pass the admission filter (hypothesis hautos) stores only checkAutom-valid generator pairs.

theorem Hex.GraphIso.Nauty.witness?_checkAutom {n : Nat} {ctx : Ctx n} {rsLab : Array Nat} {tc o : Nat} {usable : Array (Array Nat × Array Nat)} {o' : Nat} {π : Array Nat} (hu : ∀ (p : Array Nat × Array Nat), p ∈ usable → checkAutom ctx.g p.fst = true ∧ checkAutom ctx.g p.snd = true) (hw : witness? n rsLab tc usable o = some (o', π)) : checkAutom ctx.g π = true

Over a store of checkAutom-valid generator pairs, every witness witness? returns passes checkAutom. The breadth-first queue holds only the identity and checkAutom-closed compositions.