theorem
Hex.GraphIso.Nauty.Generation.Cover.receipt
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{base : List (Fin n)}
{guide tv : Fin n}
{tcell : VSet n}
{cursor : Option Nat}
{tcLevel specFuel level numcells tc len : Nat}
{codes bs fs : List Nat}
{rsLab rsPtn : Array Nat}
{entry parent child out : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(h : Cover G base guide tcell cursor)
(hinv :
LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor entry parent best trail)
(hnext : tcell.nextElem cursor = some ↑tv)
(hpast : CanonPast level tc cursor parent)
(hgca : child.gcaCanon = parent.gcaCanon)
(hlab : child.canonlab = parent.canonlab)
(hguide : GuideRel (level + 1) child out)
(hreceipt : RefReturn ctx out (Int.ofNat level))
(htrace : ∀ (γ : Array Nat), γ ∈ out.genTrace → γ ∈ Aut.trace G)
(hfix : ∀ (γ : Array Nat), γ ∈ out.genTrace → ∀ (b : Fin n), b ∈ base → γ[↑b]! = ↑b)
(hfirst : out.firstlab[tc]! = ↑guide)
(hcurrent : out.lab[tc]! = ↑tv)
(hcoset : out.cosetindex = ↑tv)
:
A reference return to a first-path receiver discharges the visited vertex's full orbit obligation. The canonical source is an earlier child; the trace's fixed-base premise is supplied by the receiver's stabilization invariant, rather than by an assumption about arbitrary off-path traces.