def
Hex.GraphIso.Nauty.Max.Loop.Count
{n : Nat}
(ctx : Ctx n)
(tcLevel guide : Nat)
(l : Loop n)
(previous : Option Nat)
(index : Nat)
:
The counter records checked carriers to the guiding vertex in the original target partition, independently of the mutable surviving set.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.Max.SweepInput.mark
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel level numcells tc tv1 tv index : Nat}
{cell : VSet n}
{st ready : Search n}
{l : Loop n}
{bs fs : List Nat}
{parents : Parents n}
{previous : Option Nat}
(h : SweepInput G ctx tcLevel fuel cfuel true level numcells tc tv1 (some tv) cell index st l bs fs parents)
(hc : Loop.Count ctx tcLevel tv1 l previous index)
(ha : After previous tv)
(ho : OrbitsOk ready)
(ht : TraceOk ctx ready)
(hg :
∀ (γ : Array Nat),
γ ∈ ready.genTrace →
CellStab (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.ptn level (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.lab
γ)
:
The actual orbit-counter test supplies a checked carrier for the vertex counted, using the current trace in the frozen parent partition.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.counted
{n k : Nat}
{G : Colored n k}
{tcLevel fuel : Nat}
(hn : (contract G tcLevel).nodeValid fuel (Generic.nodeCall { g := rowsOf G } (n + 2) tcLevel fuel))
(cfuel level numcells tc tv1 : Nat)
(cursor : Option Nat)
(cell : VSet n)
(index : Nat)
(st : Search n)
(l : Loop n)
(bs fs : List Nat)
(parents : Parents n)
(previous : Option Nat)
:
SweepInput G { g := rowsOf G } tcLevel fuel cfuel true level numcells tc tv1 cursor cell index st l bs fs parents →
Loop.Count { g := rowsOf G } tcLevel tv1 l previous index →
(∀ (tv : Nat), cursor = some tv → After previous tv) →
∃ (last : Option Nat), Loop.Count { g := rowsOf G } tcLevel tv1 l last
(sweep true { g := rowsOf G } (n + 2) tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.fst
The first sweep's counter has witnesses for distinct original vertices. Child contracts provide the accumulated cell stabilizers at actual returns; neither key equality nor transitivity is assumed.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.full
{n k : Nat}
{G : Colored n k}
{tcLevel fuel cfuel level numcells tc tv1 : Nat}
{cursor : Option Nat}
{cell : VSet n}
{st : Search n}
{l : Loop n}
{bs fs : List Nat}
{parents : Parents n}
(h : SweepInput G { g := rowsOf G } tcLevel fuel cfuel true level numcells tc tv1 cursor cell 0 st l bs fs parents)
(hn : (contract G tcLevel).nodeValid fuel (Generic.nodeCall { g := rowsOf G } (n + 2) tcLevel fuel))
(hcount :
(Loop.prepare { g := rowsOf G } tcLevel l).snd.snd.snd.fst ≤ (sweep true { g := rowsOf G } (n + 2) tcLevel fuel cfuel level numcells tc tv1 cursor cell 0 st).snd.fst)
(v : Nat)
:
v ∈ segN (Loop.prepare { g := rowsOf G } tcLevel l).snd.snd.snd.snd.lab tc
(Loop.prepare { g := rowsOf G } tcLevel l).snd.snd.snd.fst →
∃ (γ : Array Nat), checkAutom (rowsOf G) γ = true ∧ CellStab (Loop.prepare { g := rowsOf G } tcLevel l).snd.snd.snd.snd.ptn level
(Loop.prepare { g := rowsOf G } tcLevel l).snd.snd.snd.snd.lab γ ∧ γ[v]! = tv1
A complete orbit count supplies a checked frozen-cell carrier for every original target vertex, even if filters removed it from the sweep.