theorem
Hex.GraphIso.Nauty.Comparison.prepare
{n : Nat}
{ctx : Ctx n}
{tcLevel numcells : Nat}
{cs bs fs : List Nat}
{st : Search n}
(h : Comparison ctx cs bs fs st)
(hlen : cs.length ≤ n)
:
Node preparation advances both code machines by the actual refinement code and preserves the incoming semantic incumbent.
def
Hex.GraphIso.Nauty.codeContract
{n k : Nat}
(G : Colored n k)
(ctx : Ctx n)
(tcLevel : Nat)
:
Generic.Contract (Search n) n
Whole-call code comparisons retain the incoming path and monotonically increase the incumbent. A positive sweep comparison requires a first child.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.codes_node
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel : Nat}
{next : Generic.SweepFn (Search n) n}
(hn0 : 0 < n)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
(hnext : (codeContract G ctx tcLevel).sweepValid fuel (n + 1) next)
(cs bs fs : List Nat)
(numcells : Nat)
(st : Search n)
(hin : NodePre G ctx tcLevel (cs.length + 1) numcells st)
(hfuel : n + 1 ≤ cs.length + 1 + (fuel + 1))
(hc : Comparison ctx cs bs fs st)
:
have result := Generic.nodeStep ctx tcLevel next false (cs.length + 1) numcells st;
∃ (bs' : List Nat), ReturnCodes ctx cs bs' fs result.snd ∧ Generic.Grows (SearchState.key ctx bs st) (SearchState.key ctx bs' result.snd)
An off-path node settles its comparison at a leaf or through the first child of its sweep, then retains that result through its return.
theorem
Hex.GraphIso.Nauty.codes_advance
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : Nat}
{next : Generic.SweepFn (Search n) n}
(hnext : (codeContract G ctx tcLevel).sweepValid fuel cfuel next)
(first : Bool)
(level numcells tc tv1 tv index : Nat)
(cell : VSet n)
(out : Search n)
(exit : Exit)
(cs bs fs : List Nat)
(before : Option (Key n))
(hlen : cs.length = level)
(hcodes : ReturnCodes ctx cs bs fs out)
(hgrows : Generic.Grows before (SearchState.key ctx bs out))
(hfuel : n ≤ level + fuel)
(hcursor : n ≤ tv + (cfuel + 1))
(hready : SweepPre G ctx tcLevel first level numcells tc tv1 (some tv) cell (recover (n + 2) level out))
:
have result := Generic.advance (n + 2) next first level numcells tc tv1 tv cell index out exit;
∃ (bs' : List Nat), ReturnCodes ctx cs bs' fs result.snd.snd ∧ Generic.Grows before (SearchState.key ctx bs' result.snd.snd)
A returned child either passes its settled comparison outward or recovers it before the next surviving sibling.
theorem
Hex.GraphIso.Nauty.codes_sweep
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : Nat}
{next : Generic.SweepFn (Search n) n}
(hn0 : 0 < n)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
(hdescend : (codeContract G ctx tcLevel).nodeValid fuel (Generic.nodeCall ctx (n + 2) tcLevel fuel))
(hnext : (codeContract G ctx tcLevel).sweepValid fuel cfuel next)
(first : Bool)
(level numcells tc tv1 tv index : Nat)
(cell : VSet n)
(st : Search n)
(hin : SweepPre G ctx tcLevel first level numcells tc tv1 (some tv) cell st)
(hfuel : n ≤ level + fuel)
(hcursor : n ≤ tv + (cfuel + 1))
(cs bs fs : List Nat)
(hlen : cs.length = level)
(hc : Comparison ctx cs bs fs st)
(hphase : st.compCanon ≤ 0 ∨ first = false ∧ (some tv).isSome = true)
:
have result :=
Generic.sweepStep (n + 2) (Generic.nodeCall ctx (n + 2) tcLevel fuel) next first level numcells tc tv1 tv cell index
st;
∃ (bs' : List Nat), ReturnCodes ctx cs bs' fs result.snd.snd ∧ Generic.Grows (SearchState.key ctx bs st) (SearchState.key ctx bs' result.snd.snd)
The actual off-path child settles both comparisons. Skipping an orbit representative is allowed only after a preceding child settled them.
theorem
Hex.GraphIso.Nauty.codePolicy
{n k : Nat}
(G : Colored n k)
(ctx : Ctx n)
(tcLevel : Nat)
(hn0 : 0 < n)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
:
Generic.CallPolicy ctx (n + 2) tcLevel (codeContract G ctx tcLevel)
The shared recursion settles both code machines and never decreases an installed incumbent on any sufficiently bounded off-path call.
theorem
Hex.GraphIso.Nauty.node_codes
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel level numcells : Nat}
{st : Search n}
(hn0 : 0 < n)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
(hin : NodePre G ctx tcLevel level numcells st)
(hfuel : n + 1 ≤ level + fuel)
{cs bs fs : List Nat}
(hlen : cs.length + 1 = level)
(hc : Comparison ctx cs bs fs st)
:
have result := node false ctx (n + 2) tcLevel fuel level numcells st;
∃ (bs' : List Nat), ReturnCodes ctx cs bs' fs result.snd ∧ Generic.Grows (SearchState.key ctx bs st) (SearchState.key ctx bs' result.snd)
An actual off-path node returns recoverable comparisons and a monotone incumbent, retaining its incoming code path through every exit.
theorem
Hex.GraphIso.Nauty.sweep_codes
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{first : Bool}
{tcLevel fuel cfuel level numcells tc tv1 index : Nat}
{cursor : Option Nat}
{cell : VSet n}
{st : Search n}
(hn0 : 0 < n)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
(hin : SweepPre G ctx tcLevel first level numcells tc tv1 cursor cell st)
(hfuel : n ≤ level + fuel)
(hcursor : Generic.CursorFuel n cfuel cursor)
{cs bs fs : List Nat}
(hlen : cs.length = level)
(hc : Comparison ctx cs bs fs st)
(hphase : st.compCanon ≤ 0 ∨ first = false ∧ cursor.isSome = true)
:
have result := sweep first ctx (n + 2) tcLevel fuel cfuel level numcells tc tv1 cursor cell index st;
∃ (bs' : List Nat), ReturnCodes ctx cs bs' fs result.snd.snd ∧ Generic.Grows (SearchState.key ctx bs st) (SearchState.key ctx bs' result.snd.snd)
An actual later-sibling sweep transports settled comparisons across nonlocal returns and composes incumbent growth across its visited children.