@[reducible, inline]
Canonical-reference provenance for the native state. Only partition, label and ancestor fields enter this shared proof predicate.
Equations
- Hex.GraphIso.Nauty.Sparse.CanonOut level st out = Hex.GraphIso.Nauty.CanonOut level st.frame out.frame
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.CanonOut.trans
{n level : Nat}
{st mid out : State n}
{k : Nat}
{G : Sparse.Colored n k}
(h : CanonOut level st mid)
(hnext : CanonOut level mid out)
(hf : FrameOut G level level st mid)
:
CanonOut level st out
theorem
Hex.GraphIso.Nauty.Sparse.CanonOut.visit
{n level : Nat}
{st out : State n}
{k : Nat}
{G : Sparse.Colored n k}
{numcells : Nat}
(hi : NodeInv G level numcells st)
(h : CanonOut level (Sparse.visit (Graph.ofGraph G.graph) level numcells st).snd.snd out)
:
CanonOut level st out
Actual cached refinement transports the reference to its entry cells. The proof uses native label permutations and literal preserved boundaries.
theorem
Hex.GraphIso.Nauty.Sparse.CanonOut.child
{n level : Nat}
{st out : State n}
{k : Nat}
{G : Sparse.Colored n k}
{numcells tc tv : Nat}
{cell : VSet n}
(first : Bool)
(hn : 0 < n)
(hl : 1 ≤ level)
(hi : Ready G level numcells st)
(ht : Generic.Target State.frame level tc cell st)
(hv : cell.mem tv = true)
(h : CanonOut (level + 1) (Generic.Policy.child first level tc tv st) out)
:
CanonOut level st out
Native individualization uses the shared breakout literally; its newly stored reference therefore lies in the parent's ordered cells.
theorem
Hex.GraphIso.Nauty.Sparse.CanonOut.recover
{n level : Nat}
{st out : State n}
(h : CanonOut level st out)
(inf : Nat)
:
CanonOut level st (Generic.Policy.recover inf level out)
The actual parent recovery clamps the ancestor while retaining its label.
theorem
Hex.GraphIso.Nauty.Sparse.CanonOut.afterSweep
{n level : Nat}
{st out : State n}
(h : CanonOut level st out)
(first : Bool)
(size index : Nat)
:
CanonOut level st (Generic.Policy.afterSweep first level size index out)