theorem Hex.GraphIso.Nauty.Sparse.Max.SweepInput.reference_visit {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel boundary tv : Nat} {l : Loop n} {bs fs : List Nat} {cell : VSet n} {st out : State n} {parents : Parents n} {targets : List Nat} {key : Key n} {previous : Option Nat} {short : Bool} (h : SweepInput G tcLevel l bs fs (some tv) cell st parents) (hfirst : l.first = false) : have c := Loop.cell G.graph tcLevel l; have R := State.refined (Graph.ofGraph G.graph) l.node.level l.node.numcells l.node.entry; Generation.PathCover G.graph tcLevel boundary l.node.level R c.tc c.len targets key cell previous → Generation.CanonPast l.node.level c.tc previous st → cell.nextElem previous = some tv → Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (l.node.level + 1) (c.numcells + 1) (Generic.Policy.child l.first l.node.level c.tc tv st) = (Generic.Exit.unwind l.node.level short, out) → (∀ (o : Nat), o < c.len → R.lab[c.tc + o]! = tv → Generation.ChildPath G.graph tcLevel boundary l.node.level R c.tc targets key o → RefReturn (Graph.context G.graph) l.node.level out) → Generation.PathCover G.graph tcLevel boundary l.node.level R c.tc c.len targets key cell (some tv)

Receiving a native off-path child advances reference coverage. A canonical carrier comes from an earlier child; the other carrier kinds return above this receiver. The child-reference implication is the local premise supplied by the recursive reference-completion induction.