inductive Hex.GraphIso.Nauty.Generation.RefPath {n : Nat} (ctx : Ctx n) (tcLevel boundary : Nat) : Nat → RefineSt n → List Nat → Key n → Prop

A reference occurrence retaining uniformity at and below a saved boundary. The target hints and complete leaf key remain part of the witness when pruning transports it to another child.

• leaf {n : Nat} {ctx : Ctx n} {tcLevel boundary level : Nat} {rs : RefineSt n} (discrete : ∀ (q : Nat), q < n → rs.ptn[q]! ≤ level) : RefPath ctx tcLevel boundary level rs [] { codes := [rs.longcode, codeSentinel], rows := leafRows ctx rs.lab }
• step {n : Nat} {ctx : Ctx n} {tcLevel boundary level tc e o : Nat} {rs : RefineSt n} {targets : List Nat} {key : Key n} (depth : level < n) (cell : (tc, e) ∈ cells rs.ptn level n) (nontrivial : tc < e) (offset : o ≤ e - tc) (target : tc = specTargetcell ctx rs.lab rs.ptn level tcLevel) (child : RefPath ctx tcLevel boundary (level + 1) (childSt ctx level rs tc rs.lab[tc + o]!) targets key) (uniform : boundary ≤ level → Uniform ctx tcLevel level rs (tc :: targets) { codes := rs.longcode :: key.codes, rows := key.rows }) : RefPath ctx tcLevel boundary level rs (tc :: targets) { codes := rs.longcode :: key.codes, rows := key.rows }

theorem Hex.GraphIso.Nauty.Generation.RefPath.occurs {n : Nat} {ctx : Ctx n} {tcLevel boundary level : Nat} {rs : RefineSt n} {targets : List Nat} {key : Key n} (h : RefPath ctx tcLevel boundary level rs targets key) : HasLeaf ctx tcLevel level rs targets key

Forgetting uniformity gives the ordinary reference occurrence.

theorem Hex.GraphIso.Nauty.Generation.RefPath.uniform {n : Nat} {ctx : Ctx n} {tcLevel boundary level : Nat} {rs : RefineSt n} {targets : List Nat} {key : Key n} (h : RefPath ctx tcLevel boundary level rs targets key) (hok : IterOk ctx level rs) (hb : boundary ≤ level) : Uniform ctx tcLevel level rs targets key

At the saved boundary, the richer occurrence supplies the uniform subtree premise needed by the emission theorem.

theorem Hex.GraphIso.Nauty.Generation.RefPath.raise {n : Nat} {ctx : Ctx n} {tcLevel boundary boundary' level : Nat} {rs : RefineSt n} {targets : List Nat} {key : Key n} (h : RefPath ctx tcLevel boundary level rs targets key) (hb : boundary ≤ boundary') : RefPath ctx tcLevel boundary' level rs targets key

Moving a saved boundary deeper weakens the uniformity obligation.

theorem Hex.GraphIso.Nauty.Generation.HasLeaf.uniformPath {n : Nat} {ctx : Ctx n} {tcLevel boundary level : Nat} {rs : RefineSt n} {targets : List Nat} {key : Key n} (h : HasLeaf ctx tcLevel level rs targets key) (hok : IterOk ctx level rs) (hu : Uniform ctx tcLevel level rs targets key) : RefPath ctx tcLevel boundary level rs targets key

In a uniform subtree, every reference occurrence carries uniformity at every later boundary along its path.

theorem Hex.GraphIso.Nauty.Generation.RefPath.transport {n : Nat} {ctx : Ctx n} {σ τ : Renaming n} {tcLevel boundary level : Nat} {U V : RefineSt n} {targets : List Nat} {key : Key n} (h : RefPath ctx tcLevel boundary level U targets key) (hg : RowsMap σ ctx.g ctx.g) (hback : RowsMap τ ctx.g ctx.g) (hinv : ∀ (v : Nat), v < n → τ.toFun (σ.toFun v) = v) (hU : IterOk ctx level U) (hsp : StPerm level V (mapSt σ U)) : RefPath ctx tcLevel boundary level V targets key

