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)
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)
:
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 })
:
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.