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.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.