def
Hex.GraphIso.Nauty.Sparse.Generation.Uniform
{n : Nat}
(G : SparseGraph n)
(tcLevel level : Nat)
(st : RefineSt n)
(targets : List Nat)
(key : Key n)
:
Every selected native descent has the same target sequence and full leaf key, allowing arbitrary bounded scratch at every literal child call.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.Generation.Uniform.leaf
{n : Nat}
{G : SparseGraph n}
{tcLevel level : Nat}
{st : RefineSt n}
{label : Label n}
(hr : RefineSt.Ready G level st)
(hd : discreteAt st.ptn level n = true)
(hp : Label.ofArray? n st.lab = some label)
:
theorem
Hex.GraphIso.Nauty.Sparse.Generation.Uniform.node
{n : Nat}
{G : SparseGraph n}
{tcLevel level : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{tc len : Nat}
(hr : RefineSt.Ready G level st)
(hc : IsCell st.ptn level tc len)
(hb : tc + len ≤ n)
(hn : 1 < len)
(ht : tc = targetcell (Graph.ofGraph G) st.lab st.ptn level tcLevel (-1))
(hchildren :
∀ (o : Nat),
o < len →
∀ (scratch : Scratch),
Scratch.Bounded n scratch →
Uniform G tcLevel (level + 1) (RefineSt.child (Graph.ofGraph G) level st tc st.lab[tc + o]! scratch) targets
key)
:
Uniformity of every literal target child gives parent uniformity. The target and code are those of the executed sparse refinement.
theorem
Hex.GraphIso.Nauty.Sparse.Generation.Uniform.child
{n : Nat}
{G : SparseGraph n}
{tcLevel level : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{tc len o : Nat}
{scratch : Scratch}
(h : Uniform G tcLevel level st (tc :: targets) { codes := st.longcode :: key.codes, graph := key.graph })
(hc : IsCell st.ptn level tc len)
(hb : tc + len ≤ n)
(hn : 1 < len)
(ho : o < len)
(hs : Scratch.Bounded n scratch)
(ht : tc = targetcell (Graph.ofGraph G) st.lab st.ptn level tcLevel (-1))
:
Uniform G tcLevel (level + 1) (RefineSt.child (Graph.ofGraph G) level st tc st.lab[tc + o]! scratch) targets key
Every literal target child inherits a uniform parent's suffix.
theorem
Hex.GraphIso.Nauty.Sparse.Generation.Uniform.carriers
{n : Nat}
{G : SparseGraph n}
{tcLevel level : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{tc len guide : Nat}
{scratch : Scratch}
(hr : RefineSt.Ready G level st)
(hc : IsCell st.ptn level tc len)
(hb : tc + len ≤ n)
(hn : 1 < len)
(hg : guide < len)
(hs : Scratch.Bounded n scratch)
(ht : tc = targetcell (Graph.ofGraph G) st.lab st.ptn level tcLevel (-1))
(hcarriers :
∀ (o : Nat),
o < len →
∃ (gamma : Array Nat), checkAutom (Graph.context G).g gamma = true ∧ CellStab st.ptn level st.lab gamma ∧ gamma[st.lab[tc + o]!]! = st.lab[tc + guide]!)
(hguide :
Uniform G tcLevel (level + 1) (RefineSt.child (Graph.ofGraph G) level st tc st.lab[tc + guide]! scratch) targets key)
:
Counted checked carriers transport every child's leaves to the guiding child. They need not belong to a group already proved complete.
theorem
Hex.GraphIso.Nauty.Sparse.Generation.Uniform.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 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 : Uniform G tcLevel level s targets key)
:
Uniform H tcLevel level t targets key
Native state equivalence transports uniformity because its inverse preserves every individual leaf key and selected target sequence.