theorem
Hex.GraphIso.Nauty.Sparse.TraceFrame.first_scatter
{n k : Nat}
{G : Sparse.Colored n k}
{base level cells numcells : Nat}
{root st : State n}
(h : TraceFrame G base root st)
(hp : Ready G base cells root)
(hn : 0 < n)
(hb : 1 ≤ base)
(he : (classify (Graph.ofGraph G.graph) level numcells st).fst = Generic.Leaf.autoFirst)
:
The first-reference verdict's actual scatter stabilizes every frozen partition containing the current and first labels. Its cheap guard does not change which permutation is scattered.
theorem
Hex.GraphIso.Nauty.Sparse.TraceFrame.canon_scatter
{n k : Nat}
{G : Sparse.Colored n k}
{base level cells numcells : Nat}
{root st : State n}
(h : TraceFrame G base root st)
(hp : Ready G base cells root)
(hn : 0 < n)
(hb : 1 ≤ base)
(he : (classify (Graph.ofGraph G.graph) level numcells st).fst = Generic.Leaf.autoCanon)
:
Canonical-reference admission scatters the saved canonical label to the current label, both inside the frozen ancestor partition.
theorem
Hex.GraphIso.Nauty.Sparse.TraceFrame.classified
{n k : Nat}
{G : Sparse.Colored n k}
{base level cells numcells : Nat}
{root st : State n}
(h : TraceFrame G base root st)
(hp : Ready G base cells root)
(hr : Ready G level numcells st)
(hn : 0 < n)
(hb : 1 ≤ base)
(hlevel : base ≤ level)
:
have c := classify (Graph.ofGraph G.graph) level numcells st;
TraceFrame G base root (leafExit c.fst level c.snd).snd
The classifier and leaf action preserve the entire frozen-ancestor invariant. Every new trace entry is the literal scattered permutation; the other verdicts retain the trace and only update their documented fields.