def Hex.GraphIso.Nauty.fixedContract {n k : Nat} (G : Colored n k) : Generic.Contract (Search n) n

Calls restore the fixed-point set they received. Freshness is supplied by singleton cells at each individualization site.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.fixed_node {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel : Nat} {next : Generic.SweepFn (Search n) n} (hn0 : 0 < n) (hnext : (fixedContract G).sweepValid fuel (n + 1) next) (first : Bool) (level numcells : Nat) (st : Search n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (hfixed : FixedCells level st) : (Generic.nodeStep ctx tcLevel next first level numcells st).snd.fixedpts = st.fixedpts

The local node operations preserve fixed vertices, and its child sweep restores the same set on every exit.

theorem Hex.GraphIso.Nauty.fixed_advance {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel cfuel : Nat} {next : Generic.SweepFn (Search n) n} (hn0 : 0 < n) (hnext : (fixedContract G).sweepValid fuel cfuel next) (first : Bool) (level numcells tc tv1 tv index : Nat) (cell : VSet n) (base out : Search n) (exit : Exit) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells base) (htarget : Generic.Target (fun (st : Search n) => st) level tc cell base) (hfixed : FixedCells level base) (hout : SearchOut G level level base out) (hf : out.fixedpts = base.fixedpts) : (Generic.advance (n + 2) next first level numcells tc tv1 tv cell index out exit).snd.snd.fixedpts = base.fixedpts

A completed child's fixed set remains restored through pruning and parent recovery, including every nonlocal return.

theorem Hex.GraphIso.Nauty.fixed_restore {n tv : Nat} {base out : Search n} (hf : out.fixedpts = base.fixedpts.insert tv) (hfresh : base.fixedpts.mem tv = false) : out.fixedpts.erase tv = base.fixedpts

Erasing a fresh child's temporary fixed vertex restores its parent set.

theorem Hex.GraphIso.Nauty.fixed_sweep {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel cfuel : Nat} {next : Generic.SweepFn (Search n) n} (hn0 : 0 < n) (hdescend : (fixedContract G).nodeValid fuel (Generic.nodeCall ctx (n + 2) tcLevel fuel)) (hnext : (fixedContract G).sweepValid fuel cfuel next) (first : Bool) (level numcells tc tv1 tv index : Nat) (cell : VSet n) (st : Search n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (htarget : Generic.Target (fun (st : Search n) => st) level tc cell st) (htv : cell.mem tv = true) (hfixed : FixedCells level st) : (Generic.sweepStep (n + 2) (Generic.nodeCall ctx (n + 2) tcLevel fuel) next first level numcells tc tv1 tv cell index st).snd.snd.fixedpts = st.fixedpts

One sweep iteration adds a fresh fixed vertex, recursively restores the child's set, then removes precisely that temporary vertex.

theorem Hex.GraphIso.Nauty.fixedPolicy {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel : Nat) (hn0 : 0 < n) : Generic.CallPolicy ctx (n + 2) tcLevel (fixedContract G)

Fixed-point restoration follows the same policy-parameterized recursion.

theorem Hex.GraphIso.Nauty.node_fixed {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells : Nat} {st : Search n} (first : Bool) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (hfixed : FixedCells level st) : (node first ctx (n + 2) tcLevel fuel level numcells st).snd.fixedpts = st.fixedpts

Every actual call restores its incoming fixed-point set, even when it returns past several ancestors or exhausts operational fuel.