@[reducible, inline]
abbrev
Hex.GraphIso.Nauty.Sparse.Generation.PathCover
{n : Nat}
(G : SparseGraph n)
(tcLevel boundary level : Nat)
(st : RefineSt n)
(tc len : Nat)
(targets : List Nat)
(key : Key n)
(cell : VSet n)
(cursor : Option Nat)
:
Coverage of a native reference carrying its saved uniformity boundary. The abstract ledger accounts for visited children and descending filters; its occurrence predicate describes native sparse child calls.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.Generation.PathCover.advance
{n : Nat}
{G : SparseGraph n}
{tcLevel boundary level tc len : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{cell : VSet n}
{cursor : Option Nat}
(h : PathCover G tcLevel boundary level st tc len targets key cell cursor)
{tv : Nat}
(hnext : cell.nextElem cursor = some tv)
(hcur : ∀ (o : Nat), o < len → st.lab[tc + o]! = tv → ¬ChildPath G tcLevel boundary level st tc targets key o)
:
theorem
Hex.GraphIso.Nauty.Sparse.Generation.PathCover.filterDesc
{n : Nat}
{G : SparseGraph n}
{tcLevel boundary level tc len : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{cell cell' : VSet n}
{cursor : Option Nat}
(h : PathCover G tcLevel boundary level st tc len targets key cell cursor)
(hstep :
∀ (o : Nat),
ChildLive st.lab tc len cell cursor o →
cell'.mem st.lab[tc + o]! = true ∨ ∃ (j : Nat), j < len ∧ ChildPath G tcLevel boundary level st tc targets key o = ChildPath G tcLevel boundary level st tc targets key j ∧ st.lab[tc + j]! < st.lab[tc + o]!)
(hsub : ∀ (v : Nat), cell'.mem v = true → cell.mem v = true)
:
PathCover G tcLevel boundary level st tc len targets key cell' cursor
A removed child retains its reference in a strictly smaller original child; previous removals are handled by the shared well-founded ledger.
theorem
Hex.GraphIso.Nauty.Sparse.Generation.PathCover.filterAutom
{n : Nat}
{G : SparseGraph n}
{tcLevel boundary level tc len : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{cell cell' : VSet n}
{cursor : Option Nat}
(h : PathCover G tcLevel boundary level st tc len targets key cell cursor)
(hr : RefineSt.Ready G level st)
(hc : IsCell st.ptn level tc len)
(hb : tc + len ≤ n)
(hn : 1 < len)
(hdrop :
∀ (o : Nat),
ChildLive st.lab tc len cell cursor o →
cell'.mem st.lab[tc + o]! = false →
∃ (gamma : Array Nat), checkAutom (Graph.context G).g gamma = true ∧ CellStab st.ptn level st.lab gamma ∧ gamma[st.lab[tc + o]!]! < st.lab[tc + o]!)
(hsub : ∀ (v : Nat), cell'.mem v = true → cell.mem v = true)
:
PathCover G tcLevel boundary level st tc len targets key cell' cursor
Checked cell stabilizers preserve the full native reference, including all target positions, codes and boundary uniformity.
theorem
Hex.GraphIso.Nauty.Sparse.Generation.PathCover.longprune
{n : Nat}
{G : SparseGraph n}
{tcLevel boundary level tc len : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{cell : VSet n}
{cursor : Option Nat}
(h : PathCover G tcLevel boundary level st tc len targets key cell cursor)
(hr : RefineSt.Ready G level st)
(hc : IsCell st.ptn level tc len)
(hb : tc + len ≤ n)
(hn : 1 < len)
{fixedpts : VSet n}
{autos : Array (VSet n × VSet n)}
(haut :
∀ (p : VSet n × VSet n),
p ∈ autos.toList → fixedpts.subset p.fst = true → PairOk (Graph.context G).g st.ptn st.lab level p.fst p.snd)
:
PathCover G tcLevel boundary level st tc len targets key (Nauty.longprune cell fixedpts autos) cursor
The literal long-prune filter preserves reference coverage using its checked active pairs. The frozen state is interpreted only for proofs.
theorem
Hex.GraphIso.Nauty.Sparse.Generation.PathCover.shortprune
{n : Nat}
{G : SparseGraph n}
{tcLevel boundary level tc len : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{cell : VSet n}
{cursor : Option Nat}
(h : PathCover G tcLevel boundary level st tc len targets key cell cursor)
(hr : RefineSt.Ready G level st)
(hc : IsCell st.ptn level tc len)
(hb : tc + len ≤ n)
(hn : 1 < len)
{out : State n}
(hlast :
∀ (fix mcr : VSet n), out.autos.back? = some (fix, mcr) → PairOk (Graph.context G).g st.ptn st.lab level fix mcr)
:
PathCover G tcLevel boundary level st tc len targets key (Nauty.shortprune cell out) cursor
The literal short-prune filter preserves reference coverage, including an implicit pair, when its receiver contract supplies pair validity.
theorem
Hex.GraphIso.Nauty.Sparse.Generation.PathCover.finish
{n : Nat}
{G : SparseGraph n}
{tcLevel boundary level tc len : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{cell : VSet n}
{cursor : Option Nat}
(h : PathCover G tcLevel boundary level st tc len targets key cell cursor)
(hnext : cell.nextElem cursor = none)
(o : Nat)
:
theorem
Hex.GraphIso.Nauty.Sparse.Generation.PathCover.smaller
{n : Nat}
{G : SparseGraph n}
{tcLevel boundary level tc len : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{cell : VSet n}
{cursor : Option Nat}
(h : PathCover G tcLevel boundary level st tc len targets key cell cursor)
{tv o : Nat}
(hnext : cell.nextElem cursor = some tv)
(ho : o < len)
(hlt : st.lab[tc + o]! < tv)
:
An earlier original child cannot retain a reference, even after an older filter removed it from the live target set.
theorem
Hex.GraphIso.Nauty.Sparse.Generation.PathCover.carrier
{n : Nat}
{G : SparseGraph n}
{tcLevel boundary level tc len : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{cell : VSet n}
{cursor : Option Nat}
(h : PathCover G tcLevel boundary level st tc len targets key cell cursor)
{tv oRef : Nat}
{ref cur : Array Nat}
{store : Array (Array Nat)}
(hnext : cell.nextElem cursor = some tv)
(hr : RefineSt.Ready G level st)
(hc : IsCell st.ptn level tc len)
(hb : tc + len ≤ n)
(hn : 1 < len)
(href : oRef < len)
(habsent : ¬ChildPath G tcLevel boundary level st tc targets key oRef)
(hcarrier : CellCarrier (Graph.context G) st.ptn level st.lab ref cur store)
(hatRef : ref[tc]! = st.lab[tc + oRef]!)
(hatCur : cur[tc]! = tv)
:
A recorded stabilizing carrier transfers reference absence to the current child, including an interrupted child that was not exhausted.
theorem
Hex.GraphIso.Nauty.Sparse.Generation.PathCover.reference
{n : Nat}
{G : SparseGraph n}
{tcLevel boundary level tc len : Nat}
{st : RefineSt n}
{targets : List Nat}
{key : Key n}
{cell : VSet n}
{cursor : Option Nat}
(h : PathCover G tcLevel boundary level st tc len targets key cell cursor)
{tv oRef : Nat}
{ref cur : Array Nat}
{store : Array (Array Nat)}
(hnext : cell.nextElem cursor = some tv)
(hr : RefineSt.Ready G level st)
(hc : IsCell st.ptn level tc len)
(hb : tc + len ≤ n)
(hn : 1 < len)
(href : oRef < len)
(hearlier : st.lab[tc + oRef]! < tv)
(hcarrier : CellCarrier (Graph.context G) st.ptn level st.lab ref cur store)
(hatRef : ref[tc]! = st.lab[tc + oRef]!)
(hatCur : cur[tc]! = tv)
:
A carrier from an earlier child advances the absence ledger using the ranked reference coverage retained through all previous filters.