theorem
Hex.GraphIso.Nauty.Sparse.Max.Cell.Cover.earlier
{n : Nat}
{G : SparseGraph n}
{tcLevel : Nat}
{c : Cell n}
{cell : VSet n}
{tv v : Nat}
{best : Option (Key n)}
(h : Cover G tcLevel c (Remaining (some tv) cell) best)
(hv : c.vertices.mem v = true)
(hlt : v < tv)
:
Every original child below the current cursor is covered. A removed child's ranked carrier cannot still be live below that cursor.
def
Hex.GraphIso.Nauty.Sparse.Max.Parent.Ranked
{n : Nat}
(G : SparseGraph n)
(tcLevel : Nat)
(p : Parent n)
:
A suspended cursor has already covered every smaller vertex of its original target cell, including vertices removed by earlier filters.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.Max.Parent.Valid.ranked
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{p : Parent n}
(h : Valid G tcLevel p)
(hc :
Cell.Cover G.graph tcLevel (Frame.target G.graph tcLevel p.node) (Remaining (some p.chosen) p.cell)
(State.key G.graph p.bs p.state))
:
The native frozen-cell coverage invariant supplies the suspended cursor's rank rule. A hinted target uses its already dominating code prefix; an unhinted target transports the actual recovered cell order.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Parent.Ranked.orbit_cover
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{p : Parent n}
{out : State n}
{best : Option (Key n)}
(h : Ranked G.graph tcLevel p)
(hp : Valid G tcLevel p)
(ho : OrbitTrace G out)
(ht : TraceOk G out)
(hs : ∀ (gamma : Array Nat), gamma ∈ out.genTrace → CellStab p.state.ptn p.node.level p.state.lab gamma)
(hlt : out.orbits[p.chosen]! < p.chosen)
(hg : Grows (State.key G.graph p.bs p.state) best)
:
A smaller orbit pointer covers the interrupted child of a suspended cursor. The word in the executed generator trace stays in its frozen target cell and transports the full native subtree key.