def Hex.GraphIso.Nauty.Sparse.Generation.ChildPath {n : Nat} (G : SparseGraph n) (tcLevel boundary level : Nat) (st : RefineSt n) (tc : Nat) (targets : List Nat) (key : Key n) (o : Nat) : Prop

A reference occurrence in a frozen native child. Fresh scratch fixes the witness state; ChildPath.reorder transfers it to the exact cached child used by a recovered search frame.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Generation.ChildPath.reorder {n : Nat} {G : SparseGraph n} {tcLevel boundary level tc len a b : Nat} {s t : RefineSt n} {targets : List Nat} {key : Key n} {scratch : Scratch} (hs : RefineSt.Ready G level s) (ht : RefineSt.Ready G level t) (hp : t.ptn = s.ptn) (he : cellsPerm s.ptn level t.lab s.lab) (hc : IsCell s.ptn level tc len) (hb : tc + len ≤ n) (hn : 1 < len) (ha : a < len) (hb' : b < len) (hsc : Scratch.Bounded n scratch) (hmove : t.lab[tc + b]! = s.lab[tc + a]!) : ChildPath G tcLevel boundary level s tc targets key a ↔ RefPath G tcLevel boundary (level + 1) (RefineSt.child (Graph.ofGraph G) level t tc t.lab[tc + b]! scratch) targets key

Cell reordering and independent bounded scratch preserve the entire reference occurrence, including its saved uniformity boundary.

theorem Hex.GraphIso.Nauty.Sparse.Generation.ChildPath.cached {n : Nat} {G : SparseGraph n} {tcLevel boundary level tc len o : Nat} {st : RefineSt n} {targets : List Nat} {key : Key n} {scratch : Scratch} (hr : RefineSt.Ready G level st) (hc : IsCell st.ptn level tc len) (hb : tc + len ≤ n) (hn : 1 < len) (ho : o < len) (hs : Scratch.Bounded n scratch) : ChildPath G tcLevel boundary level st tc targets key o ↔ RefPath G tcLevel boundary (level + 1) (RefineSt.child (Graph.ofGraph G) level st tc st.lab[tc + o]! scratch) targets key

The frozen occurrence is equivalent to the same chosen child with the actual bounded scratch supplied by the executable.

theorem Hex.GraphIso.Nauty.Sparse.Generation.ChildPath.carried {n : Nat} {G : SparseGraph n} {tcLevel boundary level tc len a b : Nat} {st : RefineSt n} {targets : List Nat} {key : Key n} {gamma : Array Nat} (hr : RefineSt.Ready G level st) (hc : IsCell st.ptn level tc len) (hb : tc + len ≤ n) (hn : 1 < len) (ha : a < len) (hb' : b < len) (hcheck : checkAutom (Graph.context G).g gamma = true) (hstab : CellStab st.ptn level st.lab gamma) (hmove : gamma[st.lab[tc + a]!]! = st.lab[tc + b]!) : ChildPath G tcLevel boundary level st tc targets key a ↔ ChildPath G tcLevel boundary level st tc targets key b

Every checked stabilizer carries frozen child occurrences in both directions, without a generation-completeness hypothesis.