inductive
Hex.GraphIso.Nauty.Sparse.Generation.RefPath
{n : Nat}
(G : SparseGraph n)
(tcLevel boundary : Nat)
:
A native selected reference descent retaining uniformity at and below the saved all-same boundary. Every step is the literal cached child operation, with its own bounded scratch and complete refinement code.
- leaf {n : Nat} {G : SparseGraph n} {tcLevel boundary level : Nat} {st : RefineSt n} (label : Label n) (discrete : discreteAt st.ptn level n = true) (parse : Label.ofArray? n st.lab = some label) : RefPath G tcLevel boundary level st [] { codes := [st.longcode, codeSentinel], graph := G.relabel label.perm }
- step {n : Nat} {G : SparseGraph n} {tcLevel boundary level tc len o : Nat} {st : RefineSt n} {scratch : Scratch} {targets : List Nat} {key : Key n} (cell : IsCell st.ptn level tc len) (range : tc + len ≤ n) (nontrivial : 1 < len) (offset : o < len) (bounded : Scratch.Bounded n scratch) (target : tc = targetcell (Graph.ofGraph G) st.lab st.ptn level tcLevel (-1)) (child : RefPath G tcLevel boundary (level + 1) (RefineSt.child (Graph.ofGraph G) level st tc st.lab[tc + o]! scratch) targets key) (uniform : boundary ≤ level → Uniform G tcLevel level st (tc :: targets) { codes := st.longcode :: key.codes, graph := key.graph }) : RefPath G tcLevel boundary level st (tc :: targets) { codes := st.longcode :: key.codes, graph := key.graph }
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.Generation.RefPath.occurs
{n : Nat}
{G : SparseGraph n}
{tcLevel boundary level : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
(h : RefPath G tcLevel boundary level st targets key)
:
HasLeaf G tcLevel level st targets key
Forgetting boundary uniformity retains the literal selected descent.
theorem
Hex.GraphIso.Nauty.Sparse.Generation.RefPath.uniform
{n : Nat}
{G : SparseGraph n}
{tcLevel boundary level : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
(h : RefPath G tcLevel boundary level st targets key)
(hr : RefineSt.Ready G level st)
(hb : boundary ≤ level)
:
Uniform G tcLevel level st targets key
theorem
Hex.GraphIso.Nauty.Sparse.Generation.RefPath.raise
{n : Nat}
{G : SparseGraph n}
{tcLevel boundary level : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{boundary' : Nat}
(h : RefPath G tcLevel boundary level st targets key)
(hb : boundary ≤ boundary')
:
RefPath G tcLevel boundary' level st targets key
Moving the boundary deeper retains all required uniform subtrees.
theorem
Hex.GraphIso.Nauty.Sparse.Generation.HasLeaf.uniformPath
{n : Nat}
{G : SparseGraph n}
{tcLevel boundary level : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
(h : HasLeaf G tcLevel level st targets key)
(hr : RefineSt.Ready G level st)
(hu : Uniform G tcLevel level st targets key)
:
RefPath G tcLevel boundary level st targets key
Every occurrence inside a uniform native subtree retains uniformity along its whole actual path, at any chosen later boundary.
theorem
Hex.GraphIso.Nauty.Sparse.Generation.RefPath.map
{n : Nat}
(G H : SparseGraph n)
(p : Perm n)
(hiso : ∀ (i j : Fin n), H.adj (p.get i) (p.get j) = G.adj i j)
{tcLevel boundary level : Nat}
{s t : RefineSt n}
{targets : List Nat}
{key : Key n}
(hs : RefineSt.Ready G level s)
(ht : RefineSt.Ready H level t)
(he : RefineSt.Equiv (renamingOf p) level s t)
(h : RefPath G tcLevel boundary level s targets key)
:
RefPath H tcLevel boundary level t targets key
Isomorphism transports the reference occurrence and every uniform subtree retained at its boundary, preserving the full native key.
theorem
Hex.GraphIso.Nauty.Sparse.Generation.RefPath.map_iff
{n : Nat}
(G H : SparseGraph n)
(p : Perm n)
(hiso : ∀ (i j : Fin n), H.adj (p.get i) (p.get j) = G.adj i j)
{tcLevel boundary level : Nat}
{s t : RefineSt n}
{targets : List Nat}
{key : Key n}
(hs : RefineSt.Ready G level s)
(ht : RefineSt.Ready H level t)
(he : RefineSt.Equiv (renamingOf p) level s t)
:
Isomorphic native refined states have the same richer reference occurrences, retaining all uniformity obligations in both directions.
theorem
Hex.GraphIso.Nauty.Sparse.Generation.RefPath.carried_iff
{n : Nat}
{G : SparseGraph n}
{tcLevel boundary level tc len a b : Nat}
{st : RefineSt n}
{scratch other : Scratch}
{gamma : Array Nat}
{targets : List Nat}
{key : Key n}
(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)
(hs : Scratch.Bounded n scratch)
(ht : Scratch.Bounded n other)
(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]!)
:
RefPath G tcLevel boundary (level + 1) (RefineSt.child (Graph.ofGraph G) level st tc st.lab[tc + a]! scratch) targets
key ↔ RefPath G tcLevel boundary (level + 1) (RefineSt.child (Graph.ofGraph G) level st tc st.lab[tc + b]! other) targets
key
An arbitrary checked cell stabilizer carries the richer reference between literal cached children before any generation theorem is known.
theorem
Hex.GraphIso.Nauty.Sparse.Generation.RefPath.carried
{n : Nat}
{G : SparseGraph n}
{tcLevel boundary level tc len a b : Nat}
{st : RefineSt n}
{scratch other : Scratch}
{gamma : Array Nat}
{targets : List Nat}
{key : Key n}
(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)
(hs : Scratch.Bounded n scratch)
(ht : Scratch.Bounded n other)
(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]!)
(h :
RefPath G tcLevel boundary (level + 1) (RefineSt.child (Graph.ofGraph G) level st tc st.lab[tc + a]! scratch) targets
key)
:
RefPath G tcLevel boundary (level + 1) (RefineSt.child (Graph.ofGraph G) level st tc st.lab[tc + b]! other) targets key
Forward transport through a checked cell stabilizer retains the native reference and its saved uniformity boundary.