theorem Hex.GraphIso.Nauty.worksetOf_congr_perm {n : Nat} {lab lab' : Array Nat} {lo hi : Nat} (hp : (segN lab lo (hi + 1 - lo)).Perm (segN lab' lo (hi + 1 - lo))) : worksetOf n lab lo hi = worksetOf n lab' lo hi

theorem Hex.GraphIso.Nauty.cellsPerm_segN_perm {lab lab' ptn : Array Nat} {level nn : Nat} (h : cellsPerm ptn level lab lab') (hnn : nn ≤ ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) (hendn : ptn[nn - 1]! ≤ level) : (segN lab 0 nn).Perm (segN lab' 0 nn)

Cell-contents equivalence permutes the whole labelling segment.

def Hex.GraphIso.Nauty.LabInj (lab : Array Nat) (nn : Nat) : Prop

The labelling is injective on the vertex range.

Equations

• Hex.GraphIso.Nauty.LabInj lab nn = ∀ (i j : Nat), i < nn → j < nn → lab[i]! = lab[j]! → i = j

theorem Hex.GraphIso.Nauty.labInj_of_perm {lab lab' : Array Nat} {nn : Nat} (hp : (segN lab' 0 nn).Perm (segN lab 0 nn)) (h : LabInj lab nn) : LabInj lab' nn

Injectivity transports across a whole-segment permutation.

theorem Hex.GraphIso.Nauty.segments_disjoint_of_labInj {lab : Array Nat} {nn a la b lb : Nat} (h : LabInj lab nn) (hab : a + la ≤ b) (hbn : b + lb ≤ nn) (v : Nat) : v ∈ segN lab a la → v ∈ segN lab b lb → False

Under an injective labelling, separated windows have disjoint members.

theorem Hex.GraphIso.Nauty.mem_activeUnion {n level : Nat} {st : RefineSt n} {v : Nat} : (activeUnion level st).mem v = true ↔ ∃ (p : Nat × Nat), p ∈ cells st.ptn level n ∧ st.active.mem p.fst = true ∧ (worksetOf n st.lab p.fst p.snd).mem v = true

Membership in the active union: some active cell's splitter set holds the vertex.

theorem Hex.GraphIso.Nauty.workset_submask_activeUnion {n level : Nat} {st : RefineSt n} {p : Nat × Nat} (hp : p ∈ cells st.ptn level n) (ha : st.active.mem p.fst = true) : (worksetOf n st.lab p.fst p.snd).inter (activeUnion level st) = worksetOf n st.lab p.fst p.snd

An active cell's splitter set lies inside the active union.

theorem Hex.GraphIso.Nauty.pairwise_rel_of_mem {α : Type} {R : α → α → Prop} {l : List α} : List.Pairwise R l → ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a = b ∨ R a b ∨ R b a

theorem Hex.GraphIso.Nauty.worksetOf_cells_disjoint {n level : Nat} {st : RefineSt n} (hinj : LabInj st.lab n) (hps : st.ptn.size = n) (hend : st.ptn[st.ptn.size - 1]! ≤ level) {p q : Nat × Nat} (hp : p ∈ cells st.ptn level n) (hq : q ∈ cells st.ptn level n) (hne : p ≠ q) : (worksetOf n st.lab p.fst p.snd).inter (worksetOf n st.lab q.fst q.snd) = VSet.empty

Distinct cells of an injective labelling have disjoint splitter sets.

theorem Hex.GraphIso.Nauty.inactive_and_activeUnion {n level : Nat} {st : RefineSt n} (hinj : LabInj st.lab n) (hps : st.ptn.size = n) (hend : st.ptn[st.ptn.size - 1]! ≤ level) {p : Nat × Nat} (hp : p ∈ cells st.ptn level n) (ha : st.active.mem p.fst = false) : (worksetOf n st.lab p.fst p.snd).inter (activeUnion level st) = VSet.empty

An inactive cell's splitter set misses the active union.

