structure Hex.GraphIso.Nauty.Sparse.Max.FirstEntry {n k : Nat} (G : Sparse.Colored n k) (f : Frame n) : Prop

Native first-path inputs retain the actual stored code prefix, reference allocations, blank row store, workspace and inherited cheap shape.

• frame : Frame.Valid G f
• shape : FirstShape G.graph f.level f.numcells f.entry
• targetSize : n < f.entry.firsttc.size
• firstSize : f.entry.firstcode.size = n + 2
• canonSize : f.entry.canoncode.size = n + 2
• blank : f.entry.canong.toRows = (Graph.ofGraph G.graph).blank
• work : f.entry.workperm.size = n
• trace : TraceOk G f.entry
• stored : StoredCodes f.entry.firstcode 1 f.codes
• codes_lt (code : Nat) : code ∈ f.codes → code < codeSentinel

theorem Hex.GraphIso.Nauty.Sparse.Max.FirstEntry.initial {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; FirstEntry G { level := 1, numcells := p.snd.length, codes := [], entry := Sparse.initial (Graph.ofGraph G.graph) p.fst p.snd }

The native root initializer establishes every first-entry field.

theorem Hex.GraphIso.Nauty.Sparse.Max.FirstEntry.child {n k : Nat} {G : Sparse.Colored n k} {tcLevel tv : Nat} {f : Frame n} (h : FirstEntry G f) (hi : (visit (Graph.ofGraph G.graph) f.level f.numcells f.entry).fst < n) (hm : (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).snd.snd.fst.mem tv = true) : FirstEntry G (Parent.child G.graph tcLevel (Frame.firstParent G.graph tcLevel f [] tv))

First-entry storage and histories follow the literal native child, including target scratch borrowing and child cache invalidation.