theorem Hex.GraphIso.Nauty.Generation.picked_singleton {n : Nat} {ctx : Ctx n} {level target : Nat} {st : SearchSt n} {trail : FrameTrail} {entry : TrailEntry} (h : TrailOk ctx level st trail) (hlt : target < level) (he : trail target = some entry) : IsCell st.ptn (target + 1) entry.frame.tc 1

The child selected at an ancestor is already a singleton at the level immediately below that ancestor, not merely at the current search level.

theorem Hex.GraphIso.Nauty.Generation.picked_fix {n : Nat} {ctx : Ctx n} {level target saved : Nat} {st : SearchSt n} {trail : FrameTrail} {entry : TrailEntry} (h : TrailOk ctx level st trail) (hlt : target < level) (he : trail target = some entry) (hdeep : target < saved) (hsize : st.ptn.size = n) (hend : st.ptn[st.ptn.size - 1]! ≤ saved) (htc : entry.frame.tc < n) (hv : st.lab[entry.frame.tc]! < n) : (fmptn st.lab st.ptn saved n).fst.mem entry.frame.rsLab[entry.frame.tc + entry.offset]! = true

An implicit pair frozen below an ancestor fixes that ancestor's selected child as well. This is the extra fixed point needed when a guiding child returns a short-prune request to its parent.