theorem Hex.GraphIso.Nauty.isCell_disj_or_eq {ptn : Array Nat} {level a la b lb : Nat} (ha : IsCell ptn level a la) (hb : IsCell ptn level b lb) : a = b ∧ la = lb ∨ a + la ≤ b ∨ b + lb ≤ a

Two maximal runs of the same partition are equal or disjoint.

theorem Hex.GraphIso.Nauty.certInv_transport {n : Nat} {ctx : Ctx n} {level split1 : Nat} {st r : RefineSt n} (hok : StOk n level st) (hrok : StOk n level r) (hinj : LabInj st.lab n) (hstarts : StartsOk level st) (hmem : st.active.mem split1 = true) (hs1 : split1 < n) (hRI : RefInv level st.lab st.ptn r) (hcc : ∀ (a len : Nat), IsCell r.ptn level a len → a + len ≤ n → ConstOn ctx (worksetOf n st.lab split1 (cellEnd st.ptn level split1)) (segN r.lab a len)) (hact3 : ∀ (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 ∨ r.ptn[u - 1]! ≤ level → r.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 ∨ r.ptn[u - 1]! ≤ level → u ≠ w → r.active.mem u = true)) (hinv : CertInv ctx level st) : CertInv ctx level r

The certificate invariant is preserved by any cell refinement which stabilizes the retired splitter and activates every fragment of an active non-splitter cell, leaving at most one inactive fragment of each other cell.

theorem Hex.GraphIso.Nauty.certInv_refineStep {n : Nat} {ctx : Ctx n} {level split1 : Nat} {st : RefineSt n} (hok : StOk n level st) (hinj : LabInj st.lab n) (hstarts : StartsOk level st) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hmem : st.active.mem split1 = true) (hs1 : split1 < n) (hinv : CertInv ctx level st) : CertInv ctx level (refineStep ctx level split1 st)

The executed dense refinement step supplies the partition, splitter, and activation facts of the shared certificate-transport theorem.

theorem Hex.GraphIso.Nauty.refineLoop_certInv {n : Nat} {ctx : Ctx n} {level : Nat} (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (fuel : Nat) (st : RefineSt n) : StOk n level st → LabInj st.lab n → StartsOk level st → CertInv ctx level st → st.active.card + 2 * n ≤ fuel + 2 * st.numcells → CertInv ctx level (refineLoop ctx level fuel st) ∧ (¬(refineLoop ctx level fuel st).numcells < n ∨ (refineLoop ctx level fuel st).active = VSet.empty)

The refinement loop leaves the invariants intact and, given fuel above the potential, exits only discrete or with an exhausted active set.

theorem Hex.GraphIso.Nauty.refine_equitable {n : Nat} {ctx : Ctx n} {level : Nat} {lab ptn : Array Nat} {active : VSet n} {numcells : Nat} (hls : lab.size = n) (hlab : LabOk lab n) (hps : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hinj : LabInj lab n) (hstarts : ∀ (v : Nat), active.mem v = true → v = 0 ∨ ptn[v - 1]! ≤ level) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hacc : bcount ptn level n = numcells) (hinv : CertInv ctx level { lab := lab, ptn := ptn, active := active, numcells := numcells, hint := 0, maxpos := 0, longcode := numcells }) : Equitable ctx level (refine ctx level lab ptn active numcells).lab (refine ctx level lab ptn active numcells).ptn

refine's output partition is equitable: entering with a labelling that is injective on the vertex range, an active set of cell starts, an accurate cell count, and the certificate invariant (vacuous when every cell is active), the refinement loop can only exit discrete or with the active set exhausted, and either way the final partition is equitable.