theorem Hex.GraphIso.Nauty.Sparse.Max.SweepInput.reference {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel cfuel boundary tv1 index : Nat} {l : Loop n} {bs fs : List Nat} {cursor previous : Option Nat} {cell : VSet n} {st : State n} {parents : Parents n} {targets : List Nat} {key : Key n} (h : SweepInput G tcLevel l bs fs cursor cell st parents) (hfirst : l.first = false) (hbudget : n ≤ l.node.level + fuel) (hcursor : Generic.CursorFuel n cfuel cursor) (hboundary : l.node.level < boundary) (hvisit : ∀ {tv : Nat} {cell : VSet n} {st : State n} {bs : List Nat}, SweepInput G tcLevel l bs fs (some tv) cell st parents → Generation.Matches G.graph (l.node.level + 1) st targets key → st.eqlevFirst = l.node.level → boundary ≤ st.allsamelevel → ∀ (o : Nat), o < (Loop.cell G.graph tcLevel l).len → (Loop.cell G.graph tcLevel l).entry.lab[(Loop.cell G.graph tcLevel l).tc + o]! = tv → Generation.ChildPath G.graph tcLevel boundary l.node.level (State.refined (Graph.ofGraph G.graph) l.node.level l.node.numcells l.node.entry) (Loop.cell G.graph tcLevel l).tc targets key o → have out := Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (l.node.level + 1) ((Loop.cell G.graph tcLevel l).numcells + 1) (Generic.Policy.child l.first l.node.level (Loop.cell G.graph tcLevel l).tc tv st); ∀ (target : Nat) (short : Bool), out.fst = Generic.Exit.unwind target short → RefReturn (Graph.context G.graph) target out.snd) : 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; cell.nextElem previous = cursor → Generation.PathCover G.graph tcLevel boundary l.node.level R c.tc c.len targets key cell previous → (∃ (o : Nat), o < c.len ∧ Generation.ChildPath G.graph tcLevel boundary l.node.level R c.tc targets key o) → Generation.CanonPast l.node.level c.tc previous st → Generation.Matches G.graph (l.node.level + 1) st targets key → st.eqlevFirst = l.node.level → boundary ≤ st.allsamelevel → l.node.level < st.noncheaplevel → have out := Generic.sweep l.first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel cfuel l.node.level c.numcells c.tc tv1 cursor cell index st; ∃ (target : Nat), ∃ (short : Bool), out.fst = Generic.Exit.unwind target short ∧ target < l.node.level ∧ RefReturn (Graph.context G.graph) target out.snd.snd

An actual off-path sweep containing a matching reference returns emitted evidence above the receiver. The induction follows its finite cursor, using reference completion only for the actual smaller child calls. Received returns and both filters retain the original occurrence ledger.