def Hex.GraphIso.Nauty.Sparse.Max.Loop.Count {n : Nat} (G : SparseGraph n) (tcLevel guide : Nat) (l : Loop n) (previous : Option Nat) (index : Nat) : Prop

The native orbit counter records distinct original target vertices with checked carriers in the frozen target-cell stabilizer.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Sparse.Max.Loop.mark {n k : Nat} {G : Sparse.Colored n k} {tcLevel guide tv index : Nat} {l : Loop n} {ready : State n} {previous : Option Nat} (h : Cell.Valid G (cell G.graph tcLevel l)) (hc : Count G.graph tcLevel guide l previous index) (ha : After previous tv) (hv : (cell G.graph tcLevel l).vertices.mem tv = true) (ho : OrbitTrace G ready) (ht : TraceOk G ready) (hg : TraceFrame G l.node.level (cell G.graph tcLevel l).entry ready) : Count G.graph tcLevel guide l (some tv) (if (ready.orbits[tv]! == guide) = true then index + 1 else index)

The literal orbit-pointer test supplies the checked carrier for each counted vertex. Its trace stabilization is read in the original target frame, independently of the surviving mutable target set.

theorem Hex.GraphIso.Nauty.Sparse.Max.SweepInput.mark {n k : Nat} {G : Sparse.Colored n k} {tcLevel guide tv index : Nat} {l : Loop n} {bs fs : List Nat} {cell : VSet n} {st ready : State n} {parents : Parents n} {previous : Option Nat} (h : SweepInput G tcLevel l bs fs (some tv) cell st parents) (hc : Loop.Count G.graph tcLevel guide l previous index) (ha : After previous tv) (ho : OrbitTrace G ready) (ht : TraceOk G ready) (hg : TraceFrame G l.node.level (Loop.cell G.graph tcLevel l).entry ready) : Loop.Count G.graph tcLevel guide l (some tv) (if (ready.orbits[tv]! == guide) = true then index + 1 else index)

Every live sweep cursor is eligible for the same frozen-cell count rule, including after target-set filtering and label reordering.

theorem Hex.GraphIso.Nauty.Sparse.Max.SweepInput.tail_counted {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel cfuel guide index : Nat} {l : Loop n} {bs fs : List Nat} {cursor previous : Option Nat} {cell : VSet n} {st : State n} {parents : Parents n} (h : SweepInput G tcLevel l bs fs cursor cell st parents) (hf : l.first = true) (heq : st.eqlevFirst = l.node.level) (hsame : l.node.level < st.allsamelevel) (hbudget : n ≤ l.node.level + fuel) (hpast : Generic.Past l.first guide cursor) (hc : Loop.Count G.graph tcLevel guide l previous index) (ha : ∀ (v : Nat), cursor = some v → After previous v) : ∃ (last : Option Nat), Loop.Count G.graph tcLevel guide l last (Generic.sweep l.first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel cfuel l.node.level (Loop.cell G.graph tcLevel l).numcells (Loop.cell G.graph tcLevel l).tc guide cursor cell index st).snd.fst

The actual later-sibling recursion retains witnesses for every counter increment. Cursor order prevents counting a vertex twice, and native trace stabilization justifies both visits and orbit skips.

theorem Hex.GraphIso.Nauty.Sparse.Max.FirstInput.counted {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel tv last : Nat} {f : Frame n} {leaf : State n} {parents : Parents n} (h : FirstInput G tcLevel f parents) (hi : (visit (Graph.ofGraph G.graph) f.level f.numcells f.entry).fst < n) (htv : (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).snd.snd.fst.nextElem none = some tv) (horbit : (cheapCheck true f.level (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).snd.snd.snd.snd).orbits[tv]! = tv) (path : have p := Frame.firstParent G.graph tcLevel f [] tv; have ch := Parent.child G.graph tcLevel p; Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel ch.level ch.numcells ch.entry last leaf) (hf : n ≤ f.level + fuel) : have l := { node := f, first := true }; have c := Loop.cell G.graph tcLevel l; have p := Frame.firstParent G.graph tcLevel f [] tv; ∃ (previous : Option Nat), Loop.Count G.graph tcLevel tv l previous (Generic.sweep true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (n + 1) f.level c.numcells p.tc tv (some tv) p.cell 0 p.state).snd.fst

The complete native first sweep counts only distinct original vertices carried to its guide. The guiding child's mark and every later increment use the actual emitted trace and recovered state.

theorem Hex.GraphIso.Nauty.Sparse.Max.Loop.Count.full {n : Nat} {G : SparseGraph n} {tcLevel guide index : Nat} {l : Loop n} {previous : Option Nat} (h : Count G tcLevel guide l previous index) (hfull : (cell G tcLevel l).len ≤ index) (v : Nat) : v ∈ segN (cell G tcLevel l).entry.lab (cell G tcLevel l).tc (cell G tcLevel l).len → ∃ (gamma : Array Nat), checkAutom (Graph.context G).g gamma = true ∧ CellStab (cell G tcLevel l).entry.ptn l.node.level (cell G tcLevel l).entry.lab gamma ∧ gamma[v]! = guide

Reaching the original target size supplies a checked stabilizing carrier for every original vertex, regardless of later target filtering.