theorem Hex.GraphIso.Nauty.Sparse.Max.FirstInput.sweep_lower {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel tv last : Nat} {f : Frame n} {leaf : State n} {parents : Parents n} (h : FirstInput G tcLevel f parents) (hi : (visit (Graph.ofGraph G.graph) f.level f.numcells f.entry).fst < n) (htv : (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).snd.snd.fst.nextElem none = some tv) (horbit : (cheapCheck true f.level (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).snd.snd.snd.snd).orbits[tv]! = tv) (path : have p := Frame.firstParent G.graph tcLevel f [] tv; have ch := Parent.child G.graph tcLevel p; Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel ch.level ch.numcells ch.entry last leaf) (hf : n ≤ f.level + fuel) (hchild : have p := Frame.firstParent G.graph tcLevel f [] tv; have ch := Parent.child G.graph tcLevel p; have raw := Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel ch.level ch.numcells ch.entry; MaxResult (Frame.key G.graph tcLevel ch) none (State.best G.graph raw.snd) f.level (Witness G tcLevel (parents.push p).frames) raw.fst) : have p := Frame.firstParent G.graph tcLevel f [] tv; have swept := Generic.sweep true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (n + 1) f.level (Frame.target G.graph tcLevel f).numcells p.tc tv (some tv) p.cell 0 p.state; ExitCover (Frame.key G.graph tcLevel f) (State.best G.graph swept.snd.snd) f.level (Witness G tcLevel (parents.frames.insert f)) swept.fst

The first child's maximum result extends through the complete native first sweep. Recovery establishes the proved later-sibling context, and the actual short filter is justified by the first call's emitted pairs.