structure
Hex.GraphIso.Nauty.Sparse.Comparison
{n : Nat}
(G : SparseGraph n)
(cs bs fs : List Nat)
(st : State n)
:
Both production code comparisons and the saved first leaf's lower bound on the native incumbent. The labels are parsed from actual storage.
- canonical : Codes cs bs st
- first : FirstCodeInv n cs fs st.firstcode st.eqlevFirst
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.Comparison.congr
{n : Nat}
{G : SparseGraph n}
{cs bs fs : List Nat}
{st : State n}
(h : Comparison G cs bs fs st)
{out : State n}
(hcc : out.canoncode = st.canoncode)
(hcl : out.canonlevel = st.canonlevel)
(hce : out.eqlevCanon = st.eqlevCanon)
(hcmp : out.compCanon = st.compCanon)
(hfc : out.firstcode = st.firstcode)
(hfe : out.eqlevFirst = st.eqlevFirst)
(hfl : out.firstlab = st.firstlab)
(hcan : out.canonlab = st.canonlab)
:
Comparison G cs bs fs out
Updates outside the two comparisons and saved labels preserve meaning.
theorem
Hex.GraphIso.Nauty.Sparse.Comparison.visit
{n : Nat}
{G : SparseGraph n}
{cs bs fs : List Nat}
{st : State n}
(h : Comparison G cs bs fs st)
(level numcells : Nat)
:
Comparison G cs bs fs (Sparse.visit (Graph.ofGraph G) level numcells st).snd.snd
theorem
Hex.GraphIso.Nauty.Sparse.Comparison.compare
{n : Nat}
{G : SparseGraph n}
{cs bs fs : List Nat}
{st : State n}
(h : Comparison G cs bs fs st)
{code : Nat}
(hc : code < codeSentinel)
(hlen : cs.length ≤ n)
:
Comparison G (cs ++ [code]) bs fs (compareCodes (cs.length + 1) code st)
The executed next code advances both path comparisons.
theorem
Hex.GraphIso.Nauty.Sparse.Comparison.target
{n : Nat}
{G : SparseGraph n}
{cs bs fs : List Nat}
{st : State n}
(h : Comparison G cs bs fs st)
(tcLevel numcells : Nat)
:
Comparison G cs bs fs (chooseTarget false (Graph.ofGraph G) tcLevel cs.length numcells st).snd.snd.snd
Native target selection retains the incumbent and may lower only agreement with the first path when a stored hint disagrees.
theorem
Hex.GraphIso.Nauty.Sparse.Comparison.child
{n : Nat}
{G : SparseGraph n}
{cs bs fs : List Nat}
{st : State n}
(h : Comparison G cs bs fs st)
(first : Bool)
(level tc tv : Nat)
:
Comparison G cs bs fs (Generic.Policy.child first level tc tv st)
theorem
Hex.GraphIso.Nauty.Sparse.Comparison.cheap
{n : Nat}
{G : SparseGraph n}
{cs bs fs : List Nat}
{st : State n}
(h : Comparison G cs bs fs st)
(first : Bool)
(level : Nat)
:
Comparison G cs bs fs (cheapCheck first level st)
theorem
Hex.GraphIso.Nauty.Sparse.Comparison.firstterminal
{n : Nat}
{G : SparseGraph n}
{cs : List Nat}
{st : State n}
{l : Label n}
(hc : Codes cs cs (Nauty.firstterminal cs.length st))
(hf : FirstCodeInv n cs cs (Nauty.firstterminal cs.length st).firstcode (Nauty.firstterminal cs.length st).eqlevFirst)
(hne : cs ≠ [])
(hl : Label.ofArray? n st.lab = some l)
:
Comparison G cs cs cs (Nauty.firstterminal cs.length st)
Initialized code machines at the first leaf have a parsed incumbent equal to the first reference, so the required key lower bound is reflexive.
theorem
Hex.GraphIso.Nauty.Sparse.initial_comparison
{n k : Nat}
(G : Sparse.Colored n k)
(hn : 0 < n)
:
have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val;
∃ (last : Nat), ∃ (leaf : State n), ∃ (codes : List Nat), Generic.FirstPath (Graph.ofGraph G.graph) 100 (n + 2) 1 p.snd.length (initial (Graph.ofGraph G.graph) p.fst p.snd)
last leaf ∧ codes.length = last ∧ Comparison G.graph codes codes codes (firstterminal last leaf)
The initialized native search supplies both comparisons and the first key bound at its actual first leaf, with no leaf invariant premise.