theorem
Hex.GraphIso.Nauty.Max.NodeInput.frame_prefix
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel : Nat}
{first : Bool}
{f : Frame n}
{bs fs : List Nat}
{parents : Parents n}
{target : Nat}
(h : NodeInput G ctx tcLevel fuel first f bs fs parents)
(ht : target < f.level - 1)
:
The saved ancestor's next code is exactly the corresponding prefix of the emitting node's path, including the root at index zero.
theorem
Hex.GraphIso.Nauty.Max.NodeInput.code_witness
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel : Nat}
{first : Bool}
{f : Frame n}
{bs fs : List Nat}
{parents : Parents n}
{target : Nat}
{best : Option (Key n)}
(h : NodeInput G ctx tcLevel fuel first f bs fs parents)
(ht : target < f.level - 1)
(hb : ∀ (tail : Key n), Generic.Covers (prefixKey (List.take (target + 1) f.codes) tail) best)
:
Witness ctx tcLevel (Parents.frames ctx tcLevel parents) target best
A frozen comparison's universal prefix bound supplies the concrete ancestor witness expected by the maximum contract.