theorem
Hex.GraphIso.Nauty.Generation.Cover.reference
{n k : Nat}
{G : Colored n k}
{gs : List (Perm n)}
{base : List (Fin n)}
{guide tv u : Fin n}
{cell : VSet n}
{previous : Option Nat}
(h : Cover G gs base guide cell previous)
(hnext : cell.nextElem previous = some ↑tv)
(href : Aut.Orbit G base guide u → Carries G gs base u guide)
{ctx : Ctx n}
{ref cur : Array Nat}
{store : Array (Array Nat)}
{pos : Nat}
(hcarrier : LabelCarrier ctx ref cur store)
(htrace : Realizes G gs store.toList)
(hfix : ∀ (γ : Array Nat), γ ∈ store → ∀ (b : Fin n), b ∈ base → γ[↑b]! = ↑b)
(hpos : pos < n)
(hatRef : ref[pos]! = ↑u)
(hatCur : cur[pos]! = ↑tv)
:
A recorded scatter consumes the current child when its reference's orbit obligation was already discharged.
theorem
Hex.GraphIso.Nauty.Generation.Cover.receipt
{n k : Nat}
{G : Colored n k}
{gs : List (Perm n)}
{base : List (Fin n)}
{ctx : Ctx n}
{tcLevel fuel cfuel level numcells tc tv1 index : Nat}
{guide tv : Fin n}
{cell : VSet n}
{previous : Option Nat}
{short : Bool}
{st out : Search n}
{l : Max.Loop n}
{bs fs : List Nat}
{parents : Max.Parents n}
(h : Cover G gs base guide cell previous)
(hs : Max.SweepInput G ctx tcLevel fuel cfuel true level numcells tc tv1 (some ↑tv) cell index st l bs fs parents)
(hnext : cell.nextElem previous = some ↑tv)
(hpast : CanonPast level tc previous st)
(hcall :
node false ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child true level tc (↑tv) st) = (Generic.Exit.unwind level short, out))
(hreceipt : RefReturn ctx level out)
(horbits : OrbitsOk out)
(htrace : Realizes G gs out.genTrace.toList)
(hfix : ∀ (γ : Array Nat), γ ∈ out.genTrace → ∀ (b : Fin n), b ∈ base → γ[↑b]! = ↑b)
(hfirst : out.firstlab[tc]! = ↑guide)
(hcoset : out.cosetindex = ↑tv)
:
All three reference-return alternatives discharge the actual first sweep's current orbit obligation in the supplied final generated group.