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

Every actual off-path node containing its matching reference returns checked emitted evidence. The fuel induction discharges the smaller-child premise of the native sweep theorem; cheap and boundary-uniform subtrees use their proved literal reference emission.