theorem
Hex.GraphIso.Nauty.Sparse.FirstRef.depth
{n : Nat}
{G : SparseGraph n}
{tcLevel base : Nat}
{root : RefineSt n}
{st : State n}
(h : FirstRef G tcLevel base root st)
{cs fs : List Nat}
(hc : FirstCodeInv n cs fs st.firstcode st.eqlevFirst)
:
Live code agreement cannot pass the saved native leaf's sentinel.
theorem
Hex.GraphIso.Nauty.Sparse.FirstRef.code_eq
{n : Nat}
{G : SparseGraph n}
{tcLevel base i : Nat}
{root : RefineSt n}
{st : State n}
(h : FirstRef G tcLevel base root st)
{cs fs : List Nat}
(hc : FirstCodeInv n cs fs st.firstcode st.eqlevFirst)
(hbase : 1 ≤ base)
(hi : i < h.codes.length)
(hf : base + i ≤ fs.length)
:
The code comparison and the saved actual descent read identical real codes at every position represented by both histories.
theorem
Hex.GraphIso.Nauty.Sparse.FirstRef.leaf_eq
{n : Nat}
{G : SparseGraph n}
{tcLevel base level : Nat}
{root current : RefineSt n}
{st : State n}
{xs : List (Nat × Nat)}
{f l : Label n}
(h : FirstRef G tcLevel base root st)
(hdepth : level ≤ h.last)
(hr : RefineSt.Ready G base root)
(hshape : NodeShape n base root.ptn)
(hp : DescPath G base root xs level current)
(ht : Targets st.firsttc base (List.map Prod.fst xs))
(hd : discreteAt current.ptn level n = true)
(hf : Label.ofArray? n st.firstlab = some f)
(hl : Label.ofArray? n current.lab = some l)
:
At a cheap ancestor, a discrete current descent following the saved targets has exactly the saved first leaf's depth and native graph.
theorem
Hex.GraphIso.Nauty.Sparse.FirstRef.scatter
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel level : Nat}
{root current : RefineSt n}
{st : State n}
{xs : List (Nat × Nat)}
{f l : Label n}
(h : FirstRef G.graph tcLevel st.gcaFirst root st)
(hdepth : level ≤ h.last)
(hr : RefineSt.Ready G.graph st.gcaFirst root)
(hshape : NodeShape n st.gcaFirst root.ptn)
(hp : DescPath G.graph st.gcaFirst root xs level current)
(ht : Targets st.firsttc st.gcaFirst (List.map Prod.fst xs))
(hd : discreteAt current.ptn level n = true)
(hcurrent : current.lab = st.lab)
(hw : st.workperm.size = n)
(hf : Label.ofArray? n st.firstlab = some f)
(hl : Label.ofArray? n st.lab = some l)
(hrf : CellsReach G.toDense st.firstlab)
(hrl : CellsReach G.toDense st.lab)
:
The saved and current native histories justify the literal first scatter as a coloured automorphism, without an adjacency scan.
theorem
Hex.GraphIso.Nauty.Sparse.classify_first_cheap
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel level numcells : Nat}
{root current : RefineSt n}
{st out : State n}
{xs : List (Nat × Nat)}
{cs fs : List Nat}
{f l : Label n}
(hauto : classify (Graph.ofGraph G.graph) level numcells st = (Generic.Leaf.autoFirst, out))
(h : FirstRef G.graph tcLevel st.gcaFirst root st)
(hc : FirstCodeInv n cs fs st.firstcode st.eqlevFirst)
(hr : RefineSt.Ready G.graph st.gcaFirst root)
(hshape : NodeShape n st.gcaFirst root.ptn)
(hp : DescPath G.graph st.gcaFirst root xs level current)
(ht : Targets st.firsttc st.gcaFirst (List.map Prod.fst xs))
(hd : discreteAt current.ptn level n = true)
(hcurrent : current.lab = st.lab)
(hw : st.workperm.size = n)
(hf : Label.ofArray? n st.firstlab = some f)
(hl : Label.ofArray? n st.lab = some l)
(hrf : CellsReach G.toDense st.firstlab)
(hrl : CellsReach G.toDense st.lab)
:
The actual first-reference classification is sound when the frozen cheap ancestor and current saved-target descent have been retained.