theorem Hex.GraphIso.Nauty.Sparse.Comparison.covers {n : Nat} {G : SparseGraph n} {cs bs fs : List Nat} {st : State n} (h : Comparison G cs bs fs st) (hneg : st.compCanon < 0) (tail : Key n) : Covers (prefixKey cs tail) (State.key G bs st)

A settled negative code comparison covers every continuation with that prefix, independently of all subsequent refinement and sparse rows.

theorem Hex.GraphIso.Nauty.Sparse.NodeInv.code_cover {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel level numcells : Nat} {cs bs fs : List Nat} {st compared : State n} (h : NodeInv G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (hf : n < fuel + 1 + numcells) (hc : Comparison G.graph (cs ++ [(visit (Graph.ofGraph G.graph) level numcells st).snd.fst]) bs fs compared) (hneg : compared.compCanon < 0) : Covers (prefixKey cs (subtreeKey G.graph tcLevel (fuel + 1) level st.lab st.ptn st.active numcells)) (State.key G.graph bs compared)

A negative comparison after the actual cached visit covers the full unpruned node, including all descendants and their terminal row keys.

theorem Hex.GraphIso.Nauty.Sparse.NodeInv.prepare_cover {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel numcells : Nat} {cs bs fs : List Nat} {st : State n} (h : NodeInv G (cs.length + 1) numcells st) (hn : 0 < n) (hf : n < fuel + 1 + numcells) (hc : Comparison G.graph cs bs fs st) : have p := prepareOther (Graph.ofGraph G.graph) tcLevel (cs.length + 1) numcells st; p.snd.snd.snd.snd.snd.compCanon < 0 → Covers (prefixKey cs (subtreeKey G.graph tcLevel (fuel + 1) (cs.length + 1) st.lab st.ptn st.active numcells)) (State.key G.graph bs p.snd.snd.snd.snd.snd)

Native off-path preparation supplies the negative-prefix coverage premise from the incoming comparison machines and its literal code write.