theorem Hex.GraphIso.Nauty.initActive_card (n : Nat) (ends : List Nat) : (initActive n ends).card ≤ ends.length

Initial activation inserts at most one vertex for each listed cell.

theorem Hex.GraphIso.Nauty.Sparse.initial_saturated {n : Nat} (g : Graph n) (lab : Array Nat) (ends : List Nat) : have s := initial g lab ends; have t := refineWith g 1 s.lab s.ptn s.active ends.length s.canong.scratch; t.queue.isEmpty = true ∨ n ≤ t.numcells

The actual root initializer supplies the premise of refinement's existing loop bound, for every endpoint list including the empty graph.

theorem Hex.GraphIso.Nauty.Sparse.initial_nodeOk {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; NodeOk n 1 p.fst (initPtn n (n + 2) p.snd) (initActive n p.snd)

Stable sparse colour buckets satisfy the shared, adjacency-independent partition-state contract.

theorem Hex.GraphIso.Nauty.Sparse.initial_cells_active {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; ∀ (c : Nat × Nat), c ∈ cells (initPtn n (n + 2) p.snd) 1 n → (initActive n p.snd).mem c.fst = true

Every initial sparse colour cell is active. The conversion here is only the proved ordered-partition bridge; the executable uses sparse adjacency.

theorem Hex.GraphIso.Nauty.Sparse.initial_count {n k : Nat} (G : Sparse.Colored n k) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; bcount (initPtn n (n + 2) p.snd) 1 n = p.snd.length

The cell count passed to root refinement is its actual boundary count.