structure
Hex.GraphIso.Nauty.Sparse.Aligned
{n : Nat}
(G : SparseGraph n)
(base : Nat)
(root : RefineSt n)
(level agreed numcells : Nat)
(st : State n)
:
Agreement with the saved first codes retains a native descent for the
current partition. Before comparison, agreed is the preceding level.
- descent : st.eqlevFirst = agreed → DescentAt G st.firsttc base root level numcells st
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.Aligned.mono
{n : Nat}
{G : SparseGraph n}
{base level agreed numcells : Nat}
{root : RefineSt n}
{st out : State n}
(h : Aligned G base root level agreed numcells st)
(he : out.eqlevFirst ≤ st.eqlevFirst)
(ht : out.firsttc = st.firsttc)
(hl : out.lab = st.lab)
(hp : out.ptn = st.ptn)
:
Aligned G base root level agreed numcells out
theorem
Hex.GraphIso.Nauty.Sparse.Aligned.compare
{n : Nat}
{G : SparseGraph n}
{base level numcells : Nat}
{root : RefineSt n}
{st : State n}
(h : Aligned G base root level (level - 1) numcells st)
(hl : 0 < level)
(code : Nat)
:
Aligned G base root level level numcells (compareCodes level code st)
theorem
Hex.GraphIso.Nauty.Sparse.Aligned.target
{n : Nat}
{G : SparseGraph n}
{base level numcells : Nat}
{root : RefineSt n}
{st : State n}
(h : Aligned G base root level level numcells st)
(tcLevel : Nat)
:
Aligned G base root level level numcells (chooseTarget false (Graph.ofGraph G) tcLevel level numcells st).snd.snd.snd
theorem
Hex.GraphIso.Nauty.Sparse.Aligned.classify
{n : Nat}
{G : SparseGraph n}
{base level numcells : Nat}
{root : RefineSt n}
{st : State n}
(h : Aligned G base root level level numcells st)
:
Aligned G base root level level numcells (Sparse.classify (Graph.ofGraph G) level numcells st).snd
theorem
Hex.GraphIso.Nauty.Sparse.Aligned.cheap
{n : Nat}
{G : SparseGraph n}
{base level numcells : Nat}
{root : RefineSt n}
{st : State n}
(h : Aligned G base root level level numcells st)
(first : Bool)
:
Aligned G base root level level numcells (cheapCheck first level st)
The actual native recovery caps first agreement at the receiving level.
theorem
Hex.GraphIso.Nauty.Sparse.Aligned.child
{n k : Nat}
{G : Sparse.Colored n k}
{base level numcells : Nat}
{root : RefineSt n}
{st : State n}
(h : Aligned G.graph base root level level numcells st)
(first : Bool)
(hr : RefineSt.Ready G.graph base root)
(hok : Ready G level numcells st)
{tc tv : Nat}
{cell : VSet n}
(ht : Generic.Target State.frame level tc cell st)
(hv : cell.mem tv = true)
(hrecord : st.eqlevFirst = level → st.firsttc[level]! = Int.ofNat tc)
:
Individualization and the real cached visit prepare the next pending history from a recorded target and the parent's equitable witness.
theorem
Hex.GraphIso.Nauty.Sparse.Aligned.recover
{n k : Nat}
{G : Sparse.Colored n k}
{base level numcells : Nat}
{root : RefineSt n}
{st out : State n}
(h : Aligned G.graph base root level level numcells st)
(hok : SearchOk G.toDense level numcells st.frame)
(hout : FrameOut G level level st out)
(ht : out.firsttc = st.firsttc)
(hdiv : st.eqlevFirst < level → out.eqlevFirst < level)
:
Aligned G.graph base root level level numcells (Generic.Policy.recover (n + 2) level out)
A return that cannot repair an earlier divergence preserves the ancestor's frozen descent through actual partition and cache recovery.
theorem
Hex.GraphIso.Nauty.Sparse.Aligned.child_return
{n k : Nat}
{G : Sparse.Colored n k}
{base level numcells : Nat}
{root : RefineSt n}
{st : State n}
(h : Aligned G.graph base root level level numcells st)
(first : Bool)
(tcLevel fuel : Nat)
(hl : 1 ≤ level)
(hok : Ready G level numcells st)
{tc tv : Nat}
{cell : VSet n}
(ht : Generic.Target State.frame level tc cell st)
(hv : cell.mem tv = true)
:
have out :=
(Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1)
(Generic.Policy.child first level tc tv st)).snd;
Aligned G.graph base root level level numcells (Generic.Policy.recover (n + 2) level (Generic.Policy.leaveChild tv out))
Every actual off-path child call has the frame and divergence effects needed to recover its parent's alignment, for arbitrary recursion fuel.