theorem
Hex.GraphIso.Nauty.Sparse.DistanceState.constOn
{n level split : Nat}
{s t : RefineSt n}
(h : DistanceState level s t n)
(hs : RefineSt.Valid level s)
(G : SparseGraph n)
(root : Fin n)
(hd : Distances G root s.hits)
(hb : split < n)
(hr : s.lab[split]! = ↑root)
(a len : Nat)
:
Completed distance classes stabilize the captured singleton splitter.
theorem
Hex.GraphIso.Nauty.Sparse.RefineSt.Valid.distance_start
{n level : Nat}
{s : RefineSt n}
(h : Valid level s)
(G : SparseGraph n)
(hq : s.queue.size = 1)
:
Valid level
{ lab := s.lab, ptn := s.ptn, active := s.active.erase s.queue[0]!, queue := #[], cellstart := s.cellstart,
cellend := s.cellend, indexed := s.indexed, hits := distvals (Graph.ofGraph G) s.lab[s.queue[0]!]!,
marks := s.marks, vmarks := s.vmarks, stamp := s.stamp, numcells := s.numcells, longcode := s.longcode }
Removing the sole queued splitter and installing native BFS distances preserves all structural state invariants.
theorem
Hex.GraphIso.Nauty.Sparse.RefineSt.Valid.distance_finish
{n level : Nat}
{s : RefineSt n}
(h : Valid level s)
(G : SparseGraph n)
(hq : s.queue.size = 1)
(hsplit : s.ptn[s.queue[0]!]! ≤ level)
(hinv : CertInv (Graph.context G) level s.toPartition)
{t : RefineSt n}
(ht :
DistanceState level
{ lab := s.lab, ptn := s.ptn, active := s.active.erase s.queue[0]!, queue := #[], cellstart := s.cellstart,
cellend := s.cellend, indexed := s.indexed, hits := distvals (Graph.ofGraph G) s.lab[s.queue[0]!]!,
marks := s.marks, vmarks := s.vmarks, stamp := s.stamp, numcells := s.numcells, longcode := s.longcode }
t n)
:
CertInv (Graph.context G) level t.toPartition
Any completed execution of the distance-cell scan transports the incoming certificate, using the proved native distance semantics.
theorem
Hex.GraphIso.Nauty.Sparse.RefineSt.Valid.distance_cert
{n level : Nat}
{s : RefineSt n}
(h : Valid level s)
(G : SparseGraph n)
(hq : s.queue.size = 1)
(hsplit : s.ptn[s.queue[0]!]! ≤ level)
(hinv : CertInv (Graph.context G) level s.toPartition)
:
have t :=
(have split := s.queue[0]!;
have state :=
{ lab := s.lab, ptn := s.ptn, active := s.active.erase split, queue := #[], cellstart := s.cellstart,
cellend := s.cellend, indexed := s.indexed, hits := distvals (Graph.ofGraph G) s.lab[split]!, marks := s.marks,
vmarks := s.vmarks, stamp := s.stamp, numcells := s.numcells, longcode := s.longcode };
have first := 0;
do
let __s ←
forIn [:n] (state, first) fun (x : Nat) (__s : RefineSt n × Nat) =>
have state := __s.fst;
have first := __s.snd;
if first ≥ n then pure (ForInStep.done (state, first))
else have last := state.cellend[first]!;
have __do_jp := fun (__r : Unit) (state : RefineSt n) =>
have first := last + 1;
pure (ForInStep.yield (state, first));
if first < last then
have state := splitCounts level first true state;
__do_jp () state
else __do_jp () state
have state : RefineSt n := __s.fst
pure state).run;
CertInv (Graph.context G) level t.toPartition
The literal shallow distance branch preserves the equitability certificate. Its extra depth and size guards require no additional semantic assumption.