theorem Hex.GraphIso.Nauty.Max.reference_complete {n k : Nat} (G : Colored n k) (tcLevel fuel : Nat) (f : Frame n) (bs fs : List Nat) (parents : Parents n) (boundary : Nat) (targets : List Nat) (key : Key n) : (∀ (q : Nat), q < fuel → (contract G tcLevel).nodeValid q (Generic.nodeCall { g := rowsOf G } (n + 2) tcLevel q)) → NodeInput G { g := rowsOf G } tcLevel fuel false f bs fs parents → Generation.RefPath { g := rowsOf G } tcLevel boundary f.level (SearchState.refined { g := rowsOf G } f.level f.numcells f.entry) targets key → Generation.Matches { g := rowsOf G } f.level f.entry targets key → f.entry.eqlevFirst = f.level - 1 → boundary ≤ f.entry.allsamelevel → ∀ (target : Nat) (short : Bool), (node false { g := rowsOf G } (n + 2) tcLevel fuel f.level f.numcells f.entry).fst = Generic.Exit.unwind target short → RefReturn { g := rowsOf G } target (node false { g := rowsOf G } (n + 2) tcLevel fuel f.level f.numcells f.entry).snd

A valid actual off-path node containing the stored reference returns emitted evidence. The only recursive premises are smaller maximum calls; reference descent and its receiving sweeps are proved here.