theorem Hex.GraphIso.Nauty.Sparse.Comparison.ancestor_cover {n : Nat} {G : SparseGraph n} {cs bs fs : List Nat} {st : State n} (h : Comparison G cs bs fs st) (hneg : st.compCanon < 0) {length : Nat} (hdiv : st.eqlevCanon.toNat < length) (hlen : length ≤ cs.length) (tail : Key n) : Covers (prefixKey (List.take length cs) tail) (State.key G bs st)

A frozen negative code comparison covers every continuation of any ancestor prefix that already contains its first divergent code.

def Hex.GraphIso.Nauty.Sparse.Max.CodeScope {n k : Nat} (G : Sparse.Colored n k) (cs : List Nat) (frames : Frames n) : Prop

Each recorded ancestor code has its original valid native entry. This invariant stores syntax and geometry, not a maximum-correctness premise.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Sparse.Max.CodeScope.root {n k : Nat} (G : Sparse.Colored n k) : CodeScope G [] fun (x : Nat) => none

theorem Hex.GraphIso.Nauty.Sparse.Max.CodeScope.push {n k : Nat} {G : Sparse.Colored n k} {f : Frame n} {frames : Frames n} (h : CodeScope G f.codes frames) (hf : Frame.Valid G f) : CodeScope G (f.codes ++ [Frame.code G.graph f]) (frames.insert f)

Entering an actual child adds its parent's entry and exact cached visit code. Every earlier ancestor keeps the same recorded prefix.

theorem Hex.GraphIso.Nauty.Sparse.Max.CodeScope.take {n k : Nat} {G : Sparse.Colored n k} {cs : List Nat} {frames : Frames n} (h : CodeScope G cs frames) (length : Nat) : CodeScope G (List.take length cs) frames

Recovery to a shorter already-recorded path retains its ancestor entries.

theorem Hex.GraphIso.Nauty.Sparse.Max.CodeScope.witness {n k : Nat} {G : Sparse.Colored n k} {tcLevel target : Nat} {cs : List Nat} {frames : Frames n} {best : Option (Key n)} (h : CodeScope G cs frames) (ht : target < cs.length) (hc : ∀ (tail : Key n), Covers (prefixKey (List.take (target + 1) cs) tail) best) : Witness G tcLevel frames target best

A prefix rejection resolves the actual frozen frame at its named receiving level, including the root entry at target zero.

theorem Hex.GraphIso.Nauty.Sparse.Max.CodeScope.rejected {n k : Nat} {G : Sparse.Colored n k} {tcLevel target : Nat} {cs bs fs : List Nat} {frames : Frames n} {st : State n} (h : CodeScope G cs frames) (ht : target < cs.length) (hc : Comparison G.graph cs bs fs st) (hneg : st.compCanon < 0) (hdiv : st.eqlevCanon.toNat ≤ target) : Witness G tcLevel frames target (State.key G.graph bs st)

The executed comparison supplies its nonlocal code-return witness. Only the recorded prefix and the literal divergence level are required.