theorem Hex.GraphIso.Nauty.FirstCodeInv.sentinel_bound {n slot elev : Nat} {cs fs : List Nat} {store : Array Nat} (h : FirstCodeInv n cs fs store elev) (hslot : 1 ≤ slot) (hsent : store[slot]! = codeSentinel) : fs.length < slot

A sentinel cannot occur inside the real codes of the first path.

structure Hex.GraphIso.Nauty.FirstRef {n : Nat} (ctx : Ctx n) (tcLevel base : Nat) (root : RefineSt n) (st : Search n) : Type

A frozen ancestor's selected descent to the saved first leaf. The sentinel connects its actual depth to the first-code comparison.

• last : Nat
• leaf : RefineSt n
• path : List (Nat × Nat)
• descent : DescPath ctx base root self.path self.last self.leaf
• selects : Selects ctx tcLevel base root self.path
• targets : Targets st.firsttc base (List.map Prod.fst self.path)
• lab : self.leaf.lab = st.firstlab
• discrete (i : Nat) : i < n → self.leaf.ptn[i]! ≤ self.last
• sentinel : st.firstcode[self.last + 1]! = codeSentinel
• codes : StoredCodes st.firstcode base (pathCodes ctx base root self.path)

def Hex.GraphIso.Nauty.FirstRef.congr {n : Nat} {ctx : Ctx n} {tcLevel base : Nat} {root : RefineSt n} {st out : Search n} (h : FirstRef ctx tcLevel base root st) (heq : SearchState.reference out = SearchState.reference st) : FirstRef ctx tcLevel base root out

Updating other state fields leaves a saved reference history valid.

Equations

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

def Hex.GraphIso.Nauty.FirstRef.node {n : Nat} {ctx : Ctx n} {inf tcLevel fuel base level numcells : Nat} {root : RefineSt n} {st : Search n} (h : FirstRef ctx tcLevel base root st) : FirstRef ctx tcLevel base root (Nauty.node false ctx inf tcLevel fuel level numcells st).snd

An off-path call preserves every frozen first-reference history.

Equations

• h.node = h.congr ⋯

def Hex.GraphIso.Nauty.FirstRef.sweep {n : Nat} {ctx : Ctx n} {first : Bool} {inf tcLevel fuel cfuel base level numcells tc tv1 index : Nat} {cursor : Option Nat} {cell : VSet n} {root : RefineSt n} {st : Search n} (h : FirstRef ctx tcLevel base root st) (hpast : Generic.Past first tv1 cursor) : FirstRef ctx tcLevel base root (Nauty.sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd

A later sibling sweep preserves every frozen first-reference history.

Equations

• h.sweep hpast = h.congr ⋯

theorem Hex.GraphIso.Nauty.firstRef_of_path {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel fuel level numcells last : Nat} {st leaf : Search n} (hn0 : 0 < n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hpath : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (heq : Equitable ctx level (SearchState.refined ctx level numcells st).lab (SearchState.refined ctx level numcells st).ptn) (htsize : n < st.firsttc.size) (hcsize : st.firstcode.size = n + 2) : ∃ (href : FirstRef ctx tcLevel level (SearchState.refined ctx level numcells st) (node true ctx inf tcLevel fuel level numcells st).snd), href.last = last

A completed first-path call supplies a reference history at its own frame.

theorem Hex.GraphIso.Nauty.FirstRef.depth {n : Nat} {ctx : Ctx n} {tcLevel base : Nat} {root : RefineSt n} {st : Search n} (h : FirstRef ctx tcLevel base root st) {cs fs : List Nat} (hc : FirstCodeInv n cs fs st.firstcode st.eqlevFirst) : st.eqlevFirst ≤ h.last

First-code agreement cannot extend below the saved first leaf.

theorem Hex.GraphIso.Nauty.FirstRef.code_eq {n : Nat} {ctx : Ctx n} {tcLevel base i : Nat} {root : RefineSt n} {st : Search n} (h : FirstRef ctx tcLevel base root st) {cs fs : List Nat} (hc : FirstCodeInv n cs fs st.firstcode st.eqlevFirst) (hbase : 1 ≤ base) (hi : i < (pathCodes ctx base root h.path).length) (hf : base + i ≤ fs.length) : (pathCodes ctx base root h.path)[i]! = fs[base + i - 1]!

The comparison's semantic first codes agree with the saved descent at every real slot represented by both histories.

theorem Hex.GraphIso.Nauty.FirstRef.target {n : Nat} {ctx : Ctx n} {tcLevel base level : Nat} {root current : RefineSt n} {st : Search n} (h : FirstRef ctx tcLevel base root st) (hdepth : level ≤ h.last) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hsmall : SubtreeOk ctx base root) (hcurrent : FollowsPerm ctx st.firsttc base root level current) (hopen : ∃ (i : Nat), i < n ∧ level < current.ptn[i]!) : Int.ofNat (specTargetcell ctx current.lab current.ptn level tcLevel) = st.firsttc[level]!

A surviving first-code comparison follows the saved target at a cheap ancestor.

theorem Hex.GraphIso.Nauty.FirstRef.leaf_eq {n : Nat} {ctx : Ctx n} {tcLevel base level : Nat} {root current : RefineSt n} {st : Search n} (h : FirstRef ctx tcLevel base root st) (hdepth : level ≤ h.last) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hsmall : SubtreeOk ctx base root) (hcurrent : FollowsPerm ctx st.firsttc base root level current) (hdisc : ∀ (i : Nat), i < n → current.ptn[i]! ≤ level) : level = h.last ∧ leafRows ctx current.lab = leafRows ctx st.firstlab

A discrete current descent below a cheap ancestor reaches the saved first depth and has the saved first leaf's rows.

theorem Hex.GraphIso.Nauty.FirstRef.scatter {n : Nat} {ctx : Ctx n} {tcLevel level : Nat} {root current : RefineSt n} {st : Search n} (h : FirstRef ctx tcLevel st.gcaFirst root st) (hdepth : level ≤ h.last) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hsmall : SubtreeOk ctx st.gcaFirst root) (hcurrent : FollowsPerm ctx st.firsttc st.gcaFirst root level current) (hdisc : ∀ (i : Nat), i < n → current.ptn[i]! ≤ level) (hlab : st.lab = current.lab) (hwork : st.workperm.size = n) : checkAutom ctx.g (Nauty.scatter st.firstlab st).workperm = true

The reference history and current descent justify the executable cheap scatter.