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

First-descent invariants before any leaf has been installed. Saved ancestor ranks and guides are local facts about the selected first child; reference containment is established only when that child's first leaf exists. The executable workspace and path invariants are retained too.

• entry : FirstEntry G f
• scope : Scope G tcLevel f [] f.entry parents
• guides : Guides G.graph tcLevel f.entry parents
• ranked (t : Nat) (p : Parent n) : parents t = some p → Parent.Ranked G.graph tcLevel p
• orbits : OrbitTrace G f.entry
• first : f.entry.gcaFirst = 0
• canon : f.entry.gcaCanon = 0
• empty : f.entry.genTrace = #[]
• capacity : 0 < f.entry.wsCap
• path : PathInv G f.level f.entry
• pairs : PairsOk G f.entry
• boundary : CheapBoundary G f.level f.entry
• bound : f.entry.noncheaplevel ≤ f.level

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

Stable colour initialization establishes the complete first-descent context directly from the native arrays and empty ancestor map.

theorem Hex.GraphIso.Nauty.Sparse.Max.FirstInput.child {n k : Nat} {G : Sparse.Colored n k} {tcLevel tv : Nat} {f : Frame 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) : have p := Frame.firstParent G.graph tcLevel f [] tv; FirstInput G tcLevel (Parent.child G.graph tcLevel p) (parents.push p)

Taking the native first cursor preserves the first-descent context. Its suspended rank follows from the complete selected window and the literal minimum cursor; the first reference is still uninstalled.