theorem Hex.GraphIso.Nauty.Selects.reference {n : Nat} {ctx : Ctx n} {tcLevel level : Nat} {root : RefineSt n} {path : List (Nat × Nat)} (h : Selects ctx tcLevel level root path) : Generation.referenceTargets ctx tcLevel level root path

The selected descent uses the same target rule as a reference occurrence.

theorem Hex.GraphIso.Nauty.pathCodes_reference {n : Nat} (ctx : Ctx n) (level : Nat) (root : RefineSt n) (path : List (Nat × Nat)) : pathCodes ctx level root path = Generation.referenceCodes ctx level root path

The two path-code definitions enumerate the same refined nodes.

theorem Hex.GraphIso.Nauty.FirstRef.occurs {n : Nat} {ctx : Ctx n} {tcLevel level : Nat} {root : RefineSt n} {st : Search n} (h : FirstRef ctx tcLevel level root st) : ∃ (targets : List Nat), ∃ (key : Key n), Generation.HasLeaf ctx tcLevel level root targets key ∧ Generation.Matches ctx level st targets key

A saved first descent supplies occurrence and exact stored matching, including the terminal sentinel. Neither conclusion assumes key maximality.

theorem Hex.GraphIso.Nauty.FirstPre.occurs {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel fuel level numcells : Nat} {st : Search n} (h : FirstPre G ctx level numcells st) (hn0 : 0 < n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hempty : st.genTrace = #[]) (hfuel : n + 1 ≤ level + fuel) : ∃ (targets : List Nat), ∃ (key : Key n), Generation.HasLeaf ctx tcLevel level (SearchState.refined ctx level numcells st) targets key ∧ Generation.Matches ctx level (node true ctx inf tcLevel fuel level numcells st).snd targets key

A valid first call produces a matching occurrence from its actual descent, without assuming the call's maximum or its return level.