theorem
Hex.GraphIso.Nauty.Sparse.storePolicy
{n k : Nat}
(G : Sparse.Colored n k)
(hn : 0 < n)
(tcLevel : Nat)
:
Generic.SoundPolicy (Graph.ofGraph G.graph) (n + 2) tcLevel (storeContract G)
The complete production recursion preserves native canonical prefixes and its partition frames, independently of any maximality claim.
theorem
Hex.GraphIso.Nauty.Sparse.node_store
{n k : Nat}
(G : Sparse.Colored n k)
(hn : 0 < n)
(first : Bool)
(tcLevel fuel level numcells : Nat)
(st : State n)
(hl : 1 ≤ level)
(h : NodeInv G level numcells st)
(hs : Store G.graph st)
:
Store G.graph (Generic.node first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel level numcells st).snd
theorem
Hex.GraphIso.Nauty.Sparse.sweep_store
{n k : Nat}
(G : Sparse.Colored n k)
(hn : 0 < n)
(first : Bool)
(tcLevel fuel cfuel level numcells tc tv1 index : Nat)
(cursor : Option Nat)
(cell : VSet n)
(st : State n)
(hl : 1 ≤ level)
(h : Ready G level numcells st)
(ht : Generic.Target State.frame level tc cell st)
(hv : ∀ (v : Nat), cursor = some v → cell.mem v = true)
(hs : Store G.graph st)
:
Store G.graph
(Generic.sweep first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel cfuel level numcells tc tv1 cursor cell index
st).snd.snd
theorem
Hex.GraphIso.Nauty.Sparse.sweep_first_store
{n k : Nat}
(G : Sparse.Colored n k)
(hn : 0 < n)
(tcLevel fuel cfuel level numcells tc tv index : Nat)
(cell : VSet n)
(st : State n)
(hl : 1 ≤ level)
(h : Ready G level numcells st)
(ht : Generic.Target State.frame level tc cell st)
(hv : cell.mem tv = true)
(horbit : Generic.Policy.orbit st tv = tv)
(hs :
Store G.graph
(Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1)
(Generic.Policy.child true level tc tv st)).snd)
:
A store established by the first child survives its entire receiving sweep, even though the parent had no installed label before that child.