Graph and cell isomorphisms transport the reference and all its saved uniformity premises, including through unrecorded checked carriers.

theorem Hex.GraphIso.Nauty.Generation.RefPath.carried {n : Nat} {ctx : Ctx n} {tcLevel boundary level tc e oU oV : Nat} {st : RefineSt n} {γ : Array Nat} {targets : List Nat} {key : Key n} (hok : IterOk ctx level st) (hlvl : level < n) (hgsz : ctx.g.size = n) (hcheck : checkAutom ctx.g γ = true) (hstab : CellStab st.ptn level st.lab γ) (hcell : (tc, e) ∈ cells st.ptn level n) (hne : tc < e) (hoU : oU ≤ e - tc) (hoV : oV ≤ e - tc) (hmap : γ[st.lab[tc + oU]!]! = st.lab[tc + oV]!) (h : RefPath ctx tcLevel boundary (level + 1) (childSt ctx level st tc st.lab[tc + oU]!) targets key) : RefPath ctx tcLevel boundary (level + 1) (childSt ctx level st tc st.lab[tc + oV]!) targets key

A checked cell stabilizer moves a richer reference occurrence to another child without losing its saved uniformity boundary. Membership in the emitted generator group is not required.

theorem Hex.GraphIso.Nauty.Generation.RefPath.carried_iff {n : Nat} {ctx : Ctx n} {tcLevel boundary level tc e oU oV : Nat} {st : RefineSt n} {γ : Array Nat} {targets : List Nat} {key : Key n} (hok : IterOk ctx level st) (hlvl : level < n) (hgsz : ctx.g.size = n) (hcheck : checkAutom ctx.g γ = true) (hstab : CellStab st.ptn level st.lab γ) (hcell : (tc, e) ∈ cells st.ptn level n) (hne : tc < e) (hoU : oU ≤ e - tc) (hoV : oV ≤ e - tc) (hmap : γ[st.lab[tc + oU]!]! = st.lab[tc + oV]!) : RefPath ctx tcLevel boundary (level + 1) (childSt ctx level st tc st.lab[tc + oU]!) targets key ↔ RefPath ctx tcLevel boundary (level + 1) (childSt ctx level st tc st.lab[tc + oV]!) targets key

A checked automorphism identifies the sets of leaf keys below the two children it relates. The reverse carrier is a forward word in the same permutation, using finite permutation cycles.

theorem Hex.GraphIso.Nauty.Generation.RefPath.orbit {n k : Nat} {G : Colored n k} {base : List (Fin n)} {rs : RefineSt n} {st : SearchSt n} {tcLevel boundary level tc e oU oV : Nat} {u v : Fin n} {targets : List Nat} {key : Key n} (hok : IterOk { g := rowsOf G } level rs) (hlvl : level < n) (hpath : PathStab { g := rowsOf G } (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st) (hlab : st.lab = rs.lab) (hptn : st.ptn = rs.ptn) (hbase : ∀ (b : Fin n), st.fixedpts.mem ↑b = true → b ∈ base) (hcell : (tc, e) ∈ cells rs.ptn level n) (hne : tc < e) (hoU : oU ≤ e - tc) (hoV : oV ≤ e - tc) (hatU : rs.lab[tc + oU]! = ↑u) (hatV : rs.lab[tc + oV]! = ↑v) (horbit : Aut.Orbit G base u v) (h : RefPath { g := rowsOf G } tcLevel boundary (level + 1) (childSt { g := rowsOf G } level rs tc rs.lab[tc + oU]!) targets key) : RefPath { g := rowsOf G } tcLevel boundary (level + 1) (childSt { g := rowsOf G } level rs tc rs.lab[tc + oV]!) targets key

Every image of a reference child under the true path stabilizer contains the same reference occurrence. This supplies the matching-search premise before any generation theorem has been established.