theorem Hex.GraphIso.Nauty.trivialCell_state {n level cell1 cell2 : Nat} {gRow : VSet n} {st : RefineSt n} (h12 : cell1 ≤ cell2) (hsz : cell2 < st.lab.size) : (trivialCell level gRow cell1 cell2 st).maxpos = st.maxpos ∧ ((trivialCell level gRow cell1 cell2 st).ptn = st.ptn ∧ (trivialCell level gRow cell1 cell2 st).active = st.active ∧ (trivialCell level gRow cell1 cell2 st).numcells = st.numcells ∨ ∃ (j : Nat), ∃ (x : Nat), cell1 ≤ j ∧ j < cell2 ∧ (trivialCell level gRow cell1 cell2 st).ptn = st.ptn.set! j level ∧ (trivialCell level gRow cell1 cell2 st).active = st.active.insert x ∧ (trivialCell level gRow cell1 cell2 st).numcells = st.numcells + 1 ∧ (x = cell1 ∨ x = j + 1) ∧ (st.active.mem cell1 = true → x = j + 1))

One processed cell of the trivial pass, the bookkeeping half: maxpos untouched, and either nothing changes or exactly one junction boundary is written together with one activation, the activated position being the junction successor whenever the cell was active.

theorem Hex.GraphIso.Nauty.refineTrivial_go_state {n level : Nat} {gRow : VSet n} (cs : List (Nat × Nat)) (st : RefineSt n) : (∀ (p : Nat × Nat), p ∈ cs → p.fst ≤ p.snd ∧ p.snd < st.lab.size) → List.Pairwise (fun (p q : Nat × Nat) => p.snd < q.fst) cs → st.ptn.size = st.lab.size → st.lab.size = n → (refineTrivial.go level gRow cs st).maxpos = st.maxpos ∧ (∀ (u : Nat), (∀ (p : Nat × Nat), p ∈ cs → u < p.fst ∨ p.snd < u) → (refineTrivial.go level gRow cs st).active.mem u = st.active.mem u) ∧ (∀ (q : Nat), (∀ (p : Nat × Nat), p ∈ cs → q < p.fst ∨ p.snd < q) → (refineTrivial.go level gRow cs st).ptn[q]! = st.ptn[q]!) ∧ (refineTrivial.go level gRow cs st).active.card + 2 * st.numcells ≤ st.active.card + 2 * (refineTrivial.go level gRow cs st).numcells ∧ st.numcells ≤ (refineTrivial.go level gRow cs st).numcells ∧ ∀ (p : Nat × Nat), p ∈ cs → ((∀ (q : Nat), p.fst ≤ q → q ≤ p.snd → (refineTrivial.go level gRow cs st).ptn[q]! = st.ptn[q]!) ∧ ∀ (u : Nat), p.fst ≤ u → u ≤ p.snd → (refineTrivial.go level gRow cs st).active.mem u = st.active.mem u) ∨ ∃ (j : Nat), ∃ (x : Nat), p.fst ≤ j ∧ j < p.snd ∧ (refineTrivial.go level gRow cs st).ptn[j]! = level ∧ (∀ (q : Nat), p.fst ≤ q → q ≤ p.snd → q ≠ j → (refineTrivial.go level gRow cs st).ptn[q]! = st.ptn[q]!) ∧ (x = p.fst ∨ x = j + 1) ∧ (st.active.mem p.fst = true → x = j + 1) ∧ (refineTrivial.go level gRow cs st).active.mem x = true ∧ ∀ (u : Nat), p.fst ≤ u → u ≤ p.snd → u ≠ x → (refineTrivial.go level gRow cs st).active.mem u = st.active.mem u

The trivial pass over a window list, the bookkeeping half: maxpos kept, partition and active bits outside the windows kept, the potential ledger balanced, and per window either nothing or one junction with one activation.

theorem Hex.GraphIso.Nauty.windowScan_active_state {n level cell1 cell2 : Nat} {counts : List Nat} (hc2 : cell2 < n) (vs : List Nat) (c1 : Nat) (maxcell : Int) (st : RefineSt n) : cell1 ≤ c1 → c1 + (List.map (multOf counts) vs).sum = cell2 + 1 → c1 = cell1 ∨ st.ptn[c1 - 1]! ≤ level ∨ c1 = cell2 + 1 → cell2 < st.ptn.size → (∀ (u : Nat), u ≤ cell1 ∨ cell2 < u → (windowScan level cell1 cell2 counts vs c1 maxcell st).active.mem u = st.active.mem u) ∧ (∀ (u : Nat), st.active.mem u = true → (windowScan level cell1 cell2 counts vs c1 maxcell st).active.mem u = true) ∧ (∀ (q : Nat), st.ptn[q]! ≤ level → (windowScan level cell1 cell2 counts vs c1 maxcell st).ptn[q]! ≤ level) ∧ (∀ (q : Nat), q < c1 → (windowScan level cell1 cell2 counts vs c1 maxcell st).ptn[q]! = st.ptn[q]!) ∧ (∀ (u : Nat), (windowScan level cell1 cell2 counts vs c1 maxcell st).active.mem u = true → st.active.mem u = true ∨ cell1 < u ∧ u ≤ cell2 ∧ (windowScan level cell1 cell2 counts vs c1 maxcell st).ptn[u - 1]! ≤ level) ∧ (∀ (u : Nat), c1 < u → u ≤ cell2 → (windowScan level cell1 cell2 counts vs c1 maxcell st).ptn[u - 1]! ≤ level → st.ptn[u - 1]! ≤ level ∨ (windowScan level cell1 cell2 counts vs c1 maxcell st).active.mem u = true) ∧ (0 < (List.map (multOf counts) vs).sum → c1 = cell1 ∨ (windowScan level cell1 cell2 counts vs c1 maxcell st).active.mem c1 = true) ∧ (windowScan level cell1 cell2 counts vs c1 maxcell st).active.card + 2 * st.numcells ≤ st.active.card + 2 * (windowScan level cell1 cell2 counts vs c1 maxcell st).numcells ∧ st.numcells ≤ (windowScan level cell1 cell2 counts vs c1 maxcell st).numcells ∧ (maxcell < 0 ∨ cell1 ≤ st.maxpos ∧ st.maxpos ≤ cell2 ∧ (st.maxpos = cell1 ∨ st.active.mem st.maxpos = true) → 0 < (List.map (multOf counts) vs).sum ∨ 0 ≤ maxcell → cell1 ≤ (windowScan level cell1 cell2 counts vs c1 maxcell st).maxpos ∧ (windowScan level cell1 cell2 counts vs c1 maxcell st).maxpos ≤ cell2 ∧ ((windowScan level cell1 cell2 counts vs c1 maxcell st).maxpos = cell1 ∨ (windowScan level cell1 cell2 counts vs c1 maxcell st).active.mem (windowScan level cell1 cell2 counts vs c1 maxcell st).maxpos = true))

The window scan's active-set ledger: bits at or below the cell start and beyond the cell end are untouched, the active set only grows, every new bit sits just after a boundary, every boundary the scan writes gets its successor activated (the successor of the last write being pending exactly while mass remains), the potential ledger balances, and the running largest-fragment position stays justified.

theorem Hex.GraphIso.Nauty.nontrivialCell_outcome {n : Nat} {ctx : Ctx n} {level cell1 cell2 : Nat} {workset : VSet n} {st : RefineSt n} (h12 : cell1 ≤ cell2) (hsz : cell2 < st.ptn.size) (hnb : cell2 < n) (hopen : ∀ (q : Nat), cell1 ≤ q → q < cell2 → st.ptn[q]! > level) : (∀ (u : Nat), u < cell1 ∨ cell2 < u → (nontrivialCell ctx level workset cell1 cell2 st).active.mem u = st.active.mem u) ∧ (∀ (q : Nat), q < cell1 ∨ cell2 ≤ q → (nontrivialCell ctx level workset cell1 cell2 st).ptn[q]! = st.ptn[q]!) ∧ (nontrivialCell ctx level workset cell1 cell2 st).ptn.size = st.ptn.size ∧ (nontrivialCell ctx level workset cell1 cell2 st).active.card + 2 * st.numcells ≤ st.active.card + 2 * (nontrivialCell ctx level workset cell1 cell2 st).numcells ∧ st.numcells ≤ (nontrivialCell ctx level workset cell1 cell2 st).numcells ∧ (st.active.mem cell1 = true → ∀ (u : Nat), cell1 ≤ u → u ≤ cell2 → u = cell1 ∨ (nontrivialCell ctx level workset cell1 cell2 st).ptn[u - 1]! ≤ level → (nontrivialCell ctx level workset cell1 cell2 st).active.mem u = true) ∧ (st.active.mem cell1 = false → ∃ (w : Nat), ∀ (u : Nat), cell1 ≤ u → u ≤ cell2 → u = cell1 ∨ (nontrivialCell ctx level workset cell1 cell2 st).ptn[u - 1]! ≤ level → u ≠ w → (nontrivialCell ctx level workset cell1 cell2 st).active.mem u = true)

One processed cell of the nontrivial pass, the bookkeeping half: active bits and boundaries outside the window untouched, the potential ledger balanced, and the two activation clauses. An active cell activates every fragment start, and an inactive one every fragment start but one.

theorem Hex.GraphIso.Nauty.refineNontrivial_go_state {n : Nat} {ctx : Ctx n} {level : Nat} {workset : VSet n} (cs : List (Nat × Nat)) (st : RefineSt n) : (∀ (p : Nat × Nat), p ∈ cs → p.fst ≤ p.snd ∧ p.snd < st.ptn.size ∧ p.snd < n) → List.Pairwise (fun (p q : Nat × Nat) => p.snd < q.fst) cs → (∀ (p : Nat × Nat), p ∈ cs → ∀ (q : Nat), p.fst ≤ q → q < p.snd → st.ptn[q]! > level) → (∀ (u : Nat), (∀ (p : Nat × Nat), p ∈ cs → u < p.fst ∨ p.snd < u) → (refineNontrivial.go ctx level workset cs st).active.mem u = st.active.mem u) ∧ (∀ (q : Nat), (∀ (p : Nat × Nat), p ∈ cs → q < p.fst ∨ p.snd ≤ q) → (refineNontrivial.go ctx level workset cs st).ptn[q]! = st.ptn[q]!) ∧ (refineNontrivial.go ctx level workset cs st).ptn.size = st.ptn.size ∧ (refineNontrivial.go ctx level workset cs st).active.card + 2 * st.numcells ≤ st.active.card + 2 * (refineNontrivial.go ctx level workset cs st).numcells ∧ st.numcells ≤ (refineNontrivial.go ctx level workset cs st).numcells ∧ ∀ (p : Nat × Nat), p ∈ cs → (st.active.mem p.fst = true → ∀ (u : Nat), p.fst ≤ u → u ≤ p.snd → u = p.fst ∨ (refineNontrivial.go ctx level workset cs st).ptn[u - 1]! ≤ level → (refineNontrivial.go ctx level workset cs st).active.mem u = true) ∧ (st.active.mem p.fst = false → ∃ (w : Nat), ∀ (u : Nat), p.fst ≤ u → u ≤ p.snd → u = p.fst ∨ (refineNontrivial.go ctx level workset cs st).ptn[u - 1]! ≤ level → u ≠ w → (refineNontrivial.go ctx level workset cs st).active.mem u = true)

The nontrivial pass over a window list, the bookkeeping half.

theorem Hex.GraphIso.Nauty.refineStep_state {n : Nat} {ctx : Ctx n} {level split1 : Nat} {st : RefineSt n} (hok : StOk n level st) (hmem : st.active.mem split1 = true) : (refineStep ctx level split1 st).active.card + 2 * st.numcells + 1 ≤ st.active.card + 2 * (refineStep ctx level split1 st).numcells ∧ st.numcells ≤ (refineStep ctx level split1 st).numcells ∧ ∀ (p : Nat × Nat), p ∈ cells st.ptn level n → (st.active.mem p.fst = true → p.fst ≠ split1 → ∀ (u : Nat), p.fst ≤ u → u ≤ p.snd → u = p.fst ∨ (refineStep ctx level split1 st).ptn[u - 1]! ≤ level → (refineStep ctx level split1 st).active.mem u = true) ∧ (st.active.mem p.fst = false ∨ p.fst = split1 → ∃ (w : Nat), ∀ (u : Nat), p.fst ≤ u → u ≤ p.snd → u = p.fst ∨ (refineStep ctx level split1 st).ptn[u - 1]! ≤ level → u ≠ w → (refineStep ctx level split1 st).active.mem u = true)

One refineStep, the bookkeeping half: the potential drops strictly, and per old cell an active non-splitter cell activates every fragment start while any other cell leaves at most one start inactive.

theorem Hex.GraphIso.Nauty.labInj_surj {lab : Array Nat} {n : Nat} (hsz : n ≤ lab.size) (hlab : LabOk lab n) (hinj : LabInj lab n) (v : Nat) : v < n → ∃ (i : Nat), i < n ∧ lab[i]! = v

An injective bounded labelling on n positions hits every vertex.