theorem Hex.GraphIso.Nauty.Sparse.canonPolicy {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) (tcLevel : Nat) : Generic.SoundPolicy (Graph.ofGraph G.graph) (n + 2) tcLevel (canonContract G)

Canonical-reference provenance follows the actual sparse mutual recursion with the proved frame, equitability and scratch contracts.

theorem Hex.GraphIso.Nauty.Sparse.node_canon {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) (first : Bool) (tcLevel fuel level numcells : Nat) (st : State n) (hl : 1 ≤ level) (h : NodeInv G level numcells st) : CanonOut level st (Generic.node first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel level numcells st).snd

Every native node couples its stored canonical label to the actual ancestor counter, including truncated calls and returns past the caller.

theorem Hex.GraphIso.Nauty.Sparse.sweep_canon {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) (first : Bool) (tcLevel fuel cfuel level numcells tc tv1 index : Nat) (cursor : Option Nat) (cell : VSet n) (st : State n) (hl : 1 ≤ level) (h : Ready G level numcells st) (ht : Generic.Target State.frame level tc cell st) (hv : ∀ (v : Nat), cursor = some v → cell.mem v = true) : CanonOut level st (Generic.sweep first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd

Every native sibling sweep retains or installs its canonical label within the current cells and maintains the corresponding ancestor bounds.