theorem Hex.GraphIso.Nauty.scatter_isPerm {nn : Nat} {γ lab₁ lab₂ : Array Nat} (hsz₁ : lab₁.size = nn) (hp₁ : lab₁.toList.Perm (List.range nn)) (hsz₂ : lab₂.size = nn) (hp₂ : lab₂.toList.Perm (List.range nn)) (hsc : ∀ (i : Nat), i < nn → γ[lab₁[i]!]! = lab₂[i]!) : (List.map (fun (v : Nat) => γ[v]!) (List.range nn)).isPerm (List.range nn) = true

The scatter of one permutation labelling over another is a permutation of [0, n): the isPerm side condition that checkAutom_of_isautom consumes, produced from the two labellings' permutation properties.

theorem Hex.GraphIso.Nauty.checkAutom_scatter_of_isautom {n : Nat} {ctx : Ctx n} {γ lab₁ lab₂ : Array Nat} (hγsz : γ.size = n) (hsz₁ : lab₁.size = n) (hp₁ : lab₁.toList.Perm (List.range n)) (hsz₂ : lab₂.size = n) (hp₂ : lab₂.toList.Perm (List.range n)) (hsc : ∀ (i : Nat), i < n → γ[lab₁[i]!]! = lab₂[i]!) (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 code-1 admission under its explicit isautom guard: the scatter of the leaf labelling over the first-path labelling passes checkAutom when the isautom scan accepted it.

theorem Hex.GraphIso.Nauty.checkAutom_scatter_of_leafRows_eq {n : Nat} {ctx : Ctx n} {γ lab₁ lab₂ : Array Nat} (hγsz : γ.size = n) (hsz₁ : lab₁.size = n) (hp₁ : lab₁.toList.Perm (List.range n)) (hsz₂ : lab₂.size = n) (hp₂ : lab₂.toList.Perm (List.range n)) (hsc : ∀ (i : Nat), i < n → γ[lab₁[i]!]! = lab₂[i]!) (hrows : leafRows ctx lab₁ = leafRows ctx lab₂) : checkAutom ctx.g γ = true

The code-2 admission: two permutation labellings presenting equal leaf rows are joined by an automorphism, so the scatter passes checkAutom with no isautom scan. Equal rows mean the two relabelled graphs coincide; transporting one row identity back through the labellings' inverses shows the scatter preserves every row.

theorem Hex.GraphIso.Nauty.foldl_scatter_size (lab₁ lab₂ : Array Nat) (l : List Nat) (base : Array Nat) : (List.foldl (fun (r : Array Nat) (i : Nat) => r.set! lab₁[i]! lab₂[i]!) base l).size = base.size

A scatter fold preserves the size of its workspace.

theorem Hex.GraphIso.Nauty.foldl_scatter_getElem {lab₁ lab₂ : Array Nat} {nn : Nat} (hinj : ∀ (a b : Nat), a < nn → b < nn → lab₁[a]! = lab₁[b]! → a = b) {base : Array Nat} (hbb : ∀ (i : Nat), i < nn → lab₁[i]! < base.size) {m : Nat} : m ≤ nn → ∀ {j : Nat}, j < m → (List.foldl (fun (r : Array Nat) (i : Nat) => r.set! lab₁[i]! lab₂[i]!) base (List.range m))[lab₁[j]!]! = lab₂[j]!

After scanning an injective source prefix, every scanned source slot contains its corresponding target value.

theorem Hex.GraphIso.Nauty.processnode_genTrace {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hinj₁ : ∀ (a b : Nat), a < n → b < n → st.firstlab[a]! = st.firstlab[b]! → a = b) (hb₁ : ∀ (i : Nat), i < n → st.firstlab[i]! < n) (hinj₂ : ∀ (a b : Nat), a < n → b < n → st.canonlab[a]! = st.canonlab[b]! → a = b) (hb₂ : ∀ (i : Nat), i < n → st.canonlab[i]! < n) : (processnode ctx level numcells st).snd.genTrace = st.genTrace ∨ ∃ (γ : Array Nat), (processnode ctx level numcells st).snd.genTrace = st.genTrace.push γ ∧ γ.size = n ∧ ((∀ (i : Nat), i < n → γ[st.firstlab[i]!]! = st.lab[i]!) ∧ st.firstcode[level + 1]! = codeSentinel ∧ isautom ctx γ = true ∨ (∀ (i : Nat), i < n → γ[st.canonlab[i]!]! = st.lab[i]!) ∧ st.compCanon = 0 ∧ st.canonlevel ≤ level ∧ (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst = 0)

processnode's effect on the admitted-generator trace: either nothing is pushed, or exactly one scatter is pushed, connecting the first-path labelling (code 1, at the recorded first-leaf depth and after an automorphism scan) or the incumbent labelling (code 2, under the testcanlab equality on the freshly completed canong) to the current leaf labelling. The injectivity and bound hypotheses on the two base labellings are permutation facts the run-level invariant carries; the scatter equations feed checkAutom_scatter_of_isautom and, through leafEvent_faithful's rows account, checkAutom_scatter_of_leafRows_eq.

theorem Hex.GraphIso.Nauty.processnode_genTrace_first {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (heq : (st.eqlevFirst == level) = true) (hsent : st.firstcode[level + 1]! = codeSentinel) (hnc : (numcells == n) = true) (hpass : isautom ctx (List.foldl (fun (w : Array Nat) (i : Nat) => w.set! st.firstlab[i]! st.lab[i]!) (Array.replicate n 0) (List.range n)) = true) : (processnode ctx level numcells st).snd.genTrace = st.genTrace.push (List.foldl (fun (w : Array Nat) (i : Nat) => w.set! st.firstlab[i]! st.lab[i]!) (Array.replicate n 0) (List.range n))

The successful code-one arm appends exactly the first-to-current scatter that passed its explicit automorphism scan.

theorem Hex.GraphIso.Nauty.processnode_firstCarrier {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hsz₁ : st.firstlab.size = n) (hp₁ : st.firstlab.toList.Perm (List.range n)) (hsz₂ : st.lab.size = n) (hp₂ : st.lab.toList.Perm (List.range n)) (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) (heq : (st.eqlevFirst == level) = true) (hsent : st.firstcode[level + 1]! = codeSentinel) (hnc : (numcells == n) = true) (hpass : isautom ctx (List.foldl (fun (w : Array Nat) (i : Nat) => w.set! st.firstlab[i]! st.lab[i]!) (Array.replicate n 0) (List.range n)) = true) : ∃ (γ : Array Nat), γ ∈ (processnode ctx level numcells st).snd.genTrace ∧ checkAutom ctx.g γ = true ∧ ∀ (i : Nat), i < n → γ[st.firstlab[i]!]! = st.lab[i]!

The successful code-one event exposes the exact checked carrier it appended, including its pointwise action from the first leaf to the current leaf.

theorem Hex.GraphIso.Nauty.processnode_genTrace_canon {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hcc : st.compCanon = 0) (hge : ¬level < st.canonlevel) (htie : (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst = 0) : (processnode ctx level numcells st).snd.genTrace = st.genTrace.push (List.foldl (fun (w : Array Nat) (i : Nat) => w.set! st.canonlab[i]! st.lab[i]!) (Array.replicate n 0) (List.range n))

The row-tied code-two arm appends exactly the incumbent-to-current scatter, independently of which greatest-common-ancestor return it takes.

theorem Hex.GraphIso.Nauty.processnode_canonCarrier {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hsz₁ : st.canonlab.size = n) (hp₁ : st.canonlab.toList.Perm (List.range n)) (hsz₂ : st.lab.size = n) (hp₂ : st.lab.toList.Perm (List.range n)) (hrows : leafRows ctx st.canonlab = leafRows ctx st.lab) (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hcc : st.compCanon = 0) (hge : ¬level < st.canonlevel) (htie : (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst = 0) : ∃ (γ : Array Nat), γ ∈ (processnode ctx level numcells st).snd.genTrace ∧ checkAutom ctx.g γ = true ∧ ∀ (i : Nat), i < n → γ[st.canonlab[i]!]! = st.lab[i]!

The code-two event exposes the exact checked carrier it appended from the incumbent leaf to the current leaf.

theorem Hex.GraphIso.Nauty.labInj_perm_range {lab : Array Nat} {n : Nat} (hsz : lab.size = n) (hlab : LabOk lab n) (hinj : LabInj lab n) : lab.toList.Perm (List.range n)

An injective bounded labelling of full size is a permutation of [0, n): the side condition of the checkAutom scatter exits, discharged from the node invariant the descents carry.

theorem Hex.GraphIso.Nauty.processnode_carrier {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hsz₁ : st.firstlab.size = n) (hok₁ : LabOk st.firstlab n) (hinj₁ : LabInj st.firstlab n) (hszL : st.lab.size = n) (hokL : LabOk st.lab n) (hinjL : LabInj st.lab n) (hsz₂ : st.canonlab.size = n) (hok₂ : LabOk st.canonlab n) (hinj₂ : LabInj st.canonlab n) (harm3 : (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst = 0 → leafRows ctx st.canonlab = leafRows ctx st.lab) : (processnode ctx level numcells st).snd.genTrace = st.genTrace ∨ ∃ (γ : Array Nat), (processnode ctx level numcells st).snd.genTrace = st.genTrace.push γ ∧ checkAutom ctx.g γ = true ∧ ((∀ (i : Nat), i < n → γ[st.firstlab[i]!]! = st.lab[i]!) ∨ ∀ (i : Nat), i < n → γ[st.canonlab[i]!]! = st.lab[i]!)

If processnode records a generator, the same generator is both checked and identified as the scatter from the first or incumbent leaf onto the current leaf.

theorem Hex.GraphIso.Nauty.processnode_checkAutom {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hsz₁ : st.firstlab.size = n) (hok₁ : LabOk st.firstlab n) (hinj₁ : LabInj st.firstlab n) (hszL : st.lab.size = n) (hokL : LabOk st.lab n) (hinjL : LabInj st.lab n) (hsz₂ : st.canonlab.size = n) (hok₂ : LabOk st.canonlab n) (hinj₂ : LabInj st.canonlab n) (harm3 : (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst = 0 → leafRows ctx st.canonlab = leafRows ctx st.lab) : (processnode ctx level numcells st).snd.genTrace = st.genTrace ∨ ∃ (γ : Array Nat), (processnode ctx level numcells st).snd.genTrace = st.genTrace.push γ ∧ checkAutom ctx.g γ = true

Every generator processnode admits passes checkAutom, given the run-level facts per arm: permutation facts for the three labellings (the run invariant carries them); the code-1 arm's mandatory isautom scan; and the code-2 arm's rows equality (harm3, discharged from the incumbent-store account: updatecan_inv completes canong to the incumbent's leaf rows and testcanlab_fst reads the tie as row equality).

def Hex.GraphIso.Nauty.GenTraceOk {n : Nat} (ctx : Ctx n) (st : SearchSt n) (P : Array Nat → Prop := fun (x : Array Nat) => True) : Prop

Every generator the run has recorded is a checked automorphism. The additional property P records admission facts such as initial colour preservation. This is the invariant the domination induction threads: processnode is the only primitive that writes genTrace, so every other event preserves it by its frame.

Equations

• Hex.GraphIso.Nauty.GenTraceOk ctx st P = ∀ (γ : Array Nat), γ ∈ st.genTrace → Hex.GraphIso.Nauty.checkAutom ctx.g γ = true ∧ P γ

theorem Hex.GraphIso.Nauty.GenTraceOk.check {n : Nat} {ctx : Ctx n} {st : SearchSt n} {P : Array Nat → Prop} (h : GenTraceOk ctx st P) {γ : Array Nat} (η : γ ∈ st.genTrace.toList) : checkAutom ctx.g γ = true

Read one checked-generator fact from the run-side store invariant.

theorem Hex.GraphIso.Nauty.genTraceOk_processnode {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} {P : Array Nat → Prop} (hprev : GenTraceOk ctx st P) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hsz₁ : st.firstlab.size = n) (hok₁ : LabOk st.firstlab n) (hinj₁ : LabInj st.firstlab n) (hszL : st.lab.size = n) (hokL : LabOk st.lab n) (hinjL : LabInj st.lab n) (hsz₂ : st.canonlab.size = n) (hok₂ : LabOk st.canonlab n) (hinj₂ : LabInj st.canonlab n) (harm3 : (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst = 0 → leafRows ctx st.canonlab = leafRows ctx st.lab) (hP : ∀ (γ : Array Nat), checkAutom ctx.g γ = true → ((∀ (i : Nat), i < n → γ[st.firstlab[i]!]! = st.lab[i]!) ∨ ∀ (i : Nat), i < n → γ[st.canonlab[i]!]! = st.lab[i]!) → P γ) : GenTraceOk ctx (processnode ctx level numcells st).snd P

The invariant survives the admission event. The only row clause is the incumbent tie behind the testcanlab arm; code 1 is scanned.