theorem
Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.first_codes
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{f : Frame n}
(h : Valid G f)
(hs : StoredCodes f.entry.firstcode 1 f.codes)
(ha : n < f.entry.firstcode.size)
:
Actual first preparation extends the stored ancestor codes by its executed refinement code at the allocated next slot.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.first_key
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{f : Frame n}
{label : Label n}
(h : Valid G f)
:
The label at an actual first discrete visit has exactly the complete frozen node key, with the native ancestor codes and sentinel.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.first_best
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{f : Frame n}
(h : Valid G f)
(hs : StoredCodes f.entry.firstcode 1 f.codes)
(ha : n < f.entry.firstcode.size)
(hc : f.entry.canoncode.size = n + 2)
(hb : ∀ (code : Nat), code ∈ f.codes → code < codeSentinel)
:
have p := Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry;
p.fst = n → State.best G.graph (firstterminal f.level p.snd.snd.snd.snd) = some (key G.graph tcLevel f)
The first leaf's installed native incumbent is the whole frozen node key. Its code machine is derived from the actual stored prefix and allocation, without an assumed leaf comparison or key equality.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Frame.first_step
{n : Nat}
{G : SparseGraph n}
{tcLevel : Nat}
{f : Frame n}
(next : Generic.SweepFn (State n) n)
(hd : (Generic.prepareFirst (Graph.ofGraph G) tcLevel f.level f.numcells f.entry).fst = n)
:
Generic.nodeStep (Graph.ofGraph G) tcLevel next true f.level f.numcells f.entry = (Generic.Exit.unwind (f.level - 1) false, firstterminal f.level (Generic.prepareFirst (Graph.ofGraph G) tcLevel f.level f.numcells f.entry).snd.snd.snd.snd)
The actual first discrete node installs its prepared leaf and invokes no sibling continuation.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.first_leaf
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel : Nat}
{f : Frame n}
(h : Valid G f)
(hs : StoredCodes f.entry.firstcode 1 f.codes)
(ha : n < f.entry.firstcode.size)
(hc : f.entry.canoncode.size = n + 2)
(hb : ∀ (code : Nat), code ∈ f.codes → code < codeSentinel)
(hd : (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).fst = n)
(witness : Nat → Option (Key n) → Prop)
:
The executed first discrete call satisfies its full maximum contract from actual code storage and allocation, including a root-level return.