theorem
Hex.GraphIso.Nauty.Sparse.short_implicit_fix
{n k : Nat}
{G : Sparse.Colored n k}
{level numcells : Nat}
{base out : State n}
(hn : 0 < n)
(hl : 1 ≤ level)
(h : Ready G level numcells base)
(hfixed : FixedCells level base.frame)
(hframe : FrameOut G level level base out)
(hf : out.fixedpts = base.fixedpts)
(hsaved : level ≤ out.noncheaplevel)
:
An implicit pair frozen below the receiving parent fixes every vertex of that parent's path, before the returned partition is recovered.
theorem
Hex.GraphIso.Nauty.Sparse.return_pair
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel level numcells tc tv target : Nat}
{first childFirst : Bool}
{cell : VSet n}
{st : State n}
{key : Nat → Key n}
{best : Option (Key n)}
(h : Ready G level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
(hpath : PathInv G level st)
(ht : Generic.Target State.frame level tc cell st)
(hv : cell.mem tv = true)
(hbound : target < level + 1)
(he :
(Generic.node childFirst (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1)
(Generic.Policy.child first level tc tv st)).fst = Generic.Exit.unwind target true)
(hreceive : level ≤ target)
(hguide : CanonGuide level tc st key best st)
(hcap : 0 < st.wsCap)
:
have raw :=
(Generic.node childFirst (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1)
(Generic.Policy.child first level tc tv st)).snd;
have out := Generic.Policy.leaveChild tv raw;
Saved G raw →
TraceOk G raw →
PairsOk G raw →
∀ (pair : VSet n × VSet n),
out.autos.back? = some pair → PairOk (Graph.context G.graph).g st.ptn st.lab level pair.fst pair.snd
Every pair read by the native short filter is valid at its receiving parent. Canonical scatters use the retained parent reference; implicit pairs use the exactly restored fixed set and established root-pair validity.
theorem
Hex.GraphIso.Nauty.Sparse.PairsReady.return_pair
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel level numcells tc tv target : Nat}
{first : Bool}
{cell : VSet n}
{st : State n}
{key : Nat → Key n}
{best : Option (Key n)}
(h : PairsReady G tcLevel level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
(ht : Generic.Target State.frame level tc cell st)
(hv : cell.mem tv = true)
(hrecord : CheapRecorded level tc st)
(hc : st.gcaCanon ≤ level)
(hcap : 0 < st.wsCap)
(he :
(Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1)
(Generic.Policy.child first level tc tv st)).fst = Generic.Exit.unwind target true)
(hreceive : level ≤ target)
(hguide : CanonGuide level tc st key best st)
:
have raw :=
(Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1)
(Generic.Policy.child first level tc tv st)).snd;
have out := Generic.Policy.leaveChild tv raw;
∀ (pair : VSet n × VSet n),
out.autos.back? = some pair → PairOk (Graph.context G.graph).g st.ptn st.lab level pair.fst pair.snd
A later sibling derives receiver validity from its reached native invariants. Complete child calls supply trace, pair and label soundness; the ancestor and cheap bounds determine the exact receiving level.
theorem
Hex.GraphIso.Nauty.Sparse.PairsReady.short_drop
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel level numcells tc tv target : Nat}
{first : Bool}
{cell : VSet n}
{st : State n}
{key : Nat → Key n}
{best : Option (Key n)}
(h : PairsReady G tcLevel level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
(ht : Generic.Target State.frame level tc cell st)
(hv : cell.mem tv = true)
(hrecord : CheapRecorded level tc st)
(hc : st.gcaCanon ≤ level)
(hcap : 0 < st.wsCap)
(he :
(Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1)
(Generic.Policy.child first level tc tv st)).fst = Generic.Exit.unwind target true)
(hreceive : level ≤ target)
(hguide : CanonGuide level tc st key best st)
:
have raw :=
(Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1)
(Generic.Policy.child first level tc tv st)).snd;
have out := Generic.Policy.leaveChild tv raw;
∀ (v : Nat),
v < n →
cell.mem v = true →
(Generic.Policy.shortprune cell out).mem v = false →
∃ (gamma : Array Nat), checkAutom (Graph.context G.graph).g gamma = true ∧ CellStab st.ptn level st.lab gamma ∧ gamma[v]! < v
A vertex removed by the actual received short filter has a strictly smaller representative under a checked automorphism of the parent cells. The witness comes from that child's emitted pair, including implicit pairs.