theorem
Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.first_scatter
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{f : Frame n}
(h : Valid G f)
(hi : CodeEntry G tcLevel f.level f.numcells f.entry)
(ha :
have p := prepareOther (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry;
(classify (Graph.ofGraph G.graph) f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.autoFirst)
:
The actual first-reference emission retains its native automorphism scatter, including admission through the cheap guard. The saved-history and workspace premises come from the production code entry.
theorem
Hex.GraphIso.Nauty.Sparse.Max.first_exit
{n : Nat}
(level : Nat)
(st : State n)
:
(leafExit Generic.Leaf.autoFirst level st).fst = Generic.Exit.unwind (leafExit Generic.Leaf.autoFirst level st).snd.gcaFirst false
First-reference admission returns exactly to its retained first ancestor and does not request a short filter.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.auto_first
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{f : Frame n}
{bs fs : List Nat}
{parents : Parents n}
(h : Valid G f)
(hi : CodeEntry G tcLevel f.level f.numcells f.entry)
(hc : Comparison G.graph f.codes bs fs f.entry)
(hs : Scope G tcLevel f bs f.entry parents)
(hg : Guides G.graph tcLevel f.entry parents)
(hpos : 0 < f.entry.gcaFirst)
(hlt : f.entry.gcaFirst < f.level)
(ha :
have p := prepareOther (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry;
(classify (Graph.ofGraph G.graph) f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.autoFirst)
:
The actual first-reference leaf satisfies the full native maximum return contract. Nonlocal coverage comes from its retained covered first child and the emitted automorphism, using the derived ancestor geometry.