theorem
Hex.GraphIso.Nauty.Max.matches_reference
{n : Nat}
{ctx : Ctx n}
{level : Nat}
{st out : Search n}
{targets : List Nat}
{key : Key n}
(h : Generation.Matches ctx level st targets key)
(he : SearchState.reference out = SearchState.reference st)
:
Generation.Matches ctx level out targets key
Stored matching depends only on the three first-reference fields.
theorem
Hex.GraphIso.Nauty.Max.firstPath_witness
{n k : Nat}
{G : Colored n k}
{tcLevel fuel level numcells last : Nat}
{st leaf : Search n}
(hp : Generic.FirstPath { g := rowsOf G } tcLevel fuel level numcells st last leaf)
(hn : ∀ (f : Nat), f < fuel → (contract G tcLevel).nodeValid f (Generic.nodeCall { g := rowsOf G } (n + 2) tcLevel f))
{cs bs fs : List Nat}
{parents : Parents n}
(hi :
NodeInput G { g := rowsOf G } tcLevel fuel true { level := level, numcells := numcells, codes := cs, entry := st } bs
fs parents)
:
have ctx := { g := rowsOf G };
have out := (node true ctx (n + 2) tcLevel fuel level numcells st).snd;
∃ (targets : List Nat), ∃ (key : Key n), Generation.RefPath ctx tcLevel out.allsamelevel level (SearchState.refined ctx level numcells st) targets key ∧ Generation.Matches ctx level out targets key
The saved first reference retains uniformity along its actual descent, at precisely the all-same boundary returned by the complete search